diff --git a/INSTALL.md b/INSTALL.md index 8cf06f616b8e35744731164d784424fbeb15b921..4fdc7fd8b309cc4cb7bbe1d53f719240657d6fa8 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 b3e8626a07754129acf3f849ad8c8c3538640d78..311311ec88e675bcba114a079bd908aa512a5064 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 a68048c098cfaf3fd9d18a030b03d7c412581785..38049b28c4c8d1e44620765127875b5d1773f8db 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 8cfbcc5b403c19145934a1d2ddc19d376ed14a56..1c19540871f090abbdb78f4ee1c4eda1b8f15625 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 c405b30931ba221f90b62163c0570f8f551a82ea..c5591484346ace29a5b93c027b1171492113898a 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 5b6358d19d5e8e7790fc3461ac451d07283fac48..19d3afc121119fb4bfbd343f526d57b9b91b33ec 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";; *)