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;
}