0001092: some typos etc. in the value-analysis manual - Frama-C Bug Tracking System

Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

ID

Project

Category

View Status

Date Submitted

Last Update

0001092

Frama-C

Documentation > manuals

public

2012-02-13 13:12

2016-06-21 14:20

Reporter

Jochen

Assigned To

pascal

Priority

normal

Severity

text

Reproducibility

N/A

Status

closed

Resolution

fixed

Platform

OS

OS Version

Product Version

Frama-C Nitrogen-20111001

Target Version

Fixed in Version

Frama-C Oxygen-20120901

Summary

0001092: some typos etc. in the value-analysis manual

Description

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.

Tags

No tags attached.

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