diff --git a/framaCIRGen_src/ACSLTermOrPredicate.cpp b/framaCIRGen_src/ACSLTermOrPredicate.cpp index a6cf4d80618e82ad2e544ebd22ffedf3a4261851..ed0baeefa0ecfdccf4cc362e1829ad898351d956 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 7c3e5ae806e003a0c81ca213acdd852d6abcc7b1..247cba88b6d18fc5841e8a3f93ec8b1d9ed6194e 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 8e785619e41f3c46faab9b3b5e597dacf448fadb..7e1a1b5555b633a20a637213b53ad36e2e995df5 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 af841f06fa63c5980ce77f2925d0adc9c8e1b3b8..9a45df60bf414465446e3b3f8936b0cc0f519fdb 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 e3995e5325a07bd0570ddacd3d4f292d0fd43c1c..769ed4ab3a1da2b8bc8a5cac2e56d358ff028386 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 3ae6bb2e7d56a3472704bda3c8c0d331aec754e9..7787be6ba39f85775f88784540c6d6a84729b522 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 023110e6eff45e3285659dde04035016c7862895..e86ef322294f9b0b67701a27aec44f440580f4f2 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;