--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on January 2012 ---
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