Tests update

src/plugins/e-acsl/share/e-acsl/e_acsl_floating_point.h

@@ -52,8 +52,6 @@
 double math_HUGE_VAL = 0.0;
 /** \brief Positive infinity for floats: same as HUGE_VALF */
 float  math_HUGE_VALF = 0.0;
-/** \brief Positive infinity for long doubles: same as HUGE_VALL */
-long double math_HUGE_VALL = 0.0;
 /** \brief Representation of infinity value for doubles: same as INFINITY */
 double math_INFINITY = 0.0;
 
@@ -61,7 +59,6 @@ double math_INFINITY = 0.0;
 static void init_infinity_values() {
   math_HUGE_VAL = HUGE_VAL;
   math_HUGE_VALF = HUGE_VALF;
-  math_HUGE_VALL = HUGE_VALL;
   math_INFINITY = INFINITY;
 }
 

src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h

@@ -78,7 +78,6 @@
 /* Infinity values for floating point types */
 #define math_HUGE_VAL                   export_alias(math_HUGE_VAL)
 #define math_HUGE_VALF                  export_alias(math_HUGE_VALF)
-#define math_HUGE_VALL                  export_alias(math_HUGE_VALL)
 #define math_INFINITY                   export_alias(math_INFINITY)
 
 /******************************/
@@ -310,9 +309,6 @@ extern double math_HUGE_VAL
 /* Positive infinity for floats: same as HUGE_VALF */
 extern float  math_HUGE_VALF
   __attribute__((FC_BUILTIN));
-/* Positive infinity for long doubles: same as HUGE_VALL */
-extern long double math_HUGE_VALL
-  __attribute__((FC_BUILTIN));
 /* Representation of infinity value for doubles: same as INFINITY */
 extern double math_INFINITY
   __attribute__((FC_BUILTIN));

src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle

 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 tests/bts/bts1304.i:23:[value] warning: assertion got status unknown.
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:90:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.

src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle

@@ -4,5 +4,5 @@ tests/bts/bts1307.i:23:[e-acsl] warning: approximating a real number by a float
 tests/bts/bts1307.i:23:[e-acsl] warning: approximating a real number by a float
 tests/bts/bts1307.i:11:[e-acsl] warning: approximating a real number by a float
 [e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:90:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
 [value] user error: type long double not implemented. Using double instead

src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle

 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:90:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.

src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle

 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:90:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.

src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle

 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:90:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
 tests/bts/bts1390.c:13:[value] warning: function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 tests/bts/bts1390.c:13:[value] warning: function __gen_e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 tests/bts/bts1390.c:18:[value] warning: out of bounds read. assert \valid_read(s);

src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle

 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:90:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.

src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle

 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:90:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.

src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle

 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:90:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.

src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle

 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:90:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.

src/plugins/e-acsl/tests/bts/oracle/bts1718.res.oracle

 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:90:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.

src/plugins/e-acsl/tests/bts/oracle/bts1740.res.oracle

 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:90:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
 tests/bts/bts1740.i:12:[value] warning: locals {a} escaping the scope of a block of main through p
 tests/bts/bts1740.i:16:[value] warning: accessing left-value that contains escaping addresses.
                  assert ¬\dangling(&p);

src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle

 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:90:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
 tests/bts/bts1837.i:18:[value] warning: signed overflow. assert -2147483648 ≤ i - 1;

src/plugins/e-acsl/tests/bts/oracle/bts2191.res.oracle

 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:90:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.

src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle

@@ -3,4 +3,4 @@
                   the generated program may miss memory instrumentation
                   if there are memory-related annotations.
 [e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:90:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.

src/plugins/e-acsl/tests/bts/oracle/bts2231.res.oracle

 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 tests/bts/bts2231.i:8:[value] warning: signed overflow. assert -9223372036854775808 ≤ __gen_e_acsl__2 - 1;
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:90:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.

src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle

@@ -2,5 +2,5 @@ tests/bts/bts2252.c:22:[kernel] warning: Calling undeclared function strncpy. Ol
 [e-acsl] beginning translation.
 tests/bts/bts2252.c:22:[kernel] warning: Neither code nor specification for function strncpy, generating default assigns from the prototype
 [e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:90:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
 tests/bts/bts2252.c:17:[value] warning: out of bounds read. assert \valid_read(srcbuf + i);

src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle

@@ -13,12 +13,15 @@
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
   __e_acsl_heap_allocation_size ∈ [--..--]
+  __e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+  __e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+  __e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
 [value] using specification for function __e_acsl_memory_init
 [value] using specification for function __e_acsl_store_block
 [value] using specification for function __e_acsl_full_init
 [value] using specification for function __e_acsl_initialized
 [value] using specification for function __e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:90:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
 [value] using specification for function __e_acsl_delete_block
 [value] using specification for function __e_acsl_memory_clean
 [value] done for function main

src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle

@@ -13,12 +13,15 @@
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
   __e_acsl_heap_allocation_size ∈ [--..--]
+  __e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+  __e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+  __e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
 [value] using specification for function __e_acsl_memory_init
 [value] using specification for function __e_acsl_store_block
 [value] using specification for function __e_acsl_full_init
 [value] using specification for function __e_acsl_initialized
 [value] using specification for function __e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:90:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
 [value] using specification for function __e_acsl_delete_block
 [value] using specification for function __e_acsl_memory_clean
 [value] done for function main