Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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>