Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001092Frama-CDocumentation > manualspublic2012-02-13 13:122016-06-21 14:20
ReporterJochen 
Assigned Topascal 
PrioritynormalSeveritytextReproducibilityN/A
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001092: some typos etc. in the value-analysis manual
DescriptionDuring reading the value-analysis manual, I collected some typos and similar issues. They are marked in cyan in the gif images (one per page) in the attached .tar.gz file. Corresponding explanatory text is contained in the file value-analysis-typos.txt.
TagsNo tags attached.
Attached Filesgz file icon value-analysis.tar.gz [^] (1,449,161 bytes) 2012-02-13 13:12

- Relationships

-  Notes
(0002923)
pascal (reporter)
2012-04-17 14:59

Hello, Jochen.

Thanks for taking these notes while reading the manual. I should warn you about a couple of suggestions I didn't apply:

- differences in log messages: I will have to play the tutorial again and update messages, but in fact, I will have to automate the updating of log messages in the manual when these change in new version.

- 55:
The program would be analyzed as non-terminating in any case, since an
overflow is considered as equivalent to non-termination, too (cf. p.18).

Right, but signed integer overflows are only considered as alarms if option -val-signed-overflow-alarms is set. Otherwise, 2's complement behavior is assumed, x eventually comes back to 0, and the loop terminates then.

- Issue History
Date Modified Username Field Change
2012-02-13 13:12 Jochen New Issue
2012-02-13 13:12 Jochen Status new => assigned
2012-02-13 13:12 Jochen Assigned To => signoles
2012-02-13 13:12 Jochen File Added: value-analysis.tar.gz
2012-02-13 13:13 signoles Assigned To signoles => pascal
2012-04-17 14:59 pascal Note Added: 0002923
2012-04-17 15:31 pascal Status assigned => resolved
2012-04-17 15:31 pascal Resolution open => fixed
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2016-06-21 14:11 signoles Category Documentation => Documentation > ACSL
2016-06-21 14:20 signoles Category Documentation > ACSL => Documentation > manuals


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker