--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on April 2011 ---
[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>