Enhancement on assigns annotation and the name of proof obligation
ID0000544: This issue was created automatically from Mantis Issue 544. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000544 | Frama-C | Plug-in > jessie | public | 2010-07-17 | 2010-07-17 |
| Reporter | logan | Assigned To | cmarche | Resolution | open |
| Priority | normal | Severity | feature | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Boron-20100401 | Target Version | - | Fixed in Version | - |
Description :
Consider the following functions. Both function violates ACSL specification, and all of the theorem prover gives UNKNOWN as result (which is correct and expected).
However, the name of proof obligation of test2() is "loop invariants initially holds" which is a little confusing. Since the problem is actually on the assign statement instead of the while-loop. I think it will be better to have an independent check for @assigns annotation just like the "postcondition" proof obligation of test1().
int global;
/*@ assigns \nothing; */ int test1() { global = 1; }
/*@ assigns \nothing; */ int test2() { global = 2;