Frama-Clang does allow access to private fields within annotations

ID0001791: This issue was created automatically from Mantis Issue 1791. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0001791	Frama-Clang	Kernel	public	2014-05-30	2015-02-16

Reporter	jens	Assigned To	virgile	Resolution	open
Priority	normal	Severity	feature	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Neon-20140301	Target Version	-	Fixed in Version	-

Description :

The following example shows that the private field A::i can be accessed in an annotation. In my opinion the access rules in annotations should be the same as for code.

struct A { private:

int i;

public:

explicit A(int k) : i(k) {}

/*@
  assigns \nothing;
  ensures \result == i;
*/
int get() const
{
    return i;
}

};

int foo(const A& a) { int b = a.get(); //@ assert b == a.i; // Frama-Clang allows access to private field of A

// a.i cannot be accessed here because it is private
// this is recognized by Frama-Clang
// int c = a.i;

return b;

}