Frama-C Bug Tracking System - Frama-C
View Issue Details
0002438Frama-CDocumentation > ACSLpublic2019-05-22 11:442019-07-17 11:14
davidrcok 
patrick 
normalfeaturehave not tried
closedfixed 
 
 
0002438: grammar and implementation disagree on predicate/logic declarations
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.
No tags attached.
Issue History
2019-05-22 11:44davidrcokNew Issue
2019-05-22 11:44davidrcokStatusnew => assigned
2019-05-22 11:44davidrcokAssigned To => patrick
2019-07-17 11:14patrickNote Added: 0006824
2019-07-17 11:14patrickStatusassigned => closed
2019-07-17 11:14patrickResolutionopen => fixed

Notes
(0006824)
patrick   
2019-07-17 11:14   
Moved to https://github.com/acsl-language/acsl [^]