Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001022Frama-CDocumentation > ACSLpublic2011-11-18 15:492016-01-26 08:52
ReporterJochen 
Assigned Topatrick 
PrioritynormalSeveritytextReproducibilityN/A
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Magnesium 
Summary0001022: suggest to explain semantics of missing loop assigns clause in Acsl manual
DescriptionIn the manual "ACSL: ANSI/ISO C Specification Language, Version 1.5", on p.35-36, the semantics of a loop assigns clause is explained. On p.34, the default for a missing assigns clause in a function contract is explained.

However, the default for a missing loop assigns clause seems to remain unexplained in the manual.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0006029)
patrick (developer)
2015-09-09 14:26

 If no loop assigns clause is given, assignments remain unspecified.
It is left to tools to compute an over-approximation of the sets
of assigned locations.
(0006030)
patrick (developer)
2015-09-09 14:26

 That text has been added into ACSL manual.

- Issue History
Date Modified Username Field Change
2011-11-18 15:49 Jochen New Issue
2011-11-18 15:49 Jochen Status new => assigned
2011-11-18 15:49 Jochen Assigned To => signoles
2011-11-18 18:56 signoles Assigned To signoles => virgile
2015-09-07 15:29 signoles Assigned To virgile => patrick
2015-09-09 14:26 patrick Note Added: 0006029
2015-09-09 14:26 patrick Note Added: 0006030
2015-09-18 07:34 patrick Status assigned => resolved
2015-09-18 07:34 patrick Resolution open => fixed
2016-01-26 08:51 signoles Fixed in Version => Frama-C Magnesium
2016-01-26 08:52 signoles Status resolved => closed
2016-06-21 14:11 signoles Category Documentation => Documentation > ACSL

Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker