More stable tests

AllanBlanchard · Nov 2, 2024 · 3986dae · 3986dae
1 parent fe884fc
commit 3986dae
Show file tree

Hide file tree

Showing 14 changed files with 41 additions and 33 deletions.
diff --git a/code/acsl-logic-definitions/inductive/even-0.c b/code/acsl-logic-definitions/inductive/even-0.c
@@ -1,7 +1,3 @@
-/* run.config
-   STDOPT:+"-wp-prover alt-ergo,z3"
-*/
-
 /*@
   inductive even_natural{L}(integer n) {
   case even_nul{L}:

diff --git a/code/acsl-logic-definitions/inductive/oracle/even-0.res.oracle b/code/acsl-logic-definitions/inductive/oracle/even-0.res.oracle
@@ -16,9 +16,9 @@
   Unreachable:     2
   Alt-Ergo:        2
   Unsuccess:       1
-[wp:pedantic-assigns] even-0.c:15: Warning: 
+[wp:pedantic-assigns] even-0.c:11: Warning: 
   No 'assigns' specification for function 'foo'.
   Callers assumptions might be imprecise.
-[wp:pedantic-assigns] even-0.c:20: Warning: 
+[wp:pedantic-assigns] even-0.c:16: Warning: 
   No 'assigns' specification for function 'bar'.
   Callers assumptions might be imprecise.
diff --git a/code/function-contract/modularity/ex-4-change-answer.c b/code/function-contract/modularity/ex-4-change-answer.c
@@ -1,3 +1,7 @@
+/* run.config
+   STDOPT:+"-wp-timeout 5"
+*/
+
 enum note { N500, N200, N100, N50, N20, N10, N5, N2, N1 };
 int const values[] = { 500, 200, 100, 50, 20, 10, 5, 2, 1 };
 

diff --git a/code/function-contract/modularity/oracle/ex-4-change-answer.res.oracle b/code/function-contract/modularity/oracle/ex-4-change-answer.res.oracle
@@ -1,4 +1,4 @@
-# frama-c -wp -wp-rte [...]
+# frama-c -wp -wp-rte -wp-timeout 5 [...]
 [kernel] Parsing ex-4-change-answer.c (with preprocessing)
 [wp] Running WP plugin...
 [rte:annot] annotating function make_change
@@ -99,12 +99,12 @@
   Unreachable:     1
   Qed:            61
   Alt-Ergo:       27
-[wp] ex-4-change-answer.c:11: Warning: 
+[wp] ex-4-change-answer.c:15: Warning: 
   Memory model hypotheses for function 'remove_max_notes':
   /*@ behavior wp_typed:
         requires \separated(rest, (int const *)values + (..)); */
   int remove_max_notes(enum note n, int *rest);
-[wp] ex-4-change-answer.c:53: Warning: 
+[wp] ex-4-change-answer.c:57: Warning: 
   Memory model hypotheses for function 'make_change':
   /*@
      behavior wp_typed:

diff --git a/code/proof-methodologies/triggering-lemmas/insert_sort-proved.c b/code/proof-methodologies/triggering-lemmas/insert_sort-proved.c
@@ -1,6 +1,6 @@
 /* run.config
    DEPS: @PTEST_DEPS@ @PTEST_DIR@/@PTEST_NAME@.@[email protected]@PTEST_CONFIG@/interactive/*.v
-   STDOPT:+"-wp-prover alt-ergo,coq -warn-unsigned-overflow -warn-unsigned-downcast -wp-session @PTEST_DIR@/@PTEST_NAME@.@[email protected]@PTEST_CONFIG@"
+   STDOPT:+"-wp-timeout 5 -wp-prover alt-ergo,coq -warn-unsigned-overflow -warn-unsigned-downcast -wp-session @PTEST_DIR@/@PTEST_NAME@.@[email protected]@PTEST_CONFIG@"
 */
 
 #include <stddef.h>

diff --git a/code/proof-methodologies/triggering-lemmas/oracle/insert_sort-proved.res.oracle b/code/proof-methodologies/triggering-lemmas/oracle/insert_sort-proved.res.oracle
@@ -1,4 +1,4 @@
-# frama-c -wp -wp-rte -warn-unsigned-overflow -warn-unsigned-downcast [...]
+# frama-c -wp -wp-rte -wp-timeout 5 -warn-unsigned-overflow -warn-unsigned-downcast [...]
 [kernel] Parsing insert_sort-proved.c (with preprocessing)
 [wp] Running WP plugin...
 [rte:annot] annotating function insert

