--- layout: fc_discuss_archives title: Message 113 from Frama-C-discuss on December 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Proof conditions with simple pointer assignment



>> The conditions is not discharged although axiom select_store_eq seems
>> quite sufficient to discharge it. Is integer_of_int32 somehow getting in
>> the way?
>
>Which prover are you using? alt-ergo 0.9 seems indeed to have some
>difficulties, but Simplify 1.5.4 and z3 2.0 succeed on all obligations.

To complete Virgile's answer, alt-ergo 0.9 has problems with
-jessie-int-model bounded and -jessie-int-model modulo,
and succeeds with -jessie-int-model exact.

I think we can pass this along to alt-ergo developers, it can
probably be considered an interesting example.

Pascal