--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on April 2011 ---
Hello! Thank you so much for your example! it helped narrow down the error possibilities! Now, the way we out the annotated file can't be the problem : we put your code instead of ours in the vspec method, and it worked! So we tried to make ours look exactly like yours, and the problem seems to come from the current_func...we seem to misuse this function. method vspec specc= ??? begin match self#current_func with ????? |Some fdec? -> ????????? synthesize the function's body cost, add it to a predicate => post_cond=>behavior=>spec; ? ? ? ? ? Format.printf "\n => EXPECTED \n"; ??? ? ? ? newSpecc.spec_behavior <- newBehavior::newSpecc.spec_behavior; ??? ? ? ? Cil.d_funspec Format.std_formatter newSpecc ;? ??? ? ? ? ChangeDoChildrenPost ( newSpecc ,fun x -> x) ????? |? _?? -> Format.printf "\n => UNEXPECTED \n" ; ?????????? (*the code you provided : *) ? ? ? ?? ? let post_cond = ??? ? ? ? ?? [Normal, Logic_const.new_predicate (Logic_const.ptrue)] ??? ? ? ?? in ??? ? ? ?? ? let spec = Cil.empty_funspec () in ??? ? ? ?? ? spec.spec_behavior <- [Cil.mk_behavior ~post_cond ()]; ???????????? Cil.d_funspec Format.std_formatter spec ; ??? ?? ? ? ? ChangeDoChildrenPost ( spec, fun x -> x) ??? end? ? We don't understand why, but the execution outs a file with ensures \true on every function (4 functions on the example), and an output that suggests 5 ensure \true clauses (five UNEXPECTED). Out of the 4 functions, only 3 are meant to be processed, and the expected pattern is indeed matched 3 times, and creates an ensure clause with the correct cost (49,295 and 1813 : three EXPECTED) ?=> UNEXPECTED ensures \true; ?=>UNEXPECTED ensures \true; ?=>EXPECTED ensures (_cost ? \old(_cost)+49U); ?=>UNEXPECTED ensures \true; ?=>EXPECTED ensures (_cost ? \old(_cost)+295U); ?=>UNEXPECTED ensures \true; ?=>EXPECTED ensures (_cost ? \old(_cost)+1813U); ?=>UNEXPECTED ensures \true; It seems like it's not connecting the functions with their specs... Thank you very much for your help! H. Zakaria Chihani. -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110421/b7906d7b/attachment.htm>