From 86d68aa9733fa63421f5185e5178e49968a62d16 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 22 Feb 2024 18:36:27 +0100
Subject: [PATCH] [clang2ir] if user wants to have useless casts in ACSL, do
 not remove them

---
 framaCIRGen_src/ACSLTermOrPredicate.cpp              | 2 --
 tests/basic/oracle/cxx_c_link.res.oracle             | 2 --
 tests/basic/oracle/placement_new.res.oracle          | 3 ++-
 tests/basic/oracle/placement_newb.res.oracle         | 3 ++-
 tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle | 3 ++-
 tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle  | 3 ++-
 tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle  | 3 ++-
 7 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/framaCIRGen_src/ACSLTermOrPredicate.cpp b/framaCIRGen_src/ACSLTermOrPredicate.cpp
index a6cf4d80..ed0baeef 100644
--- a/framaCIRGen_src/ACSLTermOrPredicate.cpp
+++ b/framaCIRGen_src/ACSLTermOrPredicate.cpp
@@ -596,8 +596,6 @@ TermOrPredicate::applyTermCast(logic_type& ccastType, term targument,
         && qualified_name_equal(ccastType->cons_logic_type.Lenum.name,
               ltype->cons_logic_type.Lenum.name))
       return targument;
-    if (!needLogicCast(ltype, ccastType))
-      return targument;
     term_node valueResult = term_node_TCastE(ccastType, targument);
     term result = term_cons(valueResult, copy_loc(targument->loc), NULL);
     ccastType = NULL;
diff --git a/tests/basic/oracle/cxx_c_link.res.oracle b/tests/basic/oracle/cxx_c_link.res.oracle
index 7c3e5ae8..247cba88 100644
--- a/tests/basic/oracle/cxx_c_link.res.oracle
+++ b/tests/basic/oracle/cxx_c_link.res.oracle
@@ -5,8 +5,6 @@ Now output intermediate result
   found two contracts. Merging them
 [kernel] FRAMAC_SHARE/libc/stdlib.h:330: Warning: 
   found two contracts. Merging them
-[kernel] FRAMAC_SHARE/libc/stdlib.h:724: Warning: 
-  found two contracts. Merging them
 /* Generated by Frama-C */
 #include "__fc_alloc_axiomatic.h"
 #include "stdlib.h"
diff --git a/tests/basic/oracle/placement_new.res.oracle b/tests/basic/oracle/placement_new.res.oracle
index 8e785619..7e1a1b55 100644
--- a/tests/basic/oracle/placement_new.res.oracle
+++ b/tests/basic/oracle/placement_new.res.oracle
@@ -1103,7 +1103,8 @@ size_t wcstombs(char * restrict s, wchar_t const * restrict pwcs, size_t n);
 /*@ requires valid_memptr: \valid(memptr);
     requires
       alignment_is_a_suitable_power_of_two:
-        alignment ≥ sizeof(void *) ∧ (alignment & alignment - 1) ≡ 0;
+        alignment ≥ sizeof(void *) ∧
+        ((size_t)alignment & (size_t)alignment - 1) ≡ 0;
     assigns __fc_heap_status, \result;
     assigns __fc_heap_status
       \from (indirect: alignment), size, __fc_heap_status;
diff --git a/tests/basic/oracle/placement_newb.res.oracle b/tests/basic/oracle/placement_newb.res.oracle
index af841f06..9a45df60 100644
--- a/tests/basic/oracle/placement_newb.res.oracle
+++ b/tests/basic/oracle/placement_newb.res.oracle
@@ -1072,7 +1072,8 @@ size_t wcstombs(char * restrict s, wchar_t const * restrict pwcs, size_t n);
 /*@ requires valid_memptr: \valid(memptr);
     requires
       alignment_is_a_suitable_power_of_two:
-        alignment ≥ sizeof(void *) ∧ (alignment & alignment - 1) ≡ 0;
+        alignment ≥ sizeof(void *) ∧
+        ((size_t)alignment & (size_t)alignment - 1) ≡ 0;
     assigns __fc_heap_status, \result;
     assigns __fc_heap_status
       \from (indirect: alignment), size, __fc_heap_status;
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
index e3995e53..769ed4ab 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
@@ -3199,7 +3199,8 @@ size_t wcstombs(char * restrict s, wchar_t const * restrict pwcs, size_t n);
 /*@ requires valid_memptr: \valid(memptr);
     requires
       alignment_is_a_suitable_power_of_two:
-        alignment ≥ sizeof(void *) ∧ (alignment & alignment - 1) ≡ 0;
+        alignment ≥ sizeof(void *) ∧
+        ((size_t)alignment & (size_t)alignment - 1) ≡ 0;
     assigns __fc_heap_status, \result;
     assigns __fc_heap_status
       \from (indirect: alignment), size, __fc_heap_status;
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
index 3ae6bb2e..7787be6b 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
@@ -2978,7 +2978,8 @@ size_t wcstombs(char * restrict s, wchar_t const * restrict pwcs, size_t n);
 /*@ requires valid_memptr: \valid(memptr);
     requires
       alignment_is_a_suitable_power_of_two:
-        alignment ≥ sizeof(void *) ∧ (alignment & alignment - 1) ≡ 0;
+        alignment ≥ sizeof(void *) ∧
+        ((size_t)alignment & (size_t)alignment - 1) ≡ 0;
     assigns __fc_heap_status, \result;
     assigns __fc_heap_status
       \from (indirect: alignment), size, __fc_heap_status;
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
index 023110e6..e86ef322 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
@@ -2984,7 +2984,8 @@ size_t wcstombs(char * restrict s, wchar_t const * restrict pwcs, size_t n);
 /*@ requires valid_memptr: \valid(memptr);
     requires
       alignment_is_a_suitable_power_of_two:
-        alignment ≥ sizeof(void *) ∧ (alignment & alignment - 1) ≡ 0;
+        alignment ≥ sizeof(void *) ∧
+        ((size_t)alignment & (size_t)alignment - 1) ≡ 0;
     assigns __fc_heap_status, \result;
     assigns __fc_heap_status
       \from (indirect: alignment), size, __fc_heap_status;
-- 
GitLab