Commit 3382e0bd authored by Andre Maroneze's avatar Andre Maroneze 💬
Browse files

Merge branch 'fix/manual/visitor' into 'master'

[devman] fix visitor example following SO question

See merge request frama-c/frama-c!3882
parents f2d5f39a 5546f53d
......@@ -31,6 +31,12 @@ class non_zero_divisor prj = object (self)
(* A division is an expression: we override the vexpr method *)
method! vexpr e = match e.enode with
| BinOp((Div|Mod), _, denom, _) ->
(* denom might contain references to variables. Since we haven't visited
the node yet, they're bound to the varinfo of the original project.
we perform a plain copy, which will just ensure that they are replaced
with varinfos of the new project: frama_c_plain_copy is a visitor that
performs a copy, using the same correspondance tables as self. *)
let denom = Visitor.visitFramacExpr self#frama_c_plain_copy denom in
let logic_denom = Logic_utils.expr_to_term ~coerce:false denom in
let assertion = Logic_const.prel (Rneq, logic_denom, Cil.lzero ()) in
(* At this point, we have built the assertion we want to insert. It remains
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment