--- layout: fc_discuss_archives title: Message 31 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



Hi Lo?c,
I don't know if it can help, but:
frama-c -save q6.sav q6_stack.c
and then
frama-c -load q6.sav -wp -wp-rte ...
does not solve the problem (ie, some VCs are still missing).

Does WP access to the AST before kernel normalization?

(Your solution of "hard normalization" through <frama-c -print ..> is a good workaround)
D.

De : frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] De la part de Lo?c Correnson
Envoy? : mercredi 4 septembre 2013 16:23
? : Frama-C public discussion
Objet : Re: [Frama-c-discuss] Issues with WP on program doing simple pointer arithmetic

The kind of rephrasing that may work is to use 'frama-c -print' to normalize the source code.
          L.

Le 4 sept. 2013 ? 16:21, Lo?c Correnson <loic.correnson at cea.fr<mailto:loic.correnson at cea.fr>> a ?crit :


Hi,

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 !

Somebody else reported a simiar problem recently, but I can not figure out what is the origin.
As reported by Dillon, rephrasing the code can help. We are investigating the problem !

          L.

Le 4 sept. 2013 ? 15:17, David MENTRE <dmentre at linux-france.org<mailto:dmentre at linux-france.org>> a ?crit :





-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130904/60c6c3ce/attachment-0001.html>