From d3f2c58234b9b01a8dc6976045372fc1f4915234 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Mon, 15 Apr 2024 14:20:43 +0200
Subject: [PATCH] [Cil] Support Relational and logical operators in
constFoldTerm
---
src/kernel_services/ast_queries/cil.ml | 18 +++++++++++++++++-
1 file changed, 17 insertions(+), 1 deletion(-)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 21881ba48f9..0dec5abfe91 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -5346,6 +5346,22 @@ let rec constFoldTermNodeAtTop = function
| BAnd -> constFoldTermBinOp Integer.logand
| BXor -> constFoldTermBinOp Integer.logxor
| BOr -> constFoldTermBinOp Integer.logor
+ | Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr ->
+ let bool_op = match op with
+ | Lt -> Integer.lt
+ | Gt -> Integer.gt
+ | Le -> Integer.le
+ | Ge -> Integer.ge
+ | Eq -> Integer.equal
+ | Ne -> (fun i1 i2 -> not (Integer.equal i1 i2))
+ | LAnd ->
+ (fun i1 i2 -> not (Integer.is_zero i1) && not (Integer.is_zero i2))
+ | LOr ->
+ (fun i1 i2 -> not (Integer.is_zero i1) || not (Integer.is_zero i2))
+ | _ -> assert false
+ in
+ constFoldTermBinOp
+ (fun i1 i2 -> if bool_op i1 i2 then Integer.one else Integer.zero)
| _ ->
TBinOp (op, {t1 with term_node = n1}, {t2 with term_node = n2})
end
@@ -5355,7 +5371,7 @@ let constFoldTerm t =
let visitor = object
inherit nopCilVisitor
method! vterm_node t =
- ChangeToPost (t,constFoldTermNodeAtTop)
+ ChangeToPost (t, constFoldTermNodeAtTop)
end
in
visitCilTerm visitor t
--
GitLab