[tests] simplify bts directory as well

src/plugins/e-acsl/tests/bts/bts1304.i

 /* run.config
    COMMENT: argument of functions must be kept, so keep its parameter
-   EXECNOW: LOG gen_bts1304.c BIN gen_bts1304.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1304.i -constfold -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1304.c > /dev/null && ./gcc_bts.sh bts1304
-   EXECNOW: LOG gen_bts13042.c BIN gen_bts13042.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1304.i -constfold -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13042.c > /dev/null && ./gcc_bts.sh bts13042
+   COMMENT: no diff
+   COMMENT: no diff
 */
 
 struct msgA { int type; int a[2]; };

src/plugins/e-acsl/tests/bts/bts1307.i

 /* run.config
    COMMENT: spec with floats and reals
-   EXECNOW: LOG gen_bts1307.c BIN gen_bts1307.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1307.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1307.c > /dev/null && ./gcc_bts.sh bts1307
-   EXECNOW: LOG gen_bts13072.c BIN gen_bts13072.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1307.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13072.c > /dev/null && ./gcc_bts.sh bts13072
+   COMMENT: no diff
+   COMMENT: no diff
 */
 
 /*@ requires \valid(Mtmax_in);

src/plugins/e-acsl/tests/bts/bts1324.i

 /* run.config
    COMMENT: fixed bug with typing of universal quantification
-   EXECNOW: LOG gen_bts1324.c BIN gen_bts1324.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1324.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1324.c > /dev/null && ./gcc_bts.sh bts1324
-   EXECNOW: LOG gen_bts13242.c BIN gen_bts13242.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1324.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13242.c > /dev/null && ./gcc_bts.sh bts13242
+   COMMENT: no diff
+   COMMENT: no diff
 */
 
 /*@ behavior yes:

src/plugins/e-acsl/tests/bts/bts1326.i

 /* run.config
    COMMENT: complex term left-values
-   EXECNOW: LOG gen_bts1326.c BIN gen_bts1326.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1326.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1326.c > /dev/null && ./gcc_bts.sh bts1326
-   EXECNOW: LOG gen_bts13262.c BIN gen_bts13262.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1326.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13262.c > /dev/null && ./gcc_bts.sh bts13262
+   COMMENT: no diff
+   COMMENT: no diff
 */
 
 typedef int ArrayInt[5];

src/plugins/e-acsl/tests/bts/bts1390.c

 /* run.config
    COMMENT: bts #1390, issue with typing of quantified variables
-   STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\""
-   EXECNOW: LOG gen_bts1390.c BIN gen_bts1390.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1390.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1390.c > /dev/null && ./gcc_bts.sh bts1390
-   EXECNOW: LOG gen_bts13902.c BIN gen_bts13902.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1390.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13902.c > /dev/null && ./gcc_bts.sh bts13902
+   COMMENT: no diff
+   COMMENT: no diff
+   COMMENT: no diff
 */
 
 #include "stdlib.h"

src/plugins/e-acsl/tests/bts/bts1398.c

 /* run.config
    COMMENT: variadic function call
-   STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\""
-   EXECNOW: LOG gen_bts1398.c BIN gen_bts1398.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1398.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1398.c > /dev/null && ./gcc_bts.sh bts1398 > /dev/null
-   EXECNOW: LOG gen_bts13982.c BIN gen_bts13982.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1398.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13982.c > /dev/null && ./gcc_bts.sh bts13982 > /dev/null
+   COMMENT: no diff
+   COMMENT: no diff
+   COMMENT: no diff
 */
 
 #include "stdio.h"

src/plugins/e-acsl/tests/bts/bts1399.c

 /* run.config
    COMMENT: complex fields and indexes + potential RTE in \initialized
-   STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
-   EXECNOW: LOG gen_bts1399.c BIN gen_bts1399.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1399.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1399.c > /dev/null && ./gcc_bts.sh bts1399
-   EXECNOW: LOG gen_bts13992.c BIN gen_bts13992.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1399.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13992.c > /dev/null && ./gcc_bts.sh bts13992
+   STDOPT: +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
+   COMMENT: no diff
+   COMMENT: no diff
 */
 
 #include "stdlib.h"

src/plugins/e-acsl/tests/bts/bts1478.c

 /* run.config
    COMMENT: bts #1478 about wrong detection of initializers in pre-analysis
-   EXECNOW: LOG gen_bts1478.c BIN gen_bts1478.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1478.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1478.c > /dev/null && ./gcc_bts.sh bts1478
-   EXECNOW: LOG gen_bts14782.c BIN gen_bts14782.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1478.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts14782.c > /dev/null && ./gcc_bts.sh bts14782
+   COMMENT: no diff
+   COMMENT: no diff
 */
 
 int global_i;

src/plugins/e-acsl/tests/bts/bts1700.i

 /* run.config
    COMMENT: pointer to an empty struct
-   EXECNOW: LOG gen_bts1700.c BIN gen_bts1700.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1700.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1700.c > /dev/null && ./gcc_bts.sh bts1700
+   COMMENT: no diff
 */
 
 struct toto {};

src/plugins/e-acsl/tests/bts/bts1717.i

 /* run.config
    COMMENT: bts #1717, issue with labels on memory-related statements
-   STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\""
-   EXECNOW: LOG gen_bts1717.c BIN gen_bts1717.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1717.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1717.c > /dev/null && ./gcc_bts.sh bts1717
-   EXECNOW: LOG gen_bts17172.c BIN gen_bts17172.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1717.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts17172.c > /dev/null && ./gcc_bts.sh bts17172
+   COMMENT: no diff
+   COMMENT: no diff
+   COMMENT: no diff
 */
 
 int main(void) {

src/plugins/e-acsl/tests/bts/bts1718.i

 /* run.config
    COMMENT: bts #1718, issue regarding incorrect initialization of literal strings in global arrays with compound initializers
-   STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\""
-   EXECNOW: LOG gen_bts1718.c BIN gen_bts1718.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1718.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1718.c > /dev/null && ./gcc_bts.sh bts1718
-   EXECNOW: LOG gen_bts17182.c BIN gen_bts17182.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1718.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts17182.c > /dev/null && ./gcc_bts.sh bts17182
+   COMMENT: no diff
+   COMMENT: no diff
+   COMMENT: no diff
 */
 
 int main(void) {

src/plugins/e-acsl/tests/bts/bts1837.i

 /* run.config
    COMMENT: bts #1837, about initialization of literal strings
-   EXECNOW: LOG gen_bts1837.c BIN gen_bts1837.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1837.i -e-acsl -then-last -print -ocode ./tests/bts/result/gen_bts1837.c > /dev/null && ./gcc_bts.sh bts1837
+   COMMENT: no diff
 */
 
 char *S = "foo";

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

-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value] Values of globals at initialization
-  __fc_random_counter ∈ {0}
-  __fc_rand_max ∈ {32767}
-  __fc_heap_status ∈ [--..--]
-  __e_acsl_init ∈ [--..--]
-  __e_acsl_internal_heap ∈ [--..--]
-  __memory_size ∈ [--..--]
-[value] using specification for function __store_block
-tests/bts/bts1304.i:23:[value] entering loop for the first time
-[value] using specification for function __initialize
-[value] using specification for function __delete_block
-tests/bts/bts1304.i:25:[value] warning: assertion got status unknown.
-[value] using specification for function __initialized
-[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
-[value] using specification for function __e_acsl_memory_clean
-[value] done for function main

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

-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value] Values of globals at initialization
-  __fc_random_counter ∈ {0}
-  __fc_rand_max ∈ {32767}
-  __fc_heap_status ∈ [--..--]
-  __e_acsl_init ∈ [--..--]
-  __e_acsl_internal_heap ∈ [--..--]
-  __memory_size ∈ [--..--]
-[value] using specification for function __store_block
-tests/bts/bts1304.i:23:[value] entering loop for the first time
-[value] using specification for function __initialize
-[value] using specification for function __delete_block
-tests/bts/bts1304.i:25:[value] warning: assertion got status unknown.
-[value] using specification for function __initialized
-[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
-[value] using specification for function __e_acsl_memory_clean
-[value] done for function main

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

-[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1304.i (no preprocessing)
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
   __memory_size ∈ [--..--]
 [value] using specification for function __store_block
-tests/e-acsl-runtime/bts1304.i:23:[value] entering loop for the first time
+tests/bts/bts1304.i:23:[value] entering loop for the first time
 [value] using specification for function __initialize
 [value] using specification for function __delete_block
-tests/e-acsl-runtime/bts1304.i:25:[value] Assertion got status unknown.
+tests/bts/bts1304.i:25:[value] warning: assertion got status unknown.
 [value] using specification for function __initialized
 [value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
 [value] using specification for function __e_acsl_memory_clean
 [value] done for function main
-[value] ====== VALUES COMPUTED ======

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

-tests/bts/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
-[e-acsl] beginning translation.
-tests/bts/bts1307.i:13:[e-acsl] warning: approximating a real number by a float
-tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
-tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value] Values of globals at initialization
-  __fc_random_counter ∈ {0}
-  __fc_rand_max ∈ {32767}
-  __fc_heap_status ∈ [--..--]
-  __e_acsl_init ∈ [--..--]
-  __e_acsl_internal_heap ∈ [--..--]
-  __memory_size ∈ [--..--]
-[value] using specification for function __store_block
-[value] using specification for function __full_init
-[value] using specification for function __valid
-[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
-[value] using specification for function __initialize
-[value] using specification for function __delete_block
-[value] using specification for function __valid_read
-[value] user error: type long double not implemented. Using double instead
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status invalid.
-[value] done for function main

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

-tests/bts/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
-[e-acsl] beginning translation.
-tests/bts/bts1307.i:13:[e-acsl] warning: approximating a real number by a float
-tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
-tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value] Values of globals at initialization
-  __fc_random_counter ∈ {0}
-  __fc_rand_max ∈ {32767}
-  __fc_heap_status ∈ [--..--]
-  __e_acsl_init ∈ [--..--]
-  __e_acsl_internal_heap ∈ [--..--]
-  __memory_size ∈ [--..--]
-[value] using specification for function __store_block
-[value] using specification for function __full_init
-[value] using specification for function __valid
-[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
-[value] using specification for function __initialize
-[value] using specification for function __delete_block
-[value] using specification for function __gmpz_init_set_si
-[value] using specification for function __gmpz_cmp
-[value] using specification for function __gmpz_init
-[value] using specification for function __gmpz_tdiv_q
-[value] using specification for function __gmpz_get_ui
-[value] using specification for function __valid_read
-[value] user error: type long double not implemented. Using double instead
-[value] using specification for function __gmpz_clear
-tests/bts/bts1307.i:25:[value] warning: function bar, behavior UnderEstimate_Motoring: postcondition got status unknown.
-tests/bts/bts1307.i:25:[value] warning: function __e_acsl_bar, behavior UnderEstimate_Motoring: postcondition got status unknown.
-[value] using specification for function __e_acsl_memory_clean
-[value] done for function main

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

-[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1307.i (no preprocessing)
-tests/e-acsl-runtime/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
+tests/bts/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
 [e-acsl] beginning translation.
-tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating a real number by a float
-tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
-tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
+tests/bts/bts1307.i:13:[e-acsl] warning: approximating a real number by a float
+tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
+tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
   __memory_size ∈ [--..--]
 [value] using specification for function __store_block
 [value] using specification for function __full_init
-tests/e-acsl-runtime/bts1307.i:7:[value] Function __e_acsl_foo: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:8:[value] Function __e_acsl_foo: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:9:[value] Function __e_acsl_foo: precondition got status valid.
 [value] using specification for function __valid
 [value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/bts1307.i:7:[value] Function foo: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:8:[value] Function foo: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:9:[value] Function foo: precondition got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
 [value] using specification for function __initialize
 [value] using specification for function __delete_block
-tests/e-acsl-runtime/bts1307.i:13:[value] Function foo, behavior OverEstimate_Motoring: postcondition got status valid.
 [value] using specification for function __valid_read
 [value] user error: type long double not implemented. Using double instead
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status invalid.
-tests/e-acsl-runtime/bts1307.i:13:[value] Function __e_acsl_foo, behavior OverEstimate_Motoring: no state left in which to evaluate postcondition, status not computed.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status invalid.
 [value] done for function main
-[value] ====== VALUES COMPUTED ======

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

-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value] Values of globals at initialization
-  __fc_random_counter ∈ {0}
-  __fc_rand_max ∈ {32767}
-  __fc_heap_status ∈ [--..--]
-  __e_acsl_init ∈ [--..--]
-  __e_acsl_internal_heap ∈ [--..--]
-  __memory_size ∈ [--..--]
-[value] using specification for function __store_block
-[value] using specification for function __initialize
-[value] using specification for function __gmpz_init
-[value] using specification for function __gmpz_init_set_si
-[value] using specification for function __gmpz_add
-[value] using specification for function __gmpz_set
-[value] using specification for function __gmpz_clear
-tests/bts/bts1324.i:8:[value] entering loop for the first time
-[value] using specification for function __gmpz_cmp
-[value] using specification for function __gmpz_sub
-[value] using specification for function __gmpz_get_ui
-tests/bts/bts1324.i:8:[kernel] warning: out of bounds read. assert \valid_read(t+__e_acsl_2);
-tests/bts/bts1324.i:8:[kernel] warning: out of bounds read. assert \valid_read(t+__e_acsl_i_2);
-tests/bts/bts1324.i:15:[value] entering loop for the first time
-[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
-[value] using specification for function __delete_block
-[value] using specification for function __e_acsl_memory_clean
-[value] done for function main