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