Skip to content
Snippets Groups Projects
Commit 638d37ca authored by Patrick Baudin's avatar Patrick Baudin
Browse files

test review of EVA plugin

parent c3628223
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 68 additions and 41 deletions
tests/test_config
+ 2
− 1
View file @ 638d37ca
MACRO: EVA_PLUGINS from,inout,eva,scope,variadic MACRO: EVA_MAIN_PLUGINS eva,scope
MACRO: EVA_PLUGINS from,inout @EVA_MAIN_PLUGINS@ variadic
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0
MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32 MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
MACRO: EVA_TEST -eva @EVA_CONFIG@ -out -input -deps MACRO: EVA_TEST -eva @EVA_CONFIG@ -out -input -deps
......
tests/test_config_apron
+ 6
− 2
View file @ 638d37ca
MACRO: EVA_PLUGINS from,inout,eva,scope,variadic MACRO: EVA_MAIN_PLUGINS eva,scope
MACRO: EVA_PLUGINS from,inout @EVA_MAIN_PLUGINS@ variadic
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-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains apron-octagon -eva-warn-key experimental=inactive
MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32 MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
MACRO: EVA_TEST -eva @EVA_CONFIG@ -out -input -deps
MACRO: RTE_TEST -rte -no-warn-invalid-pointer
# Compare the result with the oracle of the default config. # Compare the result with the oracle of the default config.
FILTER: diff --new-file @PTEST_DIR@/oracle/@PTEST_ORACLE@ - FILTER: diff --new-file @PTEST_DIR@/oracle/@PTEST_ORACLE@ -
PLUGIN: @EVA_PLUGINS@ PLUGIN: @EVA_PLUGINS@
OPT: -eva @EVA_CONFIG@ -out -input -deps OPT: @EVA_TEST@
tests/test_config_bitwise
+ 8
− 3
View file @ 638d37ca
MACRO: EVA_PLUGINS from,inout,eva,scope,variadic MACRO: EVA_MAIN_PLUGINS eva,scope
MACRO: EVA_PLUGINS from,inout @EVA_MAIN_PLUGINS@ variadic
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains bitwise MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains bitwise
MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32 MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
MACRO: EVA_TEST -eva @EVA_CONFIG@ -out -input -deps
MACRO: RTE_TEST -rte -no-warn-invalid-pointer
# Compare the result with the oracle of the default config. # Compare the result with the oracle of the default config.
FILTER: diff --new-file @PTEST_DIR@/oracle/@PTEST_ORACLE@ - FILTER: diff --new-file @PTEST_DIR@/oracle/@PTEST_ORACLE@ -
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps PLUGIN: @EVA_PLUGINS@
OPT: @EVA_TEST@
tests/test_config_equality
+ 6
− 2
View file @ 638d37ca
MACRO: EVA_PLUGINS from,inout,eva,scope,variadic MACRO: EVA_MAIN_PLUGINS eva,scope
MACRO: EVA_PLUGINS from,inout @EVA_MAIN_PLUGINS@ variadic
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains equality MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains equality
MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32 MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
MACRO: EVA_TEST -eva @EVA_CONFIG@ -out -input -deps
MACRO: RTE_TEST -rte -no-warn-invalid-pointer
# Compare the result with the oracle of the default config. # Compare the result with the oracle of the default config.
FILTER: diff --new-file @PTEST_DIR@/oracle/@PTEST_ORACLE@ - FILTER: diff --new-file @PTEST_DIR@/oracle/@PTEST_ORACLE@ -
PLUGIN: @EVA_PLUGINS@ PLUGIN: @EVA_PLUGINS@
OPT: -eva @EVA_CONFIG@ -out -input -deps OPT: @EVA_TEST@
tests/test_config_gauges
+ 6
− 2
View file @ 638d37ca
MACRO: EVA_PLUGINS from,inout,eva,scope,variadic MACRO: EVA_MAIN_PLUGINS eva,scope
MACRO: EVA_PLUGINS from,inout @EVA_MAIN_PLUGINS@ variadic
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains gauges MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains gauges
MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32 MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
MACRO: EVA_TEST -eva @EVA_CONFIG@ -out -input -deps
MACRO: RTE_TEST -rte -no-warn-invalid-pointer
# Compare the result with the oracle of the default config. # Compare the result with the oracle of the default config.
FILTER: diff --new-file @PTEST_DIR@/oracle/@PTEST_ORACLE@ - FILTER: diff --new-file @PTEST_DIR@/oracle/@PTEST_ORACLE@ -
PLUGIN: @EVA_PLUGINS@ PLUGIN: @EVA_PLUGINS@
OPT: -eva @EVA_CONFIG@ -out -input -deps OPT: @EVA_TEST@
tests/test_config_octagon
+ 6
− 2
View file @ 638d37ca
MACRO: EVA_PLUGINS from,inout,eva,scope,variadic MACRO: EVA_MAIN_PLUGINS eva,scope
MACRO: EVA_PLUGINS from,inout @EVA_MAIN_PLUGINS@ variadic
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-domains octagon MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-domains octagon
MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32 MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
MACRO: EVA_TEST -eva @EVA_CONFIG@ -out -input -deps
MACRO: RTE_TEST -rte -no-warn-invalid-pointer
# Compare the result with the oracle of the default config. # Compare the result with the oracle of the default config.
FILTER: diff --new-file @PTEST_DIR@/oracle/@PTEST_ORACLE@ - FILTER: diff --new-file @PTEST_DIR@/oracle/@PTEST_ORACLE@ -
PLUGIN: @EVA_PLUGINS@ PLUGIN: @EVA_PLUGINS@
OPT: -eva @EVA_CONFIG@ -out -input -deps OPT: @EVA_TEST@
tests/test_config_symblocs
+ 6
− 2
View file @ 638d37ca
MACRO: EVA_PLUGINS from,inout,eva,scope,variadic MACRO: EVA_MAIN_PLUGINS eva,scope
MACRO: EVA_PLUGINS from,inout @EVA_MAIN_PLUGINS@ variadic
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains symbolic-locations MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains symbolic-locations
MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32 MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
MACRO: EVA_TEST -eva @EVA_CONFIG@ -out -input -deps
MACRO: RTE_TEST -rte -no-warn-invalid-pointer
# Compare the result with the oracle of the default config. # Compare the result with the oracle of the default config.
FILTER: diff --new-file @PTEST_DIR@/oracle/@PTEST_ORACLE@ - FILTER: diff --new-file @PTEST_DIR@/oracle/@PTEST_ORACLE@ -
PLUGIN: @EVA_PLUGINS@ PLUGIN: @EVA_PLUGINS@
OPT: -eva @EVA_CONFIG@ -out -input -deps OPT: @EVA_TEST@
tests/value/ai_annot.i
+ 1
− 1
View file @ 638d37ca
/* run.config* /* run.config*
STDOPT: #"-load-module scope -scope-verbose 2 -eva-remove-redundant-alarms -eva-context-width 3" STDOPT: #"-scope-verbose 2 -eva-remove-redundant-alarms -eva-context-width 3"
*/ */
......
tests/value/align_char_array.c
+ 2
− 2
View file @ 638d37ca
/* run.config* /* run.config*
OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -cpp-extra-args="-DPTEST" -journal-disable PLUGIN: @EVA_MAIN_PLUGINS@
OPT: -eva @EVA_CONFIG@ -cpp-extra-args="-DPTEST"
*/ */
#ifndef PTEST #ifndef PTEST
#include <stdio.h> #include <stdio.h>
#endif #endif
......
tests/value/array_initializer.i
+ 2
− 2
View file @ 638d37ca
/* run.config* /* run.config*
OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -then -eva-initialization-padding-globals maybe PLUGIN: @EVA_MAIN_PLUGINS@
OPT: -eva @EVA_CONFIG@ -then -eva-initialization-padding-globals maybe
*/ */
int t[5] = { [2] = 3 }; int t[5] = { [2] = 3 };
struct { char a; int t[5]; } s = { 'a' , { [2] = 3 } }; struct { char a; int t[5]; } s = { 'a' , { [2] = 3 } };
......
tests/value/array_zero_length.i
+ 4
− 4
View file @ 638d37ca
/* run.config* /* run.config*
OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -journal-disable -machdep gcc_x86_32 PLUGIN: @EVA_MAIN_PLUGINS@
OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -lib-entry -journal-disable -machdep gcc_x86_32 OPT: -eva @EVA_CONFIG@ -machdep gcc_x86_32
OPT: -eva @EVA_CONFIG@ -lib-entry -machdep gcc_x86_32
EXIT: 1 EXIT: 1
OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -lib-entry -journal-disable OPT: -eva @EVA_CONFIG@ -lib-entry
*/ */
char T[]; char T[];
char U[0]; char U[0];
char V[][2]; char V[][2];
......
tests/value/base_addr_offset_block_length.i
+ 2
− 2
View file @ 638d37ca
/* run.config* /* run.config*
OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -eva-context-width 3 -then -eva-slevel 3 PLUGIN: @EVA_MAIN_PLUGINS@
OPT: -eva @EVA_CONFIG@ -eva-context-width 3 -then -eva-slevel 3
*/ */
int x, y; int x, y;
short z; short z;
......
tests/value/big_lib_entry.i
+ 2
− 2
View file @ 638d37ca
/* run.config* /* run.config*
OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -lib-entry -eva-context-width 4 -eva-initialization-padding-globals no PLUGIN: @EVA_MAIN_PLUGINS@
OPT: -eva @EVA_CONFIG@ -lib-entry -eva-context-width 4 -eva-initialization-padding-globals no
*/ */
typedef struct { typedef struct {
int f1; int f1;
float f2; float f2;
......
tests/value/bitfield_longlong.c
+ 3
− 3
View file @ 638d37ca
/* run.config* /* run.config*
OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -cpp-extra-args="-Dprintf=Frama_C_show_each" -journal-disable PLUGIN: @EVA_MAIN_PLUGINS@
OPT: -eva @EVA_CONFIG@ -cpp-extra-args="-Dprintf=Frama_C_show_each"
*/ */
struct X50 { struct X50 {
long long int z:50; long long int z:50;
} s50 = { 2 }; } s50 = { 2 };
struct X10 { struct X10 {
long long int z:10; long long int z:10;
} s10 = { 2 }; } s10 = { 2 };
struct U32 { struct U32 {
unsigned long z:32; unsigned long z:32;
} u32 = { -1 }; } u32 = { -1 };
......
tests/value/bts1306.i
+ 2
− 1
View file @ 638d37ca
/* run.config* /* run.config*
OPT: -no-autoload-plugins -load-module from,inout,eva -constfold -eva-slevel 0 -eva @EVA_CONFIG@ -print -then -eva-slevel 10 -eva -print PLUGIN: @EVA_MAIN_PLUGINS@
OPT: -constfold -eva-slevel 0 -eva @EVA_CONFIG@ -print -then -eva-slevel 10 -eva -print
*/ */
void g(double x) { double y= x*x; } void g(double x) { double y= x*x; }
......
tests/value/case_analysis.i
+ 2
− 2
View file @ 638d37ca
/* run.config* /* run.config*
OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -eva-slevel 30 -journal-disable -float-normal PLUGIN: @EVA_MAIN_PLUGINS@
OPT: -eva @EVA_CONFIG@ -eva-slevel 30 -float-normal
*/ */
int sq,s; int sq,s;
......
tests/value/cond_integer_cast_of_float.i
+ 2
− 2
View file @ 638d37ca
/* run.config* /* run.config*
OPT: -no-autoload-plugins -load-module eva -eva @EVA_CONFIG@ -eva-no-results -then -float-hex -main mainbis PLUGIN: @EVA_MAIN_PLUGINS@
OPT: -eva @EVA_CONFIG@ -eva-no-results -then -float-hex -main mainbis
*/ */
typedef double D; typedef double D;
typedef float F; typedef float F;
int b; int b;
extern F f1, f2, f3, f4; extern F f1, f2, f3, f4;
extern D d1, d2, d3; extern D d1, d2, d3;
......
tests/value/const_typedef.i
+ 2
− 2
View file @ 638d37ca
/* run.config* /* run.config*
OPT: -machdep x86_32 -no-autoload-plugins -load-module inout,eva -print -then -eva @EVA_CONFIG@ -lib-entry -no-print PLUGIN: @EVA_MAIN_PLUGINS@
OPT: -machdep x86_32 -print -then -eva @EVA_CONFIG@ -lib-entry -no-print
*/ */
typedef int INT[3][3]; typedef int INT[3][3];
typedef int INT2[][3]; typedef int INT2[][3];
typedef int INT3[2][7]; typedef int INT3[2][7];
......
tests/value/constarraystructlibentry.i
+ 2
− 2
View file @ 638d37ca
/* run.config* /* run.config*
OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -lib-entry -eva-initialization-padding-globals yes -then -eva-initialization-padding-globals no PLUGIN: @EVA_MAIN_PLUGINS@
OPT: -eva @EVA_CONFIG@ -lib-entry -eva-initialization-padding-globals yes -then -eva-initialization-padding-globals no
*/ */
const int t[] = { 1, 2, 3, 4, 5 } ; const int t[] = { 1, 2, 3, 4, 5 } ;
const int t2[3][3] = { 1, 2, 3, 4, 5, 6, 7, 8, 9 } ; const int t2[3][3] = { 1, 2, 3, 4, 5, 6, 7, 8, 9 } ;
......
tests/value/context_free.i
+ 2
− 2
View file @ 638d37ca
/* run.config* /* run.config*
PLUGIN: @EVA_MAIN_PLUGINS@
OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -lib-entry -main f -absolute-valid-range 0x200-0x199 -eva-msg-key initial-state -journal-disable OPT: -eva @EVA_CONFIG@ -lib-entry -main f -absolute-valid-range 0x200-0x199 -eva-msg-key initial-state
*/ */
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment