Frama-C Bug Tracking System - Frama-C
View Issue Details
0001092Frama-CDocumentation > manualspublic2012-02-13 13:122016-06-21 14:20
Jochen 
pascal 
normaltextN/A
closedfixed 
Frama-C Nitrogen-20111001 
Frama-C Oxygen-20120901 
0001092: some typos etc. in the value-analysis manual
During 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.
No tags attached.
gz value-analysis.tar.gz (1,449,161) 2012-02-13 13:12
https://bts.frama-c.com/file_download.php?file_id=334&type=bug
Issue History
2012-02-13 13:12JochenNew Issue
2012-02-13 13:12JochenStatusnew => assigned
2012-02-13 13:12JochenAssigned To => signoles
2012-02-13 13:12JochenFile Added: value-analysis.tar.gz
2012-02-13 13:13signolesAssigned Tosignoles => pascal
2012-04-17 14:59pascalNote Added: 0002923
2012-04-17 15:31pascalStatusassigned => resolved
2012-04-17 15:31pascalResolutionopen => fixed
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed
2016-06-21 14:11signolesCategoryDocumentation => Documentation > ACSL
2016-06-21 14:20signolesCategoryDocumentation > ACSL => Documentation > manuals

Notes
(0002923)
pascal   
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.