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
- Subject: [Frama-c-discuss] Visitor example in plugin-development guide
- From: virgile.prevosto at cea.fr (Virgile Prevosto)
- Date: Wed, 11 Jan 2012 10:33:53 +0100
- In-reply-to: <1326192880.2067.46.camel@iti27.informatik.htw-dresden.de>
- References: <1326192880.2067.46.camel@iti27.informatik.htw-dresden.de>
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
- Follow-Ups:
- [Frama-c-discuss] Visitor example in plugin-development guide
- From: hollas at informatik.htw-dresden.de (Boris Hollas)
- [Frama-c-discuss] Visitor example in plugin-development guide
- References:
- [Frama-c-discuss] Visitor example in plugin-development guide
- From: hollas at informatik.htw-dresden.de (Boris Hollas)
- [Frama-c-discuss] Visitor example in plugin-development guide
- Prev by Date: [Frama-c-discuss] New release of WP plug-in
- Next by Date: [Frama-c-discuss] Visitor example in plugin-development guide
- Previous by thread: [Frama-c-discuss] Visitor example in plugin-development guide
- Next by thread: [Frama-c-discuss] Visitor example in plugin-development guide
- Index(es):