From 780b14de726f0da7516f8cc29b3c9ed7d39a8f23 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 30 Apr 2020 09:33:24 +0200
Subject: [PATCH] [devman] fix compilation of example script
---
doc/developer/examples/syntactic_check.ml | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/doc/developer/examples/syntactic_check.ml b/doc/developer/examples/syntactic_check.ml
index 7fd91ded169..74c141bde19 100644
--- a/doc/developer/examples/syntactic_check.ml
+++ b/doc/developer/examples/syntactic_check.ml
@@ -31,7 +31,7 @@ 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, _) ->
- let logic_denom = Logic_utils.expr_to_term ~cast:true 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
to attach it to the correct statement. The cil visitor maintains the
@@ -43,7 +43,7 @@ class non_zero_divisor prj = object (self)
| Kglobal -> assert false
| Kstmt s -> s
in
- let kf = Extlib.the self#current_kf in
+ let kf = Extlib.the self#current_kf in
(* The above statement and function are related to the original project. We
need to attach the new assertion to the corresponding statement and
function of the new project. Cil provides functions to convert a
--
GitLab