--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on June 2014 ---
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>