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] Queries regarding WP plugin

Hello,
How can I get the flow of this tool? I mean which function is calling which
functions, from where the execution is starting and so on (profiling and
functional callgraph). I have searched for tools. I tried using ddd, gdb,
gnuprof, ocamldebug. For ddd/gdb/gnuprof generally the make is done with
cflags=<option>. Here these options are not working. According to the
makefile of frama-c ocamlviz can be used. I have installed ocamlviz and
tried modifying the makefile by setting USE_OCAMLVIZ_TOOL to yes (line no.
383 in Makefile). But it is giving me an error "Cannot find file
/home/d/lib/ocaml/libocamlviz.cma".

Debasmita Lohar
MS Student
Computer Science and Engineering
IIT Kharagpur


On Tue, Dec 16, 2014 at 2:05 PM, Lo?c Correnson <loic.correnson at cea.fr>
wrote:
>
> The standard way of using WP is for proving assertions, and more generally
> for proving Hoare triples.
> Frama-C/WP is optimized for that purpose, hence if some Hoare triple is
> trivial, then, we expect no proof obligation to be generated.
> However, if you want to obtain the weakest precondition of what *computes*
> a function, you can still use Frama-C/WP, but you must use a fake Hoare
> Triple that exhibit your needs.
> Continuing on your trivial, example you can introduce a ? model ? logic
> function that encapsulate your need:
>
> ```
> /*@ axiomatic WeakestPrecondition {
>        predicate OBSERVE(integer a,integer b);
>        }
> */
>
> /*@ ensures OBSERVE( x , \result ) ; */
> int f(int x)
> {
>  return x + 1;
> }
> ```
>
> Now using `frama-c -wp -wp-gen -wp-print`, you obtain the WP of f-return:
> ```
> Let x_0 = f_0-1.
> Assume { (* Domain *) Type: (is_sint32 f_0) /\ (is_sint32 x_0). }
> Prove: (P_OBSERVE x_0 f_0).
> ```
> which implicitly defines the relation OBSERVE, hence providing you with
> the WP of \result in terms of x.
>
> L.
>
>
>
>
> Le 16 d?c. 2014 ? 06:00, Debasmita Lohar <dlohar2009 at gmail.com> a ?crit :
>
> > Hello,
> > I have finally installed frama-c without any configuration error.
> > But I want to get initial weakest precondition of a
> program(simple/complicated). I did not find anything like this in frama-c
> (As for small programs it is not generating the proof obligations). I will
> look into why3. Thank you for your suggestion.
> >
> > Debasmita Lohar
> > MS Student
> > Computer Science and Engineering
> > IIT Kharagpur
> >
> >
> > On Mon, Dec 15, 2014 at 2:58 PM, David MENTRE <d.mentre at fr.merce.mee.com>
> wrote:
> > Hello,
> >
> > Le 08/12/2014 10:49, Debasmita Lohar a ?crit :
> > I am looking for a tool that computes weakest precondition of a program.
> >
> > Another option would be to use Why3 directly, instead of Frama-C.
> >
> > For example, on attached program, if you run:
> >   mkdir out
> >   why3 prove -o out -P alt-ergo compute.mlw
> >
> > Then in directory out/ you have generated VC:
> > """
> > $ tail -3 out/compute-Compute-WP_parameter_f.why
> > goal WP_parameter_f :
> >   (forall x:int. (((0 <= x) and (x <= 10)) -> ((1 <= (x + 1)) and
> >   ((x + 1) <= 11))))
> >
> > """
> >
> > Why3 can be found here: http://why3.lri.fr/
> >
> > There is also a dedicated mailing-list if you have questions.
> >
> > For sake of completness, SPARK 2014 also generates VCs in a subdirectory:
> >  http://www.spark-2014.org/
> >
> > Best regards,
> > david
> > --
> > David MENTR? - Research engineer, Ph.D.
> >   Formal Methods and tools
> > MITSUBISHI ELECTRIC R&D Centre Europe (MERCE)
> > Phone: +33 2 23 45 58 29 / Fax: +33 2 23 45 58 59
> > http://www.fr.mitsubishielectric-rce.eu
> >
> > _______________________________________________
> > 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
> > _______________________________________________
> > 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
>
> _______________________________________________
> 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/20141218/66a8698a/attachment.html>