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
Reporterdavidrcok 
Assigned Topatrick 
PrioritynormalSeverityfeatureReproducibilityhave not tried
StatusclosedResolutionfixed 
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
(0006824)
patrick (developer)
2019-07-17 11:14

Moved to https://github.com/acsl-language/acsl [^]

- 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 - 2019 MantisBT Team
Powered by Mantis Bugtracker