--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on April 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem with current_func



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>