0001461: assigns, loop assigns and loop invariant

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0001461

Frama-C

Plug-in > wp

public

2013-07-24 18:36

2014-06-17 15:02

Reporter

virgile

Assigned To

correnson

Priority

normal

Severity

minor

Reproducibility

always

Status

acknowledged

Resolution

open

Platform

OS Version

Product Version

Frama-C GIT, precise the release id

Target Version

Fixed in Version

Summary

0001461: assigns, loop assigns and loop invariant

Description

In the following (admittedly contrived) example, the assigns of g is not proved by WP (in fact it is reduced to false by Qed), although it is correct from ACSL semantics: as long as the loop invariant states that x still has its old value, the fact that it is mentioned in the loop assigns should not impede its absence in the assigns.

--- test.c
int x;

/*@ assigns \nothing; */
int g() {
  /*@ loop assigns i,x;
      loop invariant x == \at(x,Pre);
  */
  for (int i = 0; i<2; i++);
  return x;
}

Steps To Reproduce

frama-c -wp test.c

Tags

No tags attached.

Attached Files

Relationships

related to

0001812

acknowledged

correnson

Assigns not respected in behaviors when using pointers to pointers

Notes
(0004012) correnson (manager) 2013-07-30 09:50	This is known limitation of the WP. Assigns are verified with a stronger method than necessary: WP checks that all effects are included in the assigns specified, which is sufficient but not necessary. The workaround is to modify the contract with: /@ assigns x; ensures x ==\old(x); / int g() { /@ loop assigns i,x; loop invariant x == \at(x,Pre); / for (int i = 0; i<2; i++); return x; } An evolution of the WP may infer automatically this workaround.

(0004013) correnson (manager) 2013-07-30 09:51	Feature wish: infer workaround.

(0004499) correnson (manager) 2014-02-05 14:30	Feature wish

Issue History
Date Modified	Username	Field	Change
2013-07-24 18:36	virgile	New Issue
2013-07-24 18:36	virgile	Status	new => assigned
2013-07-24 18:36	virgile	Assigned To	=> correnson
2013-07-30 09:50	correnson	Note Added: 0004012
2013-07-30 09:51	correnson	Note Added: 0004013
2013-07-30 09:51	correnson	Status	assigned => confirmed
2014-02-05 14:30	correnson	Note Added: 0004499
2014-02-05 14:30	correnson	Status	confirmed => acknowledged
2014-06-17 11:02	correnson	Relationship added	related to 0001812