dubious discharge of postcondition
ID0002390: This issue was created automatically from Mantis Issue 2390. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002390 | Frama-C | Plug-in > wp | public | 2018-07-24 | 2019-10-17 |
| Reporter | jens | Assigned To | correnson | Resolution | no change required |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C 17-Chlorine | Target Version | - | Fixed in Version | - |
Description :
Consider 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.