Frama-C Bug Tracking System - Frama-C
View Issue Details
0002438Frama-CDocumentation > ACSLpublic2019-05-22 11:442019-07-17 11:14
normalfeaturehave not tried
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

2019-07-17 11:14   
Moved to