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

[Frama-c-discuss] Using frama-c script to get proof obligations



Hi Julien,

I had already come to the same conclusion, but still thank you for the
clear answer. The folds you talk about are fold_requires, fold_assumes,
fold_ensures right? For example fold_requires, i am having a bit difficult
understanding the type:

val fold_requires : (Emitter.t -> Cil_types.identified_predicate
<./Cil_types.html#TYPEidentified_predicate> -> 'a -> 'a) ->
       Cil_types.kernel_function
<./Cil_types.html#TYPEkernel_function> -> string -> 'a -> 'a


I understand the Emmitter.t, Cil_types.identified_predicate, ('a -> 'a)
(fold accumulator) and kernel_function are to use inside the fold, but what
is the string? Stopage case?

More, inside the fold_requires i intend the use module Property and its
smart constructors to build the identified property lists, but most of them
require Cil_types.kinstr , what is this type? From what i found searching
the api the only way to get it is to use the module CilE with the function
current_stmt, is this correct?

If you or someone could help me with these doubts i would be very grateful.

Cheers,
Jos? Pinheiro


2014-06-11 11:43 GMT+01:00 SIGNOLES Julien <julien.signoles at cea.fr>:

>  Hello,
>
> The functions Annotations.fold_all_code_annot folds over code annotations,
> which are the annotations attached to statements (assertions, loop
> invariants, stmt contracts, etc). They do not include elements of function
> contracts like the ones defined in swap.c. I guess that is why you get no
> result. For instance, if you computes the RTE first (option -rte), your
> script correctly runs Alt-Ergo on the proof obligations corresponding to
> the generated assertions.
>
> The module Annotations also contains iterators/folders over the other kind
> of annotations (ensures, ...). You might have to use each of them...
>
> Hope this helps,
> Julien
>
>  ------------------------------
> *De :* Frama-c-discuss [frama-c-discuss-bounces at lists.gforge.inria.fr] de
> la part de Jos? Pinheiro [7jpinheiro at gmail.com]
> *Envoy? :* mardi 27 mai 2014 17:46
> *? :* frama-c-discuss at lists.gforge.inria.fr
> *Objet :* [Frama-c-discuss] Using frama-c script to get proof obligations
>
>   Hi all,
>
>  I am trying to develop a frama-c script that uses wp api to get a list
> of list of pos.
>
>  I am using Annotations.fold_all_code_annot and applying the
> function goals_of_property to get the proof obligations list, after i
> invoke wp_run() and a function that calls the prover on the annotations.
> The types all check correctly but when i use it it always returns me an
> empty list.
>
>  I think i am not invoking wp plugin correctly or not using
> fold_all_code_annot correctly.
>
>  If you could explain me what i am doing wrong i would be very grateful.
> I have tried to study wp plugin but there is little information about how
> you can use the api and only how to use the wp plugin itself, which is
> understandable due to be still in development.
>
>  In annex, i attach my script and the example i use as input.
>
>  Thanks in advance,
> Jos? Pinheiro
>
>
> _______________________________________________
> 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
>



-- 
Cumprimentos,
Jos? Pinheiro
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140611/6dd0564c/attachment-0001.html>