Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
pub
frama-c
Commits
9150130a
Commit
9150130a
authored
Sep 13, 2022
by
Allan Blanchard
Browse files
[eva] enable apron suite + oracle update
parent
f3c832f9
Changes
13
Hide whitespace changes
Inline
Side-by-side
tests/ptests_config
View file @
9150130a
...
...
@@ -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
tests/test_config
View file @
9150130a
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@
tests/test_config_apron
View file @
9150130a
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
tests/test_config_bitwise
View file @
9150130a
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
tests/test_config_equality
View file @
9150130a
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
tests/test_config_gauges
View file @
9150130a
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
tests/test_config_multidim
View file @
9150130a
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
tests/test_config_octagon
View file @
9150130a
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
tests/test_config_symblocs
View file @
9150130a
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
tests/value/oracle_apron/relation_reduction.res.oracle
View file @
9150130a
...
...
@@ -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]
tests/value/oracle_apron/relations2.res.oracle
View file @
9150130a
...
...
@@ -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]
tests/value/redundant_alarms.c
View file @
9150130a
/* 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
;
...
...
tests/value/unknown_sizeof.i
View file @
9150130a
/* 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
;
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment