0002114: ACSL manual:issues affecting technical correctness or understanding

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0002114

Frama-C

Documentation > ACSL

public

2015-05-05 17:29

2016-01-26 08:52

Reporter

dcok@grammatech.com

Assigned To

patrick

Priority

normal

Severity

minor

Reproducibility

have not tried

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C Sodium

Target Version

Frama-C Magnesium

Fixed in Version

Frama-C Magnesium

Summary

0002114: ACSL manual:issues affecting technical correctness or understanding

Description

These are issues affecting technical correctness or understanding that I encountered in a recent read through of the ACSL 1.9 manual.

p. 27: There are extraneous { delimiters in the example.

p. 51/52, Example 2.42: Either line 3 of the example should have ? (n-1) :" instead of "? n :" or the explanation should be corrected.

p. 56, Example 2.47: "modifies t[k]" -> "only modifies t[k]"

p. 57: "where the file list.acsl contains logic definitions" -> "where the file List.acsl contains logic definitions" - at least I presume the name of the file must be a case-senstive match to the name of the module

p. 58: "\valid {L}(p) <==> \valid{L}(((char *)p)+(0..sizeof(*p)))" should be "\valid {L}(p) <==> \valid{L}(((char *)p)+(0..sizeof(*p)-1))" and similarly for \valid_read

p. 71, Example 2.59: These specs allow forbidden to have more values than the union of {\result} and \old(forbidden)

p. 72: In "It is however possible to write multi-line annotations for ghost code. These annotations
are enclosed between /@ and @/. As in normal annotations, @s at the beginning of a line
and at the end of the comment (before the final @/) are considered as blank." the /@ and @/ should be /*@ and @*/

Steps To Reproduce

Read the documentation

Tags

No tags attached.

Attached Files

Relationships

Notes
(0005911) dcok@grammatech.com (reporter) 2015-05-05 17:36	One more: p. 27: The statement "Beware that equality of unions is also equality of all fields." deserves some explanation. It is equality of all fields, even if they overlap - so not just equality of the last assignment. If it is equality of all fields, then the example just above ought to be true.

(0006022) patrick (developer) 2015-09-07 10:18	all accepted except: p.27 "There are extraneous { delimiters in the example." -> Extraneous { was not found? p. 72 "... the /@ and @/ should be /@ and @/" -> No, because the C preprocessor closes alls /@ when it reaches the first @/ p. 27 "... If it is equality of all fields, then the example just above ought to be true." -> No, for the union type the equality is false.

Issue History
Date Modified	Username	Field	Change
2015-05-05 17:29	dcok@grammatech.com	New Issue
2015-05-05 17:29	dcok@grammatech.com	Status	new => assigned
2015-05-05 17:29	dcok@grammatech.com	Assigned To	=> signoles
2015-05-05 17:33	signoles	Assigned To	signoles => virgile
2015-05-05 17:33	signoles	Target Version	=> Frama-C Magnesium
2015-05-05 17:36	dcok@grammatech.com	Note Added: 0005911
2015-09-04 10:50	bobot	Assigned To	virgile => patrick
2015-09-07 10:18	patrick	Note Added: 0006022
2015-09-07 10:29	patrick	Status	assigned => resolved
2015-09-07 10:29	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