Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002390Frama-CPlug-in > wppublic2018-07-24 17:572018-07-25 15:25
Reporterjens 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusfeedbackResolutionreopened 
PlatformOSOS Version
Product VersionFrama-C 17-Chlorine 
Target VersionFixed in Version 
Summary0002390: dubious discharge of postcondition
DescriptionConsider the following function

/*@
   assigns \nothing;
   ensures a == 0;
*/
void foo(int a)
{
   a = 0;
}

The postcondition can of course not be verified because the assignment happens to a copy "a" and furthermore nothing is known about the value of "a" in the pre-state.

If I add, however, the admittedly weird looking precondition "requires \valid(&a);" as shown here

/*@
   requires \valid(&a);
   assigns \nothing;
   ensures a == 0;
*/
void bar(int a)
{
   a = 0;
}

then Qed discharges the postcondition.
I am not sure this a bug or rather caused by taking the address of a formal argument in the precondition
but in any case it would be nice if someone could have a look at it.
Steps To Reproduce
Call
   frama-c -wp -wp-rte foo.c
on the attached file.
TagsNo tags attached.
Attached Filesc file icon foo.c [^] (187 bytes) 2018-07-24 17:57 [Show Content]

- Relationships

-  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 😛

- 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

Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker