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] 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