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

[Frama-c-discuss] Assigns broken for arrays?



Hello,

On Wed, Apr 1, 2009 at 16:09, David MENTRE <dmentre at linux-france.org> wrote:
> I have open a bug:
> ?[#7560] Inability to prove assigns clauses on simple array code
> ?https://gforge.inria.fr/tracker/index.php?func=detail&aid=7560&group_id=1123&atid=5488

Virgile closed the bug. After further investigation, it appears that
even on original Boris' code, Alt-Ergo is unable to prove "assigns"
clause.

Boris, are you using another automated theorem prover than Alt-Ergo?

If this is the case, the issue is more related to Alt-Ergo than Jessie
itself. Is it possible to circumvent this issue, still using Alt-Ergo?

Yours,
d.