--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on January 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Visitor example in plugin-development guide



Hello Boris,

thanks for reporting this. Plugin development guide indeed contains some 
out-of-date sections. Unfortunately, we currently don't have that much 
time to fix this situation...

On 10/01/2012 11:54, Boris Hollas wrote:
> class non_zero_divisor prj = object(self)
> 	inherit Visitor.generic_frama_c_visitor prj (Cil.copy_visit ())
> 	method vexpr e = match e.enode with
> 		| BinOp((Div|Mod), _, denom, _) ->
> 			let t = Cil.typeOf denom in
> 			let logic_denom = Logic_const.term TCastE(t, Logic_utils.expr_to_term ~cast:true denom) (Ctype t)
> 			(* why not just
> 			   logic_denom = Logic_utils.expr_to_term ~cast:true denom
> 			*)

That's right, the cast will be inserted directly by expr_to_term if 
needed (with ~cast:true), there's no need to add one explicitly.

> 			in
> 			let assertion = Logic_const.prel (Rneq, logic_denom, Cil.lzero ()) in
> 			let stmt =  the_stmt self#current_kinstr in
> 			(* current_stmt is deprecated, so I changed this to current_kinstr. To extract the Kstmt part, is there a function similar to Extlib.the or do I have to provide my own the_stmt function? *)

There's currently no function to do that. One might be added in a later 
version in Cil_datatype.Kinstr (where there is already a 
kinstr_of_opt_stmt), but anyways, most functions should take a kinstr 
and not a stmt

> 			Queue.add (fun () -> Annotations.add_assert
> 				(* here, the guide says that the following line is incorrect since the new kernel function is not yet created. What to do? *)
> 				(Kernel_function.find_englobing_kf stmt)
>

Actually, since Nitrogen, you have access to the new kernel function, 
but not to Kernel_function.find_englobing_kf (At this very point, AST 
has been computed, but not the auxiliary tables necessary to compute 
this information). The proper way to retrieve the new kf is the following:

let new_kf = Cil.get_kernel_function (Extlib.the self#current_kf) in
Queue.add (fun () -> Annotations.add_assert new_kf ...)

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile