Skip to content
Snippets Groups Projects
Commit 3b482498 authored by GARION Christophe's avatar GARION Christophe
Browse files

[scripts] typos in frama-c-lustrec.sh script

parent c4519532
No related branches found
No related tags found
No related merge requests found
...@@ -2,7 +2,7 @@ ...@@ -2,7 +2,7 @@
# simple shell script to launch Frama-C with the right options to # simple shell script to launch Frama-C with the right options to
# prove C files generated by LustreC. # prove C files generated by LustreC.
# look at the usage function for more explanations # see the usage function for more explanations
# usage function # usage function
usage () { usage () {
...@@ -11,12 +11,13 @@ usage () { ...@@ -11,12 +11,13 @@ usage () {
echo " - [-h|--help] | prints this message and exits" echo " - [-h|--help] | prints this message and exits"
echo " - [-g|--gui] | use Frama-C GUI" echo " - [-g|--gui] | use Frama-C GUI"
echo " - [-n|--no-strategies] | do not use LustreC custom WP strategies" echo " - [-n|--no-strategies] | do not use LustreC custom WP strategies"
echo " - [-t|--timeout T] | set provers timeout to T" echo " - [-t|--timeout T] | set provers timeout to T (default to 30)"
echo "" echo ""
echo " Frama-C is launched with the following options:" echo " Frama-C is launched with the following options:"
echo " -wp | use WP plugin" echo " -wp | use WP plugin"
echo " -wp-model ref,real | use ref memory model and ideal floats as reals model" echo " -wp-model ref,real | use ref memory model and ideal floats as reals model"
echo " -wp-prover alt-ergo,z3,cvc4 | use Alt-Ergo, Z3 and CVC4 SMT solvers" echo " -wp-prover alt-ergo,z3,cvc4 | use Alt-Ergo, Z3 and CVC4 SMT solvers"
echo " -wp-timeout $TIMEOUT | set solvers timeout, default to 30s"
echo " -wp-par 16 | use 16 jobs at most" echo " -wp-par 16 | use 16 jobs at most"
echo " -wp-no-warn-memory-model | dismiss various memory model related warnings" echo " -wp-no-warn-memory-model | dismiss various memory model related warnings"
echo " -wp-auto LustreC:Transitions,LustreC:MemoryPacks | use custom proof strategies if -n is not used" echo " -wp-auto LustreC:Transitions,LustreC:MemoryPacks | use custom proof strategies if -n is not used"
...@@ -68,6 +69,7 @@ done ...@@ -68,6 +69,7 @@ done
frama-c${GUI} -wp \ frama-c${GUI} -wp \
-wp-model ref,real \ -wp-model ref,real \
-wp-prover alt-ergo,z3,cvc4 \ -wp-prover alt-ergo,z3,cvc4 \
-wp-timeout $TIMEOUT \
-wp-par 16 \ -wp-par 16 \
-wp-no-warn-memory-model \ -wp-no-warn-memory-model \
${STRATEGIES} \ ${STRATEGIES} \
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment