diff --git a/ptests/ptests.ml b/ptests/ptests.ml index 97c99a60a221afca0cde53195161eacb6f1bf574..e5d457cf1e1fef7ca67f5b7ac0b4d9058a3259b6 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 eefa38fff2087923666e4081abac86364bc9a613..aa9705642bacf96cf211654480b019e1c957e3ec 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 5de45901ce62a18d26c6309c170b943215b78b67..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 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 9cff3b7e3501705461f50781d898a11121decb63..f961bf9c73cebdb87d6a5a5320734800943c5d07 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 0000000000000000000000000000000000000000..5bf7aa4f39c61e0f2a36094f97327d3f11610ef7 --- /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 0000000000000000000000000000000000000000..dab83d56ab21c31cbfdae80d7c3b62a27d4cb4ff --- /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 0000000000000000000000000000000000000000..69279536b7155982fd3e9eae5480a12be0a87951 --- /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 0000000000000000000000000000000000000000..af6c101a62175e3216651e847000b5bc335971df --- /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.