WP simple goal unproved
ID0001625: This issue was created automatically from Mantis Issue 1625. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001625 | Frama-C | Plug-in > wp | public | 2014-01-22 | 2014-02-05 |
| Reporter | Anne | Assigned To | correnson | Resolution | no change required |
| Priority | normal | Severity | major | Reproducibility | have not tried |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Fluorine-20130601 | Target Version | - | Fixed in Version | - |
Description :
I don't succeed to prove simple assertions such as this one :
struct S { int n; int s; }; //@ ensures X->s == \old (X->s); assigns X; void g (struct S * X); void f (struct S * X, struct S * Y) { X->s = Y->s; g (X); /@ assert a2: X->s ≡ Y->s; */ } Alt-Ergo (0.95.2) says : [wp] [Alt-Ergo] Goal typed_f_assert_a2 : Unknown
and I also tried with coqide, and I get to a point where I have:
H3 : havoc (Mint_0 .[ shift X_0 1 <- Mint_0 (shift Y_0 1)]) Mint_1 X_0 2 ______________________________________(1/1) Mint_0 (shift Y_0 1) = Mint_1 (shift Y_0 1)
which seams ok (but I don't know how to finish).
Anyway, shouldn't this be proved automatically ?