--- layout: fc_discuss_archives title: Message 43 from Frama-C-discuss on June 2010 ---
Hi On Thu, Jun 17, 2010 at 8:29 AM, Pascal Cuoq <pascal.cuoq at gmail.com> wrote: > To go back to the larger point, both frama-c and frama-c-gui seem to > work as expected (not doing anything when invoked as "frama-c first.i" > is the expect behavior as Virgile pointed out) when they are passed > already pre-processed .i files. > However, while frama-c-gui is working correctly, gwhy isn't, it crashes when it is launched. This wasn't being a problem for me because what I needed to do was to generate VCs for a small code and check the validity of the ACSL annotations written by me and so I could easily do this in the batch mode. However, there is one VC that none automated provers seems to be able to verify, but I'd like to know the reason. And since this sort of informations is (I think) presented to the user in the gui-mode, I'd like to know if there is any way of knowing this in batch-mode. The command that I'm using is frama-c -jessie -jessie-atp alt-ergo array.c and in order to complete what I'm trying to do, that would be more useful to me than to set gwhy working. I should add that I actually know the code line that causes 1 VC not to be verified, it is v[i] = -v[i] I know this because I've noticed that if I replace it with v[i] = 1 there are no VCs left to be proved. I also know that it has to do with Integer Overflow because I've noticed that if I add the IntegerOverflow pragma in the top of the file it solves the problem. Thank you Ricardo > > Frama-C shows the command it tries to use for pre-processing .c files, > but if that doesn't work, you can instruct it to use another command > with the -cpp-command option. > Note that the "%1" and "%2" syntax in -cpp-command doesn't work if you > have not applied the patch at: > > http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2010-May/002073.html > > so perhaps the simplest solution overall would be to always > pre-process all your .c files as .i files yourself and invoke Frama-C > only on the .i files. > > Pascal > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100621/ca5a06b4/attachment.htm>