From 43bb2612925fc88b03489fba3ceea4d57929f3ce Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Fri, 29 Jan 2021 10:49:17 +0100
Subject: [PATCH] [Tests] adds bitwise_SUITES = value
---
ptests/ptests.ml | 2 +-
tests/ptests_config | 2 +-
tests/value/.gitignore | 1 -
tests/value/empty_struct2.c | 2 +-
.../value/oracle_bitwise/addition.res.oracle | 20 +++++++++++++++++++
tests/value/oracle_bitwise/bitwise.res.oracle | 7 +++++++
.../oracle_bitwise/bitwise_pointer.res.oracle | 12 +++++++++++
.../oracle_bitwise/logic_ptr_cast.res.oracle | 6 ++++++
8 files changed, 48 insertions(+), 4 deletions(-)
create mode 100644 tests/value/oracle_bitwise/addition.res.oracle
create mode 100644 tests/value/oracle_bitwise/bitwise.res.oracle
create mode 100644 tests/value/oracle_bitwise/bitwise_pointer.res.oracle
create mode 100644 tests/value/oracle_bitwise/logic_ptr_cast.res.oracle
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index 97c99a60a22..e5d457cf1e1 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -1044,7 +1044,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
let filter = Str.global_replace regexp foracle filter in
Format.fprintf result_fmt
"(rule ; FILTER %s #%d OF TEST FILE %S\n \
- (action (with-stdout-to %S (system %S)))\n\
+ (action (with-stdout-to %S (with-accepted-exit-codes (or 0 1 2 125) (system %S))))\n\
)@."
txt
command.nth command.file
diff --git a/tests/ptests_config b/tests/ptests_config
index eefa38fff20..aa9705642ba 100644
--- a/tests/ptests_config
+++ b/tests/ptests_config
@@ -16,7 +16,7 @@ IGNORE= DEFAULT_SUITES= make_run_script
IGNORE= DEFAULT_SUITES= value/numerors
IGNORE= apron_SUITES = value
-IGNORE= bitwise_SUITES = value
+bitwise_SUITES = value
IGNORE= equalities_SUITES = value
IGNORE= gauges_SUITES = value
IGNORE= octagon_SUITES = value
diff --git a/tests/value/.gitignore b/tests/value/.gitignore
index 5de45901ce6..e69de29bb2d 100644
--- a/tests/value/.gitignore
+++ b/tests/value/.gitignore
@@ -1 +0,0 @@
-/oracle_*
diff --git a/tests/value/empty_struct2.c b/tests/value/empty_struct2.c
index 9cff3b7e350..f961bf9c73c 100644
--- a/tests/value/empty_struct2.c
+++ b/tests/value/empty_struct2.c
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config*
STDOPT: +"-machdep gcc_x86_64"
*/
diff --git a/tests/value/oracle_bitwise/addition.res.oracle b/tests/value/oracle_bitwise/addition.res.oracle
new file mode 100644
index 00000000000..5bf7aa4f39c
--- /dev/null
+++ b/tests/value/oracle_bitwise/addition.res.oracle
@@ -0,0 +1,20 @@
+121,123c121
+< [eva] addition.i:52:
+< Assigning imprecise value to p10.
+< The imprecision originates from Arithmetic {addition.i:52}
+---
+> [eva] addition.i:52: Assigning imprecise value to p10.
+163a162
+> {{ garbled mix of &{p1} (origin: Misaligned {addition.i:52}) }}
+165a165
+> {{ garbled mix of &{p2} (origin: Misaligned {addition.i:56}) }}
+186c186
+< p10 ∈ {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:52}) }}
+---
+> p10 ∈ {{ garbled mix of &{p1} }}
+405a406
+> {{ garbled mix of &{p1} (origin: Misaligned {addition.i:52}) }}
+429c430
+< p10 ∈ {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:52}) }}
+---
+> p10 ∈ {{ garbled mix of &{p1} }}
diff --git a/tests/value/oracle_bitwise/bitwise.res.oracle b/tests/value/oracle_bitwise/bitwise.res.oracle
new file mode 100644
index 00000000000..dab83d56ab2
--- /dev/null
+++ b/tests/value/oracle_bitwise/bitwise.res.oracle
@@ -0,0 +1,7 @@
+96c96,99
+< [eva] bitwise.i:158: Frama_C_show_each_dead: {0}
+---
+> [eva] bitwise.i:156:
+> The evaluation of the expression x & 2
+> led to bottom without alarms:
+> at this point the product of states has no possible concretization.
diff --git a/tests/value/oracle_bitwise/bitwise_pointer.res.oracle b/tests/value/oracle_bitwise/bitwise_pointer.res.oracle
new file mode 100644
index 00000000000..69279536b71
--- /dev/null
+++ b/tests/value/oracle_bitwise/bitwise_pointer.res.oracle
@@ -0,0 +1,12 @@
+34,36c34
+< [eva] bitwise_pointer.i:18:
+< Assigning imprecise value to p.
+< The imprecision originates from Arithmetic {bitwise_pointer.i:18}
+---
+> [eva] bitwise_pointer.i:18: Assigning imprecise value to p.
+41,43c39
+< [eva] bitwise_pointer.i:22:
+< Assigning imprecise value to p1.
+< The imprecision originates from Arithmetic {bitwise_pointer.i:22}
+---
+> [eva] bitwise_pointer.i:22: Assigning imprecise value to p1.
diff --git a/tests/value/oracle_bitwise/logic_ptr_cast.res.oracle b/tests/value/oracle_bitwise/logic_ptr_cast.res.oracle
new file mode 100644
index 00000000000..af6c101a621
--- /dev/null
+++ b/tests/value/oracle_bitwise/logic_ptr_cast.res.oracle
@@ -0,0 +1,6 @@
+8,10c8
+< [eva] logic_ptr_cast.i:8:
+< Assigning imprecise value to p.
+< The imprecision originates from Arithmetic {logic_ptr_cast.i:8}
+---
+> [eva] logic_ptr_cast.i:8: Assigning imprecise value to p.
--
GitLab