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.