diff --git a/tests/ptests_config b/tests/ptests_config index 7f88d14afd5084b1a1b167317be74a23dda7f814..1df830115c750baa5eb44fd157a1e90054422381 100644 --- a/tests/ptests_config +++ b/tests/ptests_config @@ -18,12 +18,11 @@ DEFAULT_SUITES= value/numerors value/traces DEFAULT_SUITES= value builtins float idct ### Tests of EVA domains -apron_SUITES = + +apron_SUITES = builtins float idct value bitwise_SUITES = value builtins float idct equality_SUITES = value builtins float idct gauges_SUITES = value builtins float idct multidim_SUITES = value builtins float idct octagon_SUITES = value builtins float idct symblocs_SUITES = value builtins float idct -# todo: -IGNORE= apron_SUITES = builtins float idct value diff --git a/tests/test_config b/tests/test_config index fb474386300e9109653c99839364a33a783455eb..e4646d0bf7209ddba9a34a6c8b9e31bcebdde41c 100644 --- a/tests/test_config +++ b/tests/test_config @@ -1,6 +1,7 @@ MACRO: EVA_MAIN_PLUGINS eva,scope MACRO: EVA_PLUGINS from,inout @EVA_MAIN_PLUGINS@ variadic MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32 +MACRO: EVA_DEFAULT_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 MACRO: EVA_TEST -eva @EVA_CONFIG@ -out -input -deps MACRO: RTE_TEST -rte -no-warn-invalid-pointer @@ -10,4 +11,4 @@ PLUGIN: @EVA_PLUGINS@ OPT: @EVA_TEST@ # Late declaration to allow redefinition of EVA_OPTIONS in subsidiary test_config files -MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 +MACRO: EVA_OPTIONS @EVA_DEFAULT_OPTIONS@ diff --git a/tests/test_config_apron b/tests/test_config_apron index 5bc02fb2551b5cbdfece488b945456d79adbb705..9ccdb858427dc54e0bc1cd9b5e3da0abe1aef063 100644 --- a/tests/test_config_apron +++ b/tests/test_config_apron @@ -1,6 +1,7 @@ -MACRO: EVA_MAIN_PLUGINS eva,scope +MACRO: EVA_MAIN_PLUGINS eva,scope,eva.apron MACRO: EVA_PLUGINS from,inout @EVA_MAIN_PLUGINS@ variadic MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32 +MACRO: EVA_DEFAULT_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 MACRO: EVA_TEST -eva @EVA_CONFIG@ -out -input -deps MACRO: RTE_TEST -rte -no-warn-invalid-pointer @@ -12,4 +13,4 @@ PLUGIN: @EVA_PLUGINS@ OPT: @EVA_TEST@ # Late declaration to allow redefinition of EVA_OPTIONS in subsidiary test_config_xxx files -MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains apron-octagon -eva-warn-key experimental=inactive +MACRO: EVA_OPTIONS @EVA_DEFAULT_OPTIONS@ -eva-domains apron-octagon -eva-warn-key experimental=inactive diff --git a/tests/test_config_bitwise b/tests/test_config_bitwise index 7cb2da1759921ae1004517f41c903f76a9067bcf..3a6cca5ea5674ad277b0ed42deef0628bc62449a 100644 --- a/tests/test_config_bitwise +++ b/tests/test_config_bitwise @@ -1,6 +1,7 @@ MACRO: EVA_MAIN_PLUGINS eva,scope MACRO: EVA_PLUGINS from,inout @EVA_MAIN_PLUGINS@ variadic MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32 +MACRO: EVA_DEFAULT_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 MACRO: EVA_TEST -eva @EVA_CONFIG@ -out -input -deps MACRO: RTE_TEST -rte -no-warn-invalid-pointer @@ -12,4 +13,4 @@ PLUGIN: @EVA_PLUGINS@ OPT: @EVA_TEST@ # Late declaration to allow redefinition of EVA_OPTIONS in subsidiary test_config_xxx files -MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains bitwise +MACRO: EVA_OPTIONS @EVA_DEFAULT_OPTIONS@ -eva-domains bitwise diff --git a/tests/test_config_equality b/tests/test_config_equality index 5dab3a18f41d57260d9b0e38ecbc357a1af12314..b838bebe8448dbe62029a5cc666aa27a36bba9b8 100644 --- a/tests/test_config_equality +++ b/tests/test_config_equality @@ -1,6 +1,7 @@ MACRO: EVA_MAIN_PLUGINS eva,scope MACRO: EVA_PLUGINS from,inout @EVA_MAIN_PLUGINS@ variadic MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32 +MACRO: EVA_DEFAULT_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 MACRO: EVA_TEST -eva @EVA_CONFIG@ -out -input -deps MACRO: RTE_TEST -rte -no-warn-invalid-pointer @@ -12,4 +13,4 @@ PLUGIN: @EVA_PLUGINS@ OPT: @EVA_TEST@ # Late declaration to allow redefinition of EVA_OPTIONS in subsidiary test_config_xxx files -MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains equality +MACRO: EVA_OPTIONS @EVA_DEFAULT_OPTIONS@ -eva-domains equality diff --git a/tests/test_config_gauges b/tests/test_config_gauges index 93f3294a8f30b92c71212f7d7e7a0569e7d7cbe3..27b3697d1a66c9c8d190828eb01da0c52534e523 100644 --- a/tests/test_config_gauges +++ b/tests/test_config_gauges @@ -1,6 +1,7 @@ MACRO: EVA_MAIN_PLUGINS eva,scope MACRO: EVA_PLUGINS from,inout @EVA_MAIN_PLUGINS@ variadic MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32 +MACRO: EVA_DEFAULT_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 MACRO: EVA_TEST -eva @EVA_CONFIG@ -out -input -deps MACRO: RTE_TEST -rte -no-warn-invalid-pointer @@ -12,4 +13,4 @@ PLUGIN: @EVA_PLUGINS@ OPT: @EVA_TEST@ # Late declaration to allow redefinition of EVA_OPTIONS in subsidiary test_config_xxx files -MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains gauges +MACRO: EVA_OPTIONS @EVA_DEFAULT_OPTIONS@ -eva-domains gauges diff --git a/tests/test_config_multidim b/tests/test_config_multidim index 4499a5369879791a5845e0353194e1c61313ea9f..5dd93355aa902f2072afb6327ab000b35871c446 100644 --- a/tests/test_config_multidim +++ b/tests/test_config_multidim @@ -1,6 +1,7 @@ MACRO: EVA_MAIN_PLUGINS eva,scope MACRO: EVA_PLUGINS from,inout @EVA_MAIN_PLUGINS@ variadic MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32 +MACRO: EVA_DEFAULT_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 MACRO: EVA_TEST -eva @EVA_CONFIG@ -out -input -deps MACRO: RTE_TEST -rte -no-warn-invalid-pointer @@ -12,4 +13,4 @@ PLUGIN: @EVA_PLUGINS@ OPT: @EVA_TEST@ # Late declaration to allow redefinition of EVA_OPTIONS in subsidiary test_config_xxx files -MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains multidim -eva-warn-key experimental=inactive +MACRO: EVA_OPTIONS @EVA_DEFAULT_OPTIONS@ -eva-domains multidim -eva-warn-key experimental=inactive diff --git a/tests/test_config_octagon b/tests/test_config_octagon index eadb9a73a24213917a975331e439207425fb4351..ba4e2eaf9eebdbb96b16d6bd185a59c0e102c057 100644 --- a/tests/test_config_octagon +++ b/tests/test_config_octagon @@ -1,6 +1,7 @@ MACRO: EVA_MAIN_PLUGINS eva,scope MACRO: EVA_PLUGINS from,inout @EVA_MAIN_PLUGINS@ variadic MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32 +MACRO: EVA_DEFAULT_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 MACRO: EVA_TEST -eva @EVA_CONFIG@ -out -input -deps MACRO: RTE_TEST -rte -no-warn-invalid-pointer @@ -12,4 +13,4 @@ PLUGIN: @EVA_PLUGINS@ OPT: @EVA_TEST@ # Late declaration to allow redefinition of EVA_OPTIONS in subsidiary test_config_xxx files -MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-domains octagon +MACRO: EVA_OPTIONS @EVA_DEFAULT_OPTIONS@ -eva-domains octagon diff --git a/tests/test_config_symblocs b/tests/test_config_symblocs index ac0fd259c17046fcb49ee99cb6450d3382f20b3b..9fa8d37ab8e2c4317a000c93d1f05b63d15bac42 100644 --- a/tests/test_config_symblocs +++ b/tests/test_config_symblocs @@ -1,6 +1,7 @@ MACRO: EVA_MAIN_PLUGINS eva,scope MACRO: EVA_PLUGINS from,inout @EVA_MAIN_PLUGINS@ variadic MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32 +MACRO: EVA_DEFAULT_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 MACRO: EVA_TEST -eva @EVA_CONFIG@ -out -input -deps MACRO: RTE_TEST -rte -no-warn-invalid-pointer @@ -12,4 +13,4 @@ PLUGIN: @EVA_PLUGINS@ OPT: @EVA_TEST@ # Late declaration to allow redefinition of EVA_OPTIONS in subsidiary test_config_xxx files -MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains symbolic-locations +MACRO: EVA_OPTIONS @EVA_DEFAULT_OPTIONS@ -eva-domains symbolic-locations diff --git a/tests/value/oracle_apron/relation_reduction.res.oracle b/tests/value/oracle_apron/relation_reduction.res.oracle index 8a21962cbf7ee29df021dc9936f5dbc44f8160e7..cb9102afadb1c2426e8f28eeba0cbd148a787039 100644 --- a/tests/value/oracle_apron/relation_reduction.res.oracle +++ b/tests/value/oracle_apron/relation_reduction.res.oracle @@ -13,3 +13,11 @@ > R2 ∈ {0; 12} > R3 ∈ {0; 7} > R4 ∈ {0; 2} +48c44 +< R4 FROM tab[0..8]; x (and SELF) +--- +> R4 FROM tab[0..5]; x (and SELF) +53c49 +< y; t; tab[0..8] +--- +> y; t; tab[0..5] diff --git a/tests/value/oracle_apron/relations2.res.oracle b/tests/value/oracle_apron/relations2.res.oracle index 6ed84293d3f612ca321a787f6310b195234a9758..826838be9fa828494778a91aa0b0b45ae7026db1 100644 --- a/tests/value/oracle_apron/relations2.res.oracle +++ b/tests/value/oracle_apron/relations2.res.oracle @@ -17,3 +17,15 @@ < len ∈ [--..--] --- > len ∈ [0..1023] +182c177 +< \result FROM a[0..513] +--- +> \result FROM a[0..511] +198c193 +< a[0..513] +--- +> a[0..511] +202c197 +< sv; a[0..513]; T[0..6] +--- +> sv; a[0..511]; T[0..6] diff --git a/tests/value/redundant_alarms.c b/tests/value/redundant_alarms.c index 1009eafff78a6b6e4c778ce62ce41d192e621084..8b30501f036b2dd1444145e6f504e42288efcc91 100644 --- a/tests/value/redundant_alarms.c +++ b/tests/value/redundant_alarms.c @@ -1,5 +1,5 @@ /* run.config* - PLUGIN: inout,scope,slicing,sparecode + PLUGIN: @EVA_MAIN_PLUGINS@ inout,scope,slicing,sparecode OPT: @EVA_CONFIG@ -eva-warn-copy-indeterminate=-@all,main3 -scope-msg-key rm_asserts -scope-verbose 2 -eva-remove-redundant-alarms -print -slice-threat main1 -then-on 'Slicing export' -print **/ volatile int v; diff --git a/tests/value/unknown_sizeof.i b/tests/value/unknown_sizeof.i index 40b7487daa78839926f4004ada6b81924d513109..7c4f11748a1213a6f50e70283c19329ca44a4698 100644 --- a/tests/value/unknown_sizeof.i +++ b/tests/value/unknown_sizeof.i @@ -1,8 +1,8 @@ /* run.config* EXIT: 1 PLUGIN: eva - OPT: -eva @EVA_CONFIG@ -main main1 - OPT: -eva @EVA_CONFIG@ -main main2 + OPT: -eva @EVA_DEFAULT_OPTIONS@ -machdep x86_32 -main main1 + OPT: -eva @EVA_DEFAULT_OPTIONS@ -machdep x86_32 -main main2 */ struct s; struct s s;