Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002438Frama-CDocumentation > ACSLpublic2019-05-22 11:442019-05-22 11:44
Assigned Topatrick 
PrioritynormalSeverityfeatureReproducibilityhave not tried
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0002438: grammar and implementation disagree on predicate/logic declarations
DescriptionThe 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.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2019-05-22 11:44 davidrcok New Issue
2019-05-22 11:44 davidrcok Status new => assigned
2019-05-22 11:44 davidrcok Assigned To => patrick

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker