From c76015a86c1f3b44bccf41c121aeddcb8117edb2 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 21 Feb 2024 19:28:54 +0100
Subject: [PATCH] [kernel] improve now-unified TCast handling
---
src/kernel_services/ast_queries/cil.ml | 6 +++---
src/kernel_services/ast_queries/logic_utils.ml | 4 ++--
2 files changed, 5 insertions(+), 5 deletions(-)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 4a40c63ae67..5d7b28b0c82 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -3187,14 +3187,14 @@ let isZero (e: exp) : bool =
let rec isLogicZero t = match t.term_node with
| TConst (Integer (n,_)) -> Integer.equal n Integer.zero
| TConst (LChr c) -> Char.code c = 0
- | TCast(false, _, t) -> isLogicZero t
+ | TCast(_, _, t) -> isLogicZero t
| _ -> false
let isLogicNull t =
isLogicZero t ||
(let rec aux t = match t.term_node with
| Tnull -> true
- | TCast(false,_, t) -> aux t
+ | TCast(_,_, t) -> aux t
| _ -> false
in aux t)
@@ -3462,7 +3462,7 @@ let rec stripCasts (e: exp) =
match e.enode with CastE(_, e') -> stripCasts e' | _ -> e
let rec stripTermCasts (t: term) =
- match t.term_node with TCast(false,_, t') -> stripTermCasts t' | _ -> t
+ match t.term_node with TCast(_,_, t') -> stripTermCasts t' | _ -> t
(* Separate out the storage-modifier name attributes *)
let separateStorageModifiers (al: attribute list) =
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 3dcd4013e17..5a8bd35caa3 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -1747,6 +1747,8 @@ let rec compare_term t1 t2 =
if res = 0 then compare_term t1 t2 else res
| TCast (false,_,_), _ -> 1
| _, TCast (false,_,_) -> -1
+ | TCast(true,_,_), _ -> 1
+ | _, TCast(true,_,_) -> -1
| TAddrOf l1, TAddrOf l2 -> compare_tlval l1 l2
| TAddrOf _, _ -> 1
| _, TAddrOf _ -> -1
@@ -1835,8 +1837,6 @@ let rec compare_term t1 t2 =
| Tlet(d1,b1), Tlet(d2,b2) ->
let res = compare_logic_info d1 d2 in
if res = 0 then compare_term b1 b2 else res
- | Tlet _, _ -> 1
- | _, Tlet _ -> -1
and compare_logic_info l1 l2 =
let res = compare_logic_signature l1 l2 in
--
GitLab