From 91fe6e38ff8e3b18ff8fda37d3efff87218f8075 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 30 Sep 2020 09:50:57 +0200
Subject: [PATCH] [logic] clarify expr-to-boolean for comparisons
---
src/kernel_services/ast_queries/logic_utils.ml | 9 ++++++++-
1 file changed, 8 insertions(+), 1 deletion(-)
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 996cdc39184..da322b0787c 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -413,6 +413,13 @@ let is_boolean_binop op =
| PlusA | PlusPI | IndexPI | MinusA | MinusPI | MinusPP
| Mult | Div | Mod | Shiftlt | Shiftrt | BAnd | BXor | BOr -> false
+let is_comparison_binop op =
+ let open Cil_types in
+ match op with
+ | Lt | Gt | Le | Ge | Eq | Ne -> true
+ | PlusA | PlusPI | IndexPI | MinusA | MinusPI | MinusPP
+ | Mult | Div | Mod | Shiftlt | Shiftrt | BAnd | BXor | BOr | LAnd | LOr -> false
+
let float_builtin prefix fkind =
let name = match fkind with
| FFloat -> Printf.sprintf "\\%s_float" prefix
@@ -518,7 +525,7 @@ and expr_to_boolean e =
let va = expr_to_boolean a in
let vb = expr_to_boolean b in
tbool @@ TBinOp(op,va,vb)
- | BinOp(op, a, b, _) when is_boolean_binop op ->
+ | BinOp(op, a, b, _) when is_comparison_binop op ->
let va = expr_to_term ~coerce:true a in
let vb = expr_to_term ~coerce:true b in
tbool @@ TBinOp(op,va,vb)
--
GitLab