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 current_func

  • Subject: [Frama-c-discuss] Problem with current_func
  • From: uaz11 at yahoo.fr (zakaria chihani)
  • Date: Thu, 21 Apr 2011 12:50:42 +0100 (BST)
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>