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] Problem with the ChangeDoChildrenPost (bis)

Hello,

Le ven. 15 avril 2011 12:28:06 CEST,
zakaria chihani <uaz11 at yahoo.fr> a ?crit :

> We overrode vspec as you advised, but we still don't get it on the outed file.
> We tried printing the result with the cil.d_funspec, which works perfectly...
> 

Well, your code seems pretty alright. For what it's worth, here is a
small script that will put an ensures \true; clause to each function
(and in fact replace any statement contract by the same clause), usable
with frama-c -load-script test.ml file.c
The only minor difference with the code you're showing us is that 
you use explicitly Project.on, while you can directly
give File.pretty_ast a ~prj argument, but this shouldn't make any
difference. Similarly, you could use the ~fmt argument of pretty_ast
instead of setting CodeOutput by hand (but again, this has nothing to
do with your issue).
A possibility would be that on the examples you tried, the funspec
degenerate to trivial ones (in the sense of Cil.is_empty_funspec), that
are not pretty-printed. Otherwise, I'm afraid that we'll need to see a
bit more code to investigate precisely what is going on.

Best regards,
-- 
Virgile Prevosto
Ing?nieur-Chercheur, CEA, LIST
Laboratoire de S?ret? des Logiciels
+33/0 1 69 08 82 98
-------------- section suivante --------------
Une pi?ce jointe autre que texte a ?t? nettoy?e...
Nom: test.ml
Type: text/x-ocaml
Taille: 518 octets
Desc: non disponible
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110419/07e80e1d/attachment.bin>