--- layout: fc_discuss_archives title: Message 43 from Frama-C-discuss on June 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem running frama-c in Windows



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>