From 9150130ae44d0a71a605720d4a9c13980e561088 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 13 Sep 2022 17:37:47 +0200
Subject: [PATCH] [eva] enable apron suite + oracle update
---
tests/ptests_config | 5 ++---
tests/test_config | 3 ++-
tests/test_config_apron | 5 +++--
tests/test_config_bitwise | 3 ++-
tests/test_config_equality | 3 ++-
tests/test_config_gauges | 3 ++-
tests/test_config_multidim | 3 ++-
tests/test_config_octagon | 3 ++-
tests/test_config_symblocs | 3 ++-
.../value/oracle_apron/relation_reduction.res.oracle | 8 ++++++++
tests/value/oracle_apron/relations2.res.oracle | 12 ++++++++++++
tests/value/redundant_alarms.c | 2 +-
tests/value/unknown_sizeof.i | 4 ++--
13 files changed, 42 insertions(+), 15 deletions(-)
diff --git a/tests/ptests_config b/tests/ptests_config
index 7f88d14afd5..1df830115c7 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 fb474386300..e4646d0bf72 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 5bc02fb2551..9ccdb858427 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 7cb2da17599..3a6cca5ea56 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 5dab3a18f41..b838bebe844 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 93f3294a8f3..27b3697d1a6 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 4499a536987..5dd93355aa9 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 eadb9a73a24..ba4e2eaf9ee 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 ac0fd259c17..9fa8d37ab8e 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 8a21962cbf7..cb9102afadb 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 6ed84293d3f..826838be9fa 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 1009eafff78..8b30501f036 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 40b7487daa7..7c4f11748a1 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;
--
GitLab