diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml index 4a40c63ae670c9ab399b715121cf18c27b954e7f..5d7b28b0c82a97af448d5b6e7c1e8c392ddb34cd 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 3dcd4013e17e4c1f302622a74a9d32860db5c993..5a8bd35caa31c3a9c990ecd4b123eab7163f4183 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