2021-01-22 20:02 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001089Frama-CDocumentation > manualspublic2016-06-21 14:20
Reporterboris 
Assigned Tosignoles 
PrioritynormalSeverityminorReproducibilityN/A
StatusclosedResolutionfixed 
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001089: Updated example in plugin-development-guide
DescriptionThe file attached is an updated version of example 5.14.7.
Additional InformationI'm unable to properly copy the comments in the guide with evince so I left them out.
TagsNo tags attached.
Attached Files
  • ? file icon ex-5-14-7.ml (1,342 bytes) 2012-02-09 14:21 -
    open Cil_types
    
    module Nonzero = Plugin.Register
      (struct
         let name = "Non zero divisor"
         let shortname = "nonzero"
         let help = "Demo plugin"
       end)
    
    module Enabled = Nonzero.False
      (struct
         let option_name = "-nonzero"
         let help = "Add assertion \"denominator is non-zero\" in expressions"
         let kind = `Correctness
       end)
    
    let the_stmt = function
      | Kstmt stmt -> stmt
      | Kglobal -> invalid_arg "Not a statement"
    
    class non_zero_divisor prj = object(self)
      inherit Visitor.generic_frama_c_visitor prj (Cil.copy_visit ())
      method vexpr e =
        begin match e.enode with
        | BinOp((Div|Mod), _, denom, _) ->
          let logic_denom = Logic_utils.expr_to_term ~cast:true denom in
          let assertion = Logic_const.prel (Rneq, logic_denom, Cil.lzero ()) in
          let stmt =  the_stmt self#current_kinstr in
          let new_kf = Cil.get_kernel_function (Cil.copy_visit ()) (Extlib.the self#current_kf) in
          Queue.add (fun () -> Annotations.add_assert new_kf stmt [Ast.self] assertion) self#get_filling_actions;
          Nonzero.feedback "Assertion added for expression %a in line %a\n" Cil.d_exp e Cil.d_loc (Cil.CurrentLoc.get ())
        | _ -> ()
        end;
        Cil.DoChildren
    end
    
    let main () =
      let _ = File.create_project_from_visitor "non zero divisor" (new non_zero_divisor) in
      ()
    
    let () = Db.Main.extend main
    
    ? file icon ex-5-14-7.ml (1,342 bytes) 2012-02-09 14:21 +

-Relationships
+Relationships

-Notes

~0003005

signoles (manager)

Thanks for your report and suggested patch.

~0004688

signoles (manager)

Fix committed to stable/neon branch.
+Notes

-Issue History
Date Modified Username Field Change
2012-02-09 14:21 boris New Issue
2012-02-09 14:21 boris Status new => assigned
2012-02-09 14:21 boris Assigned To => signoles
2012-02-09 14:21 boris File Added: ex-5-14-7.ml
2012-05-10 16:32 svn
2012-05-10 16:32 svn Status assigned => resolved
2012-05-10 16:32 svn Resolution open => fixed
2012-05-10 16:33 signoles Note Added: 0003005
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2013-12-19 01:11 signoles Source_changeset_attached => framac master f5ae4698
2014-02-12 16:54 signoles Source_changeset_attached => framac stable/neon f5ae4698
2014-02-12 16:58 signoles Note Added: 0004688
2014-02-12 16:58 signoles Status closed => resolved
2016-06-21 14:11 signoles Category Documentation => Documentation > ACSL
2016-06-21 14:20 signoles Category Documentation > ACSL => Documentation > manuals
+Issue History