From 2c5dfa53e7db8cf28af3766ed76564113403a473 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 29 Sep 2020 18:00:38 +0200
Subject: [PATCH] [logic] fixes translation of expr to boolean term or
predicate
---
src/kernel_services/ast_queries/logic_utils.ml | 12 ++++++------
1 file changed, 6 insertions(+), 6 deletions(-)
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 84f577652be..996cdc39184 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -512,9 +512,9 @@ and expr_to_boolean e =
let open Cil_types in
let tbool n = Logic_const.term n Logic_const.boolean_type in
match e.enode with
- | UnOp(BNot, a,_) ->
- tbool @@ TUnOp(BNot, expr_to_boolean a)
- | BinOp((BAnd|BOr) as op,a,b,_) ->
+ | UnOp(LNot, a,_) ->
+ tbool @@ TUnOp(LNot, expr_to_boolean a)
+ | BinOp((LAnd|LOr) as op,a,b,_) ->
let va = expr_to_boolean a in
let vb = expr_to_boolean b in
tbool @@ TBinOp(op,va,vb)
@@ -545,11 +545,11 @@ and expr_to_predicate e =
| BinOp(Ge, a, b, _) -> prel Rge a b
| BinOp(Eq, a, b, _) -> prel Req a b
| BinOp(Ne, a, b, _) -> prel Rneq a b
- | BinOp(BAnd, a, b, _) ->
+ | BinOp(LAnd, a, b, _) ->
unamed @@ Pand(expr_to_predicate a,expr_to_predicate b)
- | BinOp(BOr, a, b, _) ->
+ | BinOp(LOr, a, b, _) ->
unamed @@ Por(expr_to_predicate a,expr_to_predicate b)
- | UnOp(BNot, a, _) ->
+ | UnOp(LNot, a, _) ->
unamed @@ Pnot(expr_to_predicate a)
| _ ->
let t = expr_to_term ~coerce:true e in
--
GitLab