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

  • Subject: [Frama-c-discuss] Using frama-c script to get proof obligations
  • From: julien.signoles at cea.fr (SIGNOLES Julien)
  • Date: Wed, 11 Jun 2014 10:43:07 +0000
  • In-reply-to: <CAM1QBJONYOzVxGpeid81KJ_YVnbAzWpcQ5b206eMuH31OPOOZA@mail.gmail.com>
  • References: <CAM1QBJONYOzVxGpeid81KJ_YVnbAzWpcQ5b206eMuH31OPOOZA@mail.gmail.com>
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

-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? nettoy?e...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140611/c8740371/attachment.html>