--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Issues with WP on program doing simple pointer arithmetic



Hello Dillon and Lo?c,

2013/9/4 Lo?c Correnson <loic.correnson at cea.fr>:
> It seems that, actually, many proof obligations are missing.
> The simple invariant over variable i is easily discharged on simple goals,
> but the proof obligation for preservation is missing in your case. There is
> a dangling node in the internal CFG generated by WP for your code, but don't
> know why !

OK, thank you for the explanations.

> Somebody else reported a simiar problem recently, but I can not figure out
> what is the origin.

Should I attach my example to this bug report? If yes, what is its identifier?

> As reported by Dillon, rephrasing the code can help. We are investigating
> the problem !

I'll use Dillon work-around for now. I'll try to keep the -print
normalization in mind for my production code.

Thanks for the quick feedback!
david