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] New user questions

Mike,

Gui: you can invoke WP from the gui by right-clicking on the
function contract and then click on the "prove functions annotations by WP"
in the context menu that appears.  On a Mac, the equivalent to right click
is ctrl + click?

Different solvers:  I get the same result here on Alt-ergo 2.3.2 and z3
4.8.7.

[wp] 180 goals scheduled
[wp] [Cache] found:5, updated:42
[wp] Proved goals:  180 / 180
 Qed:           133  (0.78ms-29ms-699ms)
 Z3 4.8.7:       47  (10ms-254ms-5.2s) (cached: 5)

[wp] 180 goals scheduled
[wp] [Cache] found:5, updated:42
[wp] Proved goals:  180 / 180
 Qed:             133  (0.83ms-31ms-705ms)
 Alt-Ergo 2.3.2:   47  (8ms-36ms-133ms) (1259) (cached: 5)

Best,

Tim

On Fri, May 1, 2020 at 2:30 PM Whalen, Mike <mww at amazon.com> wrote:

> Hello,
>
>
>
>   My name is Mike Whalen and I work at Amazon.  I am looking at
> potentially using Frama-C for verification of some of the C code that we
> use.  I am working my way through the Frama-C WP tutorial for version 20.0
> (the March 30, 2020 edition).  I have a few questions related to
> installation, different solvers, and debugging.  I am running on Mac OS X
> 10.14.6.
>
>
>
> For installation, I can run the frama-c command line tool and the
> frama-c-gui, but I can’t invoke WP from within the GUI.  I can run WP from
> the command line and the proof goals are annotated properly, but the WP
> panel on the left side of the GUI does not provide a button to ‘prove’ as
> it does in the tutorial, as shown in the attached screen shot.  For the
> moment, I am making do with the command line tool.
>
>
>
> For different solvers, I get different answers from alt-ergo and z3 for
> the same properties, with z3 timing out or failing on a handful of goals
> that alt-ergo succeeds on.  I would expect differences in timeouts between
> solvers (e.g., one times out but not the other), but not discrepancies as
> to whether obligations are true or false.  Perhaps ‘failure’ in this case
> simply means ‘failure to prove’.  I am running z3 4.8.4 and alt-ergo
> 2.3.2.  I am attaching the .c and .h files.  The command lines are:
>
> frama-c -rte -wp -wp-prover z3 skip.c
>
> frama-c -rte -wp -wp-prover alt-ergo skip.c
>
>
>
> Finally, for debugging is there any kind of symbolic debugger or way to
> get counterexample information?  The VeriFast tool has a nice IDE where you
> can forward/back-step through a program with a symbolic heap.  At the
> moment, when a proof fails, I just stare hard at it and try to figure out
> how to fix it, but I would expect power-users have a few more things in
> their bag of tricks.  The WP tutorial did not have a lot of information on
> this aspect.
>
>
>
> Thank you very much for any help!  I am having fun with frama-c and look
> forward to learning how to use it effectively.
>
>
>
> Best regards,
>
>
>
> Mike
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss



-- 
Future planes will have one pilot and one dog in the cockpit. The pilot's
job will be to feed the dog. The dog's job will be to make sure the pilot
stays away from the instruments.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200502/050d6888/attachment.html>