Soundness issue with dependency taclets

[wadoon]

This issue was created at git.key-project.org where the discussions are preserved.

---

Description

It is possible to prove false using the observerDependency taclets.

The problem is that this/these taclet/s do not check for recursion. They should not be applicable for certain symbols (without measuredby check).

Reproducible

Since the rules are not part of the automatic verification process, and usually the Use Dependency Contract Builtin Rule is used, one really must deliberately use this.

Still it should be fixed!

Steps to reproduce

Load the attached proof bundle problem.zproof. In one proof, the dependency contract is illegally applied.

Additional information

class A {

    int f;

    //@ normal_behaviour
    //@ ensures \result == f;
    //@ accessible \nothing;
    int m() { return f; }

    //@ normal_behaviour
    //@ ensures false;
    void problem() {}
}

---

• Commit: %"v2.8.0"

---

Information:

• created_at: 2021-02-17T16:30:05.372Z
• updated_at: 2021-02-17T16:30:05.372Z
• closed_at: None (closed_by: )
• milestone:
• user_notes_count: 0