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