View Issue Details [ Jump to Notes ] | [ 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 | ||||||
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 |
|
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2014-03-04 09:36 | Anne | New Issue | |
2014-03-04 09:36 | Anne | Status | new => assigned |
2014-03-04 09:36 | Anne | Assigned To | => correnson |
2014-06-02 15:38 | correnson | Source_changeset_attached | => framac master 777b87af |
2014-06-02 15:38 | correnson | Note Added: 0005180 | |
2014-06-02 15:38 | correnson | Status | assigned => resolved |
2014-06-02 15:38 | correnson | Resolution | open => fixed |
2015-03-17 22:17 | signoles | Fixed in Version | => Frama-C Sodium |
2015-03-17 22:17 | signoles | Status | resolved => closed |