diff --git a/scripts/frama-c-lustrec.sh b/scripts/frama-c-lustrec.sh index 1577af1453eec82994cb15f60833ac3fddce08a1..346ad14b76ce0c8147bce7b21eb3fbdb373d300d 100755 --- a/scripts/frama-c-lustrec.sh +++ b/scripts/frama-c-lustrec.sh @@ -2,7 +2,7 @@ # simple shell script to launch Frama-C with the right options to # prove C files generated by LustreC. -# look at the usage function for more explanations +# see the usage function for more explanations # usage function usage () { @@ -11,12 +11,13 @@ usage () { echo " - [-h|--help] | prints this message and exits" echo " - [-g|--gui] | use Frama-C GUI" 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 " Frama-C is launched with the following options:" echo " -wp | use WP plugin" 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-timeout $TIMEOUT | set solvers timeout, default to 30s" echo " -wp-par 16 | use 16 jobs at most" 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" @@ -68,6 +69,7 @@ done frama-c${GUI} -wp \ -wp-model ref,real \ -wp-prover alt-ergo,z3,cvc4 \ + -wp-timeout $TIMEOUT \ -wp-par 16 \ -wp-no-warn-memory-model \ ${STRATEGIES} \