Add remark about additional axioms for read clauses
ID0001698: This issue was created automatically from Mantis Issue 1698. Further discussion may take place here.
|ID0001698||Frama-C||Documentation > ACSL||public||2014-03-14||2016-06-22|
|Reporter||jens||Assigned To||patrick||Resolution||won't fix|
|Product Version||Frama-C Neon-20140301||Target Version||-||Fixed in Version||-|
As long as WP does not generate foot prints for reads clauses of axiomatic declarations (see https://bts.frama-c.com/view.php?id=1693), it might be helpful for users to understand, that it is their responsibility to formulate additional axioms/lemmas to express the foot print. This could be added to Section 2.6.10 of "ACSL Version 1.8 Implementation in Neon-20140301".