grammar and implementation disagree on predicate/logic declarations
ID0002438: This issue was created automatically from Mantis Issue 2438. Further discussion may take place here.
|ID0002438||Frama-C||Documentation > ACSL||public||2019-05-22||2019-07-17|
|Priority||normal||Severity||feature||Reproducibility||have not tried|
|Product Version||-||Target Version||-||Fixed in Version||-|
The ACSL grammar has declarations: //@ predicate a; and definitions //@ predicate a = \true;
The current grammar requires declarations to be in an axiomatic. However the current implementation in Frama-C allows both definitions and declarations both at global scope and within axiomatics.
I propose changing the ACSL documentation/grammar to match current behavior.
Similarly axioms should be allowed both inside and outside axiomatics.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information