diff --git a/tests/value/memexec.c b/tests/value/memexec.c index bb6bb912db9935c2a1a631b9b398d127236419f3..e87602726a13efd85890a02ab97e39e205d27042 100644 --- a/tests/value/memexec.c +++ b/tests/value/memexec.c @@ -1,7 +1,7 @@ /* run.config* - STDOPT: +"-rte-select fbug @RTE_TEST@ -then -eva" + PLUGIN: @PTEST_PLUGIN@ rtegen + STDOPT: #"-machdep x86_32 -rte-select fbug @RTE_TEST@ -then -eva" */ - int x1, y1, z1, z2; volatile int c, nondet; void f11() { diff --git a/tests/value/oracle/summary.4.res.oracle b/tests/value/oracle/summary.4.res.oracle index 6faede6c061bc435ba56fa292654caf779bf975c..81eb244352197d5f99e3c7f35bb16ba46ccbe574 100644 --- a/tests/value/oracle/summary.4.res.oracle +++ b/tests/value/oracle/summary.4.res.oracle @@ -1,5 +1,3 @@ -[kernel] Warning: -slevel is a deprecated alias for option -eva-slevel. - Please use -eva-slevel instead. [kernel] Parsing summary.i (no preprocessing) [rte:annot] annotating function alarms [rte:annot] annotating function bottom @@ -8,6 +6,8 @@ [rte:annot] annotating function logic [rte:annot] annotating function main [rte:annot] annotating function minimal +[kernel] Warning: -slevel is a deprecated alias for option -eva-slevel. + Please use -eva-slevel instead. [eva] Analyzing a complete application starting at main [eva] Computing initial state [eva] Initial state computed @@ -107,7 +107,7 @@ ---------------------------------------------------------------------------- Some errors and warnings have been raised during the analysis: by the Eva analyzer: 0 errors 1 warning - by the Frama-C kernel: 0 errors 2 warnings + by the Frama-C kernel: 0 errors 3 warnings ---------------------------------------------------------------------------- 18 alarms generated by the analysis: 3 invalid memory accesses diff --git a/tests/value/summary.i b/tests/value/summary.i index 718f105808a8e7a74784f387e3945490e35f5f0b..3ef6022672e965f17208f8baaf7385d8cfc54c8b 100644 --- a/tests/value/summary.i +++ b/tests/value/summary.i @@ -3,8 +3,8 @@ STDOPT: +"-eva-msg-key=summary -main minimal" STDOPT: +"-eva-msg-key=summary -main bottom" STDOPT: +"-eva-msg-key=summary -main main" -PLUGIN: @PTEST_PLUGIN@ rtegen - STDOPT: +"@RTE_TEST@ -eva-msg-key=summary -main main -slevel 0" + PLUGIN: @PTEST_PLUGIN@ rtegen + OPT: -machdep x86_32 @RTE_TEST@ -then @EVA_TEST@ -eva-msg-key=summary -main main -slevel 0 */ /* Tests the summary on the smallest possible program. */ void minimalist ();