diff --git a/code/statements/function-calls/ex-2-terminates-answer.c b/code/statements/function-calls/ex-2-terminates-answer.c
@@ -1,3 +1,7 @@
+/* run.config
+   STDOPT:+"-wp-timeout 5"
+*/
+
 #include <limits.h>
 #include <stddef.h>
 

diff --git a/code/statements/function-calls/ex-2-terminates.c b/code/statements/function-calls/ex-2-terminates.c
@@ -1,3 +1,7 @@
+/* run.config
+   STDOPT:+"-wp-timeout 5"
+*/
+
 #include <limits.h>
 #include <stddef.h>
 

diff --git a/code/statements/function-calls/oracle/ex-2-terminates-answer.res.oracle b/code/statements/function-calls/oracle/ex-2-terminates-answer.res.oracle
@@ -1,14 +1,14 @@
-# frama-c -wp -wp-rte [...]
+# frama-c -wp -wp-rte -wp-timeout 5 [...]
 [kernel] Parsing ex-2-terminates-answer.c (with preprocessing)
 [wp] Running WP plugin...
 [rte:annot] annotating function abs
 [rte:annot] annotating function distance
 [rte:annot] annotating function distances
 [rte:annot] annotating function prepare
-[kernel:annot:missing-spec] ex-2-terminates-answer.c:52: Warning: 
+[kernel:annot:missing-spec] ex-2-terminates-answer.c:56: Warning: 
   Neither code nor explicit exits for function initialize,
    generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] ex-2-terminates-answer.c:59: Warning: 
+[kernel:annot:missing-spec] ex-2-terminates-answer.c:63: Warning: 
   Neither code nor explicit exits for function connect,
    generating default clauses. See -generated-spec-* options for more info
 [rte:annot] annotating function terminates_f1
@@ -17,9 +17,9 @@
 [wp] [Valid] Goal abs_terminates (Cfg) (Trivial)
 [wp] [Valid] Goal terminates_f1_exits (Cfg) (Unreachable)
 [wp] [Valid] Goal terminates_f2_exits (Cfg) (Unreachable)
-[wp] ex-2-terminates-answer.c:73: Warning: 
+[wp] ex-2-terminates-answer.c:77: Warning: 
   Missing assigns clause (assigns 'everything' instead)
-[wp] ex-2-terminates-answer.c:80: Warning: 
+[wp] ex-2-terminates-answer.c:84: Warning: 
   Missing assigns clause (assigns 'everything' instead)
 [wp] 46 goals scheduled
 [wp] [Valid] typed_abs_ensures (Qed)
@@ -73,9 +73,9 @@
   Unreachable:     3
   Qed:            35
   Alt-Ergo:       11
-[wp:pedantic-assigns] ex-2-terminates-answer.c:72: Warning: 
+[wp:pedantic-assigns] ex-2-terminates-answer.c:76: Warning: 
   No 'assigns' specification for function 'terminates_f1'.
   Callers assumptions might be imprecise.
-[wp:pedantic-assigns] ex-2-terminates-answer.c:79: Warning: 
+[wp:pedantic-assigns] ex-2-terminates-answer.c:83: Warning: 
   No 'assigns' specification for function 'terminates_f2'.
   Callers assumptions might be imprecise.
diff --git a/code/statements/function-calls/oracle/ex-2-terminates.res.oracle b/code/statements/function-calls/oracle/ex-2-terminates.res.oracle
@@ -1,14 +1,14 @@
-# frama-c -wp -wp-rte [...]
+# frama-c -wp -wp-rte -wp-timeout 5 [...]
 [kernel] Parsing ex-2-terminates.c (with preprocessing)
 [wp] Running WP plugin...
 [rte:annot] annotating function abs
 [rte:annot] annotating function distance
 [rte:annot] annotating function distances
 [rte:annot] annotating function prepare
-[kernel:annot:missing-spec] ex-2-terminates.c:51: Warning: 
+[kernel:annot:missing-spec] ex-2-terminates.c:55: Warning: 
   Neither code nor explicit exits for function initialize,
    generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] ex-2-terminates.c:58: Warning: 
