diff --git a/tests/builtins/malloc-optimistic.c b/tests/builtins/malloc-optimistic.c index 67dea08d8a9e525bb232160ad435fc17e553daad..bb1e66301f34a10a42e31ff8f1c745c6f25a35b2 100644 --- a/tests/builtins/malloc-optimistic.c +++ b/tests/builtins/malloc-optimistic.c @@ -1,5 +1,5 @@ /* run.config* - STDOPT: +"-slevel 30 -eva-slevel-merge-after-loop @all -eva-malloc-functions malloc -memexec-all" + STDOPT: +"-slevel 30 -eva-slevel-merge-after-loop @all -eva-malloc-functions malloc -eva-memexec" */ //@ assigns \result \from \nothing; diff --git a/tests/builtins/malloc_memexec.c b/tests/builtins/malloc_memexec.c index 73caf738d77d23c41743d87c9e5f50dc994c5db3..004e113f6197bbcd78285c831de022ed7d246e7f 100644 --- a/tests/builtins/malloc_memexec.c +++ b/tests/builtins/malloc_memexec.c @@ -1,5 +1,5 @@ /* run.config* - OPT: -eva @VALUECONFIG@ -memexec-all -deps -inout -eva-mlevel 0 + OPT: -eva @VALUECONFIG@ -eva-memexec -deps -inout -eva-mlevel 0 */ //@ assigns \result; diff --git a/tests/idct/ieee_1180_1990.c b/tests/idct/ieee_1180_1990.c index 4926fbb95a5d04ffe9ea8693dd60f7eb6699b85c..1f0f4325eeb430e18ca50f20b716f4ecdcc6f207 100644 --- a/tests/idct/ieee_1180_1990.c +++ b/tests/idct/ieee_1180_1990.c @@ -1,6 +1,6 @@ /* run.config* GCC: - STDOPT: +"-load-module report,scope,variadic -float-normal -no-warn-signed-overflow tests/idct/idct.c -remove-redundant-alarms -memexec-all -eva-builtin sqrt:Frama_C_sqrt,cos:Frama_C_cos -then -report -report-print-properties" + STDOPT: +"-load-module report,scope,variadic -float-normal -no-warn-signed-overflow tests/idct/idct.c -remove-redundant-alarms -eva-memexec -eva-builtin sqrt:Frama_C_sqrt,cos:Frama_C_cos -then -report -report-print-properties" */ /* IEEE_1180_1990: a testbed for IDCT accuracy * Copyright (C) 2001 Renaud Pacalet diff --git a/tests/value/logicdeps.i b/tests/value/logicdeps.i index 94e2e15754f8ecea9b901ec4e2c3398b9ace3f2e..d9cb3cbed54ec814f0e5164bb9cb995713e8d30a 100644 --- a/tests/value/logicdeps.i +++ b/tests/value/logicdeps.i @@ -1,5 +1,5 @@ /* run.config* - STDOPT: +"-memexec-all -calldeps -no-deps -no-input -no-out -then -inout" + STDOPT: +"-eva-memexec -calldeps -no-deps -no-input -no-out -then -inout" */ int t[50];