[Eva] Update remaining occurrences of -val

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)
 
 
 

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:

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  

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  

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:

tests/scope/zones.ml

 (* when using toplevel.top :
-bin/topleval.top -val tests/scope/zones.c
+bin/topleval.top -eva tests/scope/zones.c
 #directory "cil/src";;
 *)