From 651ec99829c3e09a8df7f37e3b58d5b089b007af Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Thu, 25 Oct 2018 09:02:52 +0200
Subject: [PATCH] [Eva] Update remaining occurrences of -val
---
INSTALL.md | 8 ++++----
README.md | 2 +-
src/plugins/value/test.assert.sh | 2 +-
src/plugins/value/test.sh | 2 +-
src/plugins/value/utils/value_util.mli | 2 +-
tests/scope/zones.ml | 2 +-
6 files changed, 9 insertions(+), 9 deletions(-)
diff --git a/INSTALL.md b/INSTALL.md
index 8cf06f616b8..4fdc7fd8b30 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -240,8 +240,8 @@ Arch Linux: `yaourt -S frama-c`
6. Optionally, test your installation by running:
- frama-c -val tests/misc/CruiseControl*.c
- frama-c-gui -val tests/misc/CruiseControl*.c # if frama-c-gui is available
+ frama-c -eva tests/misc/CruiseControl*.c
+ frama-c-gui -eva tests/misc/CruiseControl*.c # if frama-c-gui is available
### Full Compilation Guide
@@ -313,8 +313,8 @@ This step is optional.
Test your installation by running:
- frama-c -val tests/misc/CruiseControl*.c
- frama-c-gui -val tests/misc/CruiseControl*.c (if frama-c-gui is available)
+ frama-c -eva tests/misc/CruiseControl*.c
+ frama-c-gui -eva tests/misc/CruiseControl*.c (if frama-c-gui is available)
diff --git a/README.md b/README.md
index b3e8626a077..311311ec88e 100644
--- a/README.md
+++ b/README.md
@@ -57,7 +57,7 @@ The recommended usage for simple files is one of the following lines:
frama-c-gui file.c
Where `-<plugin>` is one of the several Frama-C plug-ins,
-e.g. `-val`, or `-wp`, or `-metrics`, etc.
+e.g. `-eva`, or `-wp`, or `-metrics`, etc.
Plug-ins can also be run directly from the GUI.
To list all plug-ins, run:
diff --git a/src/plugins/value/test.assert.sh b/src/plugins/value/test.assert.sh
index a68048c098c..38049b28c4c 100755
--- a/src/plugins/value/test.assert.sh
+++ b/src/plugins/value/test.assert.sh
@@ -14,7 +14,7 @@ gcc $GCC3264 -pipe t$N.a.i $CSMITH/dump_assert_nop-$FRAMAC3264.o -o e$N
rcexec=$?
if [[ $rcexec != 127 && $rcexec != 152 && $rcexec != 137 ]]
then
- ( ulimit -S -t 18000 -m 2500000 ; exec ~/ppc/bin/toplevel.opt -no-collapse-call-cast -slevel-function main:0 -no-results -warn-signed-overflow -val t$N.a.i -no-val-show-progress -machdep $FRAMAC3264 -precise-unions > res$N.value )
+ ( ulimit -S -t 18000 -m 2500000 ; exec ~/ppc/bin/toplevel.opt -no-collapse-call-cast -slevel-function main:0 -no-results -warn-signed-overflow -eva t$N.a.i -eva-no-show-progress -machdep $FRAMAC3264 -precise-unions > res$N.value )
rc=$?
if grep imprecise res$N.value
then
diff --git a/src/plugins/value/test.sh b/src/plugins/value/test.sh
index 8cfbcc5b403..1c19540871f 100755
--- a/src/plugins/value/test.sh
+++ b/src/plugins/value/test.sh
@@ -15,7 +15,7 @@ if [[ $rcexec != 152 && $rcexec != 137 ]]
then
if grep "user.0m0.0[01]" time$N
then
- ( ulimit -S -t 18000 -m 2500000 ; exec ~/ppc/bin/toplevel.opt -warn-signed-overflow -val t$N.i -stop-at-first-alarm -no-val-show-progress -machdep $FRAMAC3264 -obviously-terminates -precise-unions > res$N.value )
+ ( ulimit -S -t 18000 -m 2500000 ; exec ~/ppc/bin/toplevel.opt -warn-signed-overflow -eva t$N.i -stop-at-first-alarm -eva-no-show-progress -machdep $FRAMAC3264 -obviously-terminates -precise-unions > res$N.value )
rc=$?
if grep imprecise res$N.value
then
diff --git a/src/plugins/value/utils/value_util.mli b/src/plugins/value/utils/value_util.mli
index c405b30931b..c5591484346 100644
--- a/src/plugins/value/utils/value_util.mli
+++ b/src/plugins/value/utils/value_util.mli
@@ -115,7 +115,7 @@ val height_lval: lval -> int
val skip_specifications: kernel_function -> bool
(** Should we skip the specifications of this function, according to
- [-val-skip-stdlib-specs] *)
+ [-eva-skip-stdlib-specs] *)
(*
Local Variables:
diff --git a/tests/scope/zones.ml b/tests/scope/zones.ml
index 5b6358d19d5..19d3afc1211 100644
--- a/tests/scope/zones.ml
+++ b/tests/scope/zones.ml
@@ -1,5 +1,5 @@
(* when using toplevel.top :
-bin/topleval.top -val tests/scope/zones.c
+bin/topleval.top -eva tests/scope/zones.c
#directory "cil/src";;
*)
--
GitLab