| 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 |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
| Issue History |
|||
| 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 |
| Issue History |