No access to inherited members of a struct in acsl clauses.
ID0001852: This issue was created automatically from Mantis Issue 1852. Further discussion may take place here.
|ID0001852||Frama-Clang||Plug-in > clang||public||2014-07-23||2014-12-12|
|Priority||normal||Severity||minor||Reproducibility||have not tried|
|Platform||-||OS||ubuntu 64 14.04||OS Version||-|
|Product Version||Frama-C Neon-20140301||Target Version||-||Fixed in Version||Frama-C GIT, precise the release id|
It is not possible to access the members of the base class through a pointer to the derived class. (pointer to object of derived struct -> member of base struct)
The problem only occurs if these two conditions are fullfilled:
- The member is inherited from the base class.
- The access happens inside an acsl clause. (i.e. after a requires or an ensures)
There are examples for all cases in the attached file "problem308.cpp".
Additional Information :
Error message: Unsupported Field Access to i in struct B