0002390: dubious discharge of postcondition - Frama-C Bug Tracking System

(0006607)
correnson (manager)
2018-07-25 14:20

Indeed, formals are not (yet) allocated in the pre-state, although they are allocated just before the first statement of the body... This is a corner case, of course.

Typically, the following program is proven:

*@ requires \valid(&a); ensures \false; */
void f(int a) {
return ;
}

But, then, the following one fails with a WP error:

void g(int x) { f(x); }

[wp] User Error: Address of logic value (x_0)

This is because, when you instantiate the pre-condition of f with the formal parameters, you get an incorrect
expression with (&a).

(0006608)
correnson (manager)
2018-07-25 14:20

Formals not allocated in the pre-state

(0006609)
correnson (manager)
2018-07-25 14:22

Side note : we are also working on running smoke tests to detect infeasible requires (those that would allow to prove false).

Second side node : probably it would be a good idea to detect the usage of (&x) on a formal (x) inside pre-conditions.

(0006610)
virgile (developer)
2018-07-25 14:33

Third side note: this would also warrant a clarification in the ACSL manual itself, because at the moment there is nothing in it that precludes the usage of \valid(&a) in a requires.

By the way what would be the status of \valid(&a) in an ensures clause?

(0006611)
jens (reporter)
2018-07-25 14:44

Shall I create a request for clarification in the ACSL manual?

(0006612)
virgile (developer)
2018-07-25 14:48

@jens, That'd be great, thanks

(0006614)
correnson (manager)
2018-07-25 15:06

For the same reason, `\valid(&a)` is not valid in the ensures clause, also it is still valid just at the end of the body.

Although, `\valid(&a)` reveals the same problem of accessing the address of values when used at call-sites.
Actually, the Kernel shall reject any access to the address of a formal inside a function specification.

(0006615)
virgile (developer)
2018-07-25 15:25

this will be on the todo list as soon as this point of view is endorsed by the ACSL manual 😛

Issue History
Date Modified	Username	Field	Change
2018-07-24 17:57	jens	New Issue
2018-07-24 17:57	jens	Status	new => assigned
2018-07-24 17:57	jens	Assigned To	=> correnson
2018-07-24 17:57	jens	File Added: foo.c
2018-07-25 14:20	correnson	Note Added: 0006607
2018-07-25 14:20	correnson	Note Added: 0006608
2018-07-25 14:20	correnson	Status	assigned => resolved
2018-07-25 14:20	correnson	Resolution	open => no change required
2018-07-25 14:22	correnson	Note Added: 0006609
2018-07-25 14:33	virgile	Note Added: 0006610
2018-07-25 14:44	jens	Note Added: 0006611
2018-07-25 14:44	jens	Status	resolved => feedback
2018-07-25 14:44	jens	Resolution	no change required => reopened
2018-07-25 14:48	virgile	Note Added: 0006612
2018-07-25 15:06	correnson	Note Added: 0006614
2018-07-25 15:25	virgile	Note Added: 0006615

Notes
(0006607) correnson (manager) 2018-07-25 14:20	Indeed, formals are not (yet) allocated in the pre-state, although they are allocated just before the first statement of the body... This is a corner case, of course. Typically, the following program is proven: @ requires \valid(&a); ensures \false; / void f(int a) { return ; } But, then, the following one fails with a WP error: void g(int x) { f(x); } [wp] User Error: Address of logic value (x_0) This is because, when you instantiate the pre-condition of f with the formal parameters, you get an incorrect expression with (&a).

(0006608) correnson (manager) 2018-07-25 14:20	Formals not allocated in the pre-state

(0006609) correnson (manager) 2018-07-25 14:22	Side note : we are also working on running smoke tests to detect infeasible requires (those that would allow to prove false). Second side node : probably it would be a good idea to detect the usage of (&x) on a formal (x) inside pre-conditions.

(0006610) virgile (developer) 2018-07-25 14:33	Third side note: this would also warrant a clarification in the ACSL manual itself, because at the moment there is nothing in it that precludes the usage of \valid(&a) in a requires. By the way what would be the status of \valid(&a) in an ensures clause?

(0006611) jens (reporter) 2018-07-25 14:44	Shall I create a request for clarification in the ACSL manual?

(0006612) virgile (developer) 2018-07-25 14:48	@jens, That'd be great, thanks

(0006614) correnson (manager) 2018-07-25 15:06	For the same reason, `\valid(&a)` is not valid in the ensures clause, also it is still valid just at the end of the body. Although, `\valid(&a)` reveals the same problem of accessing the address of values when used at call-sites. Actually, the Kernel shall reject any access to the address of a formal inside a function specification.

(0006615) virgile (developer) 2018-07-25 15:25	this will be on the todo list as soon as this point of view is endorsed by the ACSL manual 😛

Relationships