From 3b4824989e615841a838899f2bb29a27a4143c24 Mon Sep 17 00:00:00 2001
From: Christophe Garion <tofgarion@runbox.com>
Date: Thu, 23 Feb 2023 11:54:11 +0100
Subject: [PATCH] [scripts] typos in frama-c-lustrec.sh script
---
scripts/frama-c-lustrec.sh | 6 ++++--
1 file changed, 4 insertions(+), 2 deletions(-)
diff --git a/scripts/frama-c-lustrec.sh b/scripts/frama-c-lustrec.sh
index 1577af14..346ad14b 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} \
--
GitLab