Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001698Frama-CDocumentation > ACSLpublic2014-03-14 10:142016-06-22 11:38
Reporterjens 
Assigned Topatrick 
PrioritynormalSeveritytextReproducibilityN/A
StatusclosedResolutionwon't fix 
PlatformOSOS Version
Product VersionFrama-C Neon-20140301 
Target VersionFixed in Version 
Summary0001698: Add remark about additional axioms for read clauses
DescriptionAs long as WP does not generate foot prints for reads clauses of axiomatic declarations (see https://bts.frama-c.com/view.php?id=1693), it might be helpful for users to understand, that it is their responsibility to formulate additional axioms/lemmas to express the foot print. This could be added to Section 2.6.10 of "ACSL Version 1.8 Implementation in Neon-20140301".
TagsNo tags attached.
Attached Files

- Relationships
related to 0001693assignedcorrenson Generate footprint from reads clauses of logic declarations 

-  Notes
(0006214)
patrick (developer)
2016-06-22 11:38

If something has to be added to WP manual, do not hesitate to reopen the issue.

- Issue History
Date Modified Username Field Change
2014-03-14 10:14 jens New Issue
2014-03-14 10:14 jens Status new => assigned
2014-03-14 10:14 jens Assigned To => signoles
2014-03-14 13:22 signoles Relationship added related to 0001693
2014-03-14 13:22 signoles Assigned To signoles => correnson
2015-09-07 15:28 signoles Assigned To correnson => patrick
2015-09-09 14:07 patrick Assigned To patrick => correnson
2016-06-21 14:11 signoles Category Documentation => Documentation > ACSL
2016-06-21 14:26 signoles Assigned To correnson => patrick
2016-06-22 11:38 patrick Note Added: 0006214
2016-06-22 11:38 patrick Status assigned => closed
2016-06-22 11:38 patrick Resolution open => won't fix


Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker