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