--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on September 2013 ---
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>