+[kernel:annot:missing-spec] ex-2-terminates.c:62: Warning: 
   Neither code nor explicit exits for function connect,
    generating default clauses. See -generated-spec-* options for more info
 [rte:annot] annotating function terminates_f1
@@ -17,9 +17,9 @@
 [wp] [Valid] Goal abs_terminates (Cfg) (Trivial)
 [wp] [Valid] Goal terminates_f1_exits (Cfg) (Unreachable)
 [wp] [Valid] Goal terminates_f2_exits (Cfg) (Unreachable)
-[wp] ex-2-terminates.c:72: Warning: 
+[wp] ex-2-terminates.c:76: Warning: 
   Missing assigns clause (assigns 'everything' instead)
-[wp] ex-2-terminates.c:79: Warning: 
+[wp] ex-2-terminates.c:83: Warning: 
   Missing assigns clause (assigns 'everything' instead)
 [wp] 45 goals scheduled
 [wp] [Valid] typed_abs_ensures (Qed)
@@ -73,9 +73,9 @@
   Qed:            33
   Alt-Ergo:       10
   Unsuccess:       2
-[wp:pedantic-assigns] ex-2-terminates.c:71: Warning: 
+[wp:pedantic-assigns] ex-2-terminates.c:75: Warning: 
   No 'assigns' specification for function 'terminates_f1'.
   Callers assumptions might be imprecise.
-[wp:pedantic-assigns] ex-2-terminates.c:78: Warning: 
+[wp:pedantic-assigns] ex-2-terminates.c:82: Warning: 
   No 'assigns' specification for function 'terminates_f2'.
   Callers assumptions might be imprecise.
diff --git a/english/acsl-logic-definitions/inductive.tex b/english/acsl-logic-definitions/inductive.tex
@@ -31,7 +31,7 @@
 an even natural number'':
 
 
-\CodeBlockInput[5][13]{c}{even-0.c}
+\CodeBlockInput[1][9]{c}{even-0.c}
 
 
 Which describes the two cases:
@@ -44,7 +44,7 @@
 This can be used to prove the following assertions:
 
 
-\CodeBlockInput[15][18]{c}{even-0.c}
+\CodeBlockInput[11][14]{c}{even-0.c}
 
 
 Note that, since the solver has to recursively unfold the inductive definition,
@@ -58,7 +58,7 @@
 to the fact that the following assertion cannot be proved:
 
 
-\CodeBlockInput[20]{c}{even-0.c}
+\CodeBlockInput[16]{c}{even-0.c}
 
 
 

diff --git a/english/statements/function-calls.tex b/english/statements/function-calls.tex
@@ -772,7 +772,7 @@
 In the following program:
 
 
-\CodeBlockInput{c}{ex-2-terminates.c}
+\CodeBlockInput{c}[5]{ex-2-terminates.c}
 
 
 Explain why termination clauses are verified or not. Modify the specification so

diff --git a/french/acsl-logic-definitions/inductive.tex b/french/acsl-logic-definitions/inductive.tex
@@ -36,7 +36,7 @@
 naturel pair ».
 
 
-\CodeBlockInput[5][13]{c}{even-0.c}
+\CodeBlockInput[1][9]{c}{even-0.c}
 
 
 Ce prédicat définit bien les deux cas :
@@ -51,7 +51,7 @@
 Cette définition peut être utilisée pour prouver les assertions suivantes :
 
 
-\CodeBlockInput[15][18]{c}{even-0.c}
+\CodeBlockInput[11][14]{c}{even-0.c}
 
 
 Notons que, puisque le solveur doit récursivement dérouler la définition
@@ -66,7 +66,7 @@
 peut pas être prouvée :
 
 
-\CodeBlockInput[20]{c}{even-0.c}
+\CodeBlockInput[16]{c}{even-0.c}
 
 
 De plus, nous préférons généralement indiquer la condition selon laquelle une

diff --git a/french/statements/function-calls.tex b/french/statements/function-calls.tex
@@ -776,7 +776,7 @@
 Dans le programme suivant :
 
 
-\CodeBlockInput{c}{ex-2-terminates.c}
+\CodeBlockInput{c}[5]{ex-2-terminates.c}
 
 
 Expliquer pourquoi les clauses de terminaison sont vérifiées ou pas. Modifier