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-07-17 11:14
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
patrick (developer)
2019-07-17 11:14

Moved to

- 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
2019-07-17 11:14 patrick Note Added: 0006824
2019-07-17 11:14 patrick Status assigned => closed
2019-07-17 11:14 patrick Resolution open => fixed

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker