diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle index 343190f2f5b574b50236b8e2a4ceadb1550e60c2..f4cf8ba21c74dd2533c6cb899f740f73630c374b 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle @@ -1,11 +1,3 @@ -[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/bts/bts1304.i (no preprocessing) [e-acsl] beginning translation. [e-acsl] translation done in project "e-acsl". [value] Analyzing a complete application starting at main @@ -28,4 +20,3 @@ tests/bts/bts1304.i:25:[value] Assertion got status unknown. FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] 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 ====== diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle index 838283a10e040746acee53e01273e1207ed3871e..2a6424a798ceeaacc82c3fee110c0734bd1243ae 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle @@ -1,11 +1,3 @@ -[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/bts/bts1307.i (no preprocessing) 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 @@ -41,4 +33,3 @@ tests/bts/bts1307.i:13:[value] Function foo, behavior OverEstimate_Motoring: pos FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status invalid. tests/bts/bts1307.i:13:[value] Function __e_acsl_foo, behavior OverEstimate_Motoring: no state left in which to evaluate postcondition, status not computed. [value] done for function main -[value] ====== VALUES COMPUTED ====== diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle index 22f38a1f1f17bc57b72f89fdb3eaabe3873139cf..36fc1092d18368c622a6f08793670231c7a92de4 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle @@ -1,11 +1,3 @@ -[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/bts/bts1324.i (no preprocessing) [e-acsl] beginning translation. [e-acsl] translation done in project "e-acsl". [value] Analyzing a complete application starting at main @@ -32,4 +24,3 @@ tests/bts/bts1324.i:9:[value] Function __e_acsl_sorted, behavior yes: postcondit tests/bts/bts1324.i:25:[value] Assertion got status valid. [value] using specification for function __e_acsl_memory_clean [value] done for function main -[value] ====== VALUES COMPUTED ====== diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle index af73383a57f2ef56b37be39c85120145d8c62049..7583cbd29fde586a13012f6a653d05780fb3c8e1 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle @@ -1,11 +1,3 @@ -[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/bts/bts1326.i (no preprocessing) [e-acsl] beginning translation. [e-acsl] translation done in project "e-acsl". [value] Analyzing a complete application starting at main @@ -29,4 +21,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got tests/bts/bts1326.i:10:[value] Function __e_acsl_atp_NORMAL_computeAverageAccel: postcondition got status valid. [value] using specification for function __e_acsl_memory_clean [value] done for function main -[value] ====== VALUES COMPUTED ====== diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle index 9a7fea6d52e7d00cbf366222993676c7e34d2f04..c98c0cb1cddef9e7b2a720bc1bddfc602e613f5c 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle @@ -1,11 +1,3 @@ -[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/bts/bts1390.c (with preprocessing) [e-acsl] beginning translation. [e-acsl] translation done in project "e-acsl". [value] Analyzing a complete application starting at main @@ -62,4 +54,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got tests/bts/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.) [value] using specification for function __e_acsl_memory_clean [value] done for function main -[value] ====== VALUES COMPUTED ====== diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle index 704fb9ba63ce5895925e3965a6c624fd464b3479..1b7e2835fd507fc263bd5ee3d24808d9f38adbe9 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle @@ -1,11 +1,3 @@ -[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/bts/bts1398.c (with preprocessing) [e-acsl] beginning translation. [e-acsl] translation done in project "e-acsl". [value] Analyzing a complete application starting at main @@ -47,4 +39,3 @@ [value] using specification for function __literal_string [value] using specification for function printf [value] done for function main -[value] ====== VALUES COMPUTED ====== diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle index 3bd71436ad9edcf5572903db4e2ecb8781881330..45341f00fdce9f3ff60dfdfda2f7a1eaff2a82c4 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle @@ -1,11 +1,3 @@ -[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/bts/bts1399.c (with preprocessing) [e-acsl] beginning translation. FRAMAC_SHARE/libc/stdlib.h:185:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:185:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation. @@ -65,4 +57,3 @@ FRAMAC_SHARE/libc/stdlib.h:175:[value] Function __e_acsl_free, behavior dealloca FRAMAC_SHARE/libc/stdlib.h:177:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown. [value] using specification for function __e_acsl_memory_clean [value] done for function main -[value] ====== VALUES COMPUTED ====== diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle index 6e5736c4a8f37d9bf94e1680244a052957112759..aa1818323b885df4bef5089b233f1d6ee3323ecc 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle @@ -1,11 +1,3 @@ -[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/bts/bts1478.c (with preprocessing) [e-acsl] beginning translation. [e-acsl] translation done in project "e-acsl". [value] Analyzing a complete application starting at main @@ -35,4 +27,3 @@ tests/bts/bts1478.c:13:[value] Function loop: precondition got status valid. [value] using specification for function __delete_block [value] using specification for function __e_acsl_memory_clean [value] done for function main -[value] ====== VALUES COMPUTED ====== diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle index 323e2e9c16b5fd1bf62774d3e24be9bf7d272746..282bf108a6571145fd47e12a50b5b6f3908414dc 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle @@ -1,11 +1,3 @@ -[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/bts/bts1700.i (no preprocessing) [e-acsl] beginning translation. [e-acsl] translation done in project "e-acsl". [value] Analyzing a complete application starting at main @@ -29,4 +21,3 @@ tests/bts/bts1700.i:13:[value] Assertion got status unknown. [value] using specification for function __delete_block [value] using specification for function __e_acsl_memory_clean [value] done for function main -[value] ====== VALUES COMPUTED ====== diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle index 5aafc7dfe0f28d89c3187e175673487ab39f0340..91778b7edbeff4e3bc5fb224e877922d4069b8ff 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle @@ -1,11 +1,3 @@ -[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/bts/bts1717.i (no preprocessing) [e-acsl] beginning translation. [e-acsl] translation done in project "e-acsl". [value] Analyzing a complete application starting at main @@ -28,4 +20,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got [value] using specification for function __delete_block [value] using specification for function __e_acsl_memory_clean [value] done for function main -[value] ====== VALUES COMPUTED ======