From 82da75ab067a92eeb1a7c47e6c38de21c3036ef1 Mon Sep 17 00:00:00 2001 From: Julien Signoles <julien.signoles@cea.fr> Date: Thu, 28 May 2015 11:10:50 +0200 Subject: [PATCH] [tests] cherry-picked simplifying test outputs --- src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle | 9 --------- src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle | 9 --------- src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle | 9 --------- src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle | 9 --------- src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle | 9 --------- src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle | 9 --------- src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle | 9 --------- src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle | 9 --------- src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle | 9 --------- src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle | 9 --------- 10 files changed, 90 deletions(-) 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 343190f2f5b..f4cf8ba21c7 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 838283a10e0..2a6424a798c 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 22f38a1f1f1..36fc1092d18 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 af73383a57f..7583cbd29fd 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 9a7fea6d52e..c98c0cb1cdd 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 704fb9ba63c..1b7e2835fd5 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 3bd71436ad9..45341f00fdc 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 6e5736c4a8f..aa1818323b8 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 323e2e9c16b..282bf108a65 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 5aafc7dfe0f..91778b7edbe 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 ====== -- GitLab