| View Issue Details [ Jump to Notes ] [ Related Changesets ] | [ Issue History ] [ Print ] |
| ID | Project | Category | View Status | Date Submitted | Last Update |
| 0001670 | Frama-C | Plug-in > wp | public | 2014-03-04 09:36 | 2015-03-17 22:17 |
|
| Reporter | Anne | |
| Assigned To | correnson | |
| Priority | normal | Severity | minor | Reproducibility | always |
| Status | closed | Resolution | fixed | |
| Platform | | OS | | OS Version | |
| Product Version | | |
| Target Version | | Fixed in Version | Frama-C Sodium | |
|
| Summary | 0001670: WP ignores some goals when 'initialized' is used in hypotheses |
| Description | The message:
[wp] warning: Allocable, Freeable, Valid_read, Fresh and Initialized not yet implemented
is perfectly clear, but I would have expected that annotations using these predicates would have been ignored. Instead of that, proof obligations of other annotations simply disappear. |
| Steps To Reproduce | Example:
/*@ requires r1: \initialized(Y+(0 .. 99));
assigns X[0..99];
ensures X[0] == Y[0];
*/
void cp( int *X, int *Y );
void f (int *A, int *B) {
cp(B, A);
/*@ assert a1: A[0] == B[0]; */
}
Without the 'requires' property, the assertion is proved:
$ frama-c -wp test.c -wp-prop a1
...
[wp] 1 goal scheduled
[wp] [Qed] Goal typed_f_assert_a1 : Valid
[wp] Proved goals: 1 / 1
Qed: 1
With the 'requires' property, the assertion is not even scheduled as a goal:
$ frama-c -wp test.c -wp-prop a1
...
[wp] 0 goal scheduled
[wp] Proved goals: 0 / 0 |
| Tags | No tags attached. |
|
| Attached Files | |
|
Relationships 
Relationships