0000765: Post-state of statement spec - Frama-C Bug Tracking System

(0001640)
Anne (reporter)
2011-03-25 15:55

It is not easy to fix because it seems that we want another behavior for the post-condition of a loop since the end of the block is never reached directly, but always through [break] statements.

(0001716)
Anne (reporter)
2011-04-11 15:48

The previous note is not true if we imagine that the break label is in the loop statement as if the loop were in a block. BTW the block also includes the initial part of the [for] loop. When fixing this bug, one should also consider the conclusion of the "commit" mailing list discussion (the 6 of April 2011) about the [assigns] property of a statement.

(0001718)
Anne (reporter)
2011-04-11 15:49

@Loïc: I transfer this task to you as you asked for.

(0002649)
patrick (developer)
2012-01-31 16:16

There is another similar example raising an exception: void g(int c) { int r; r=0; //@ assigns \nothing; if(c) { goto stop; } stop: ; r=1; } frama-c -wp file.c ... [wp] failure: Merging different assigns goals [kernel] The full backtrace is: Raised at file "src/wp/register.ml", line 615, characters 27-29

Issue History
Date Modified	Username	Field	Change
2011-03-25 15:52	Anne	New Issue
2011-03-25 15:52	Anne	Status	new => assigned
2011-03-25 15:52	Anne	Assigned To	=> dargaye
2011-03-25 15:52	Anne	File Added: toto.c
2011-03-25 15:52	Anne	Assigned To	dargaye => Anne
2011-03-25 15:55	Anne	Note Added: 0001640
2011-03-25 15:55	Anne	Assigned To	Anne => patrick
2011-03-25 15:55	Anne	Assigned To	patrick => Anne
2011-04-11 15:48	Anne	Note Added: 0001716
2011-04-11 15:48	Anne	Assigned To	Anne => correnson
2011-04-11 15:49	Anne	Note Added: 0001718
2012-01-31 16:16	patrick	Note Added: 0002649

Notes
(0001640) Anne (reporter) 2011-03-25 15:55	It is not easy to fix because it seems that we want another behavior for the post-condition of a loop since the end of the block is never reached directly, but always through [break] statements.

(0001716) Anne (reporter) 2011-04-11 15:48	The previous note is not true if we imagine that the break label is in the loop statement as if the loop were in a block. BTW the block also includes the initial part of the [for] loop. When fixing this bug, one should also consider the conclusion of the "commit" mailing list discussion (the 6 of April 2011) about the [assigns] property of a statement.

(0001718) Anne (reporter) 2011-04-11 15:49	@Loïc: I transfer this task to you as you asked for.

(0002649) patrick (developer) 2012-01-31 16:16	There is another similar example raising an exception: void g(int c) { int r; r=0; //@ assigns \nothing; if(c) { goto stop; } stop: ; r=1; } frama-c -wp file.c ... [wp] failure: Merging different assigns goals [kernel] The full backtrace is: Raised at file "src/wp/register.ml", line 615, characters 27-29

Relationships