Merge pull request #68 from AllanBlanchard/pdfs-ci

PDFs in separate CIs + use latex image
AllanBlanchard · Nov 2, 2024 · 0a2b4db · 0a2b4db
2 parents 5fd3cee + 518ba9f
commit 0a2b4db
Show file tree

Hide file tree

Showing 18 changed files with 103 additions and 52 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -0,0 +1,50 @@
+name: CI
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+
+jobs:
+  compile-en:
+    name: EN version
+    runs-on: ubuntu-latest
+    container: allanblanchardgh/tutoriel_wp:latex
+    steps:
+      - name: retrieve sources
+        uses: actions/checkout@v4
+      - name: compile
+        run: make -C english
+      - name: archive PDFs
+        uses: actions/upload-artifact@v4
+        with:
+          name: frama-c-wp-tutorial-en.pdf
+          path: english/main.pdf
+
+  compile-fr:
+    name: FR version
+    runs-on: ubuntu-latest
+    container: allanblanchardgh/tutoriel_wp:latex
+    steps:
+      - name: retrieve sources
+        uses: actions/checkout@v4
+      - name: compile
+        run: make -C french
+      - name: archive PDFs
+        uses: actions/upload-artifact@v4
+        with:
+          name: frama-c-wp-tutoriel-fr.pdf
+          path: french/main.pdf
+
+  check-code:
+    name: Check code
+    runs-on: ubuntu-latest
+    container: allanblanchardgh/tutoriel_wp:frama-c
+    steps:
+      - name: Check Why3
+        run: cat /root/.why3.conf && why3 config detect
+      - name: retrieve sources
+        uses: actions/checkout@v4
+      - name: execute
+        run: cd code ; make
diff --git a/.github/workflows/pdfs.yml b/.github/workflows/pdfs.yml
diff --git a/code/acsl-logic-definitions/inductive/even-0.c b/code/acsl-logic-definitions/inductive/even-0.c
@@ -1,5 +1,5 @@
 /* run.config
-   STDOPT:+"-wp-prover alt-ergo,z3"
+   STDOPT:+"-wp-timeout 5"
 */
 
 /*@

diff --git a/code/acsl-logic-definitions/inductive/oracle/even-0.res.oracle b/code/acsl-logic-definitions/inductive/oracle/even-0.res.oracle
@@ -1,4 +1,4 @@
-# frama-c -wp -wp-rte [...]
+# frama-c -wp -wp-rte -wp-timeout 5 [...]
 [kernel] Parsing even-0.c (with preprocessing)
 [wp] Running WP plugin...
 [rte:annot] annotating function bar

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/code/statements/loops/check-admit-invariant.c b/code/statements/loops/check-admit-invariant.c
@@ -1,5 +1,5 @@
 /* run.config
-   OPT: -wp -wp-print -wp-no-let -wp-prover qed -wp-prop="C3,I4"
+   OPT: -wp -wp-print -wp-no-let -wp-prover qed -wp-prop="C3,I4" -wp-msg-key shell
 */
 
 int main(void) {

diff --git a/code/statements/loops/oracle/check-admit-invariant.res.oracle b/code/statements/loops/oracle/check-admit-invariant.res.oracle
@@ -1,7 +1,12 @@
+# frama-c -wp [...]
 [kernel] Parsing check-admit-invariant.c (with preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
 [wp] 4 goals scheduled
+[wp] [Valid] typed_main_check_loop_invariant_C3_preserved (Qed)
+[wp] [Valid] typed_main_check_loop_invariant_C3_established (Qed)
+[wp] [Valid] typed_main_loop_invariant_I4_preserved (Qed)
+[wp] [Valid] typed_main_loop_invariant_I4_established (Qed)
 [wp] Proved goals:    4 / 4
   Qed:             4
 ------------------------------------------------------------

diff --git a/code/statements/loops/oracle/two-loop-invariants.res.oracle b/code/statements/loops/oracle/two-loop-invariants.res.oracle
@@ -1,21 +1,27 @@
+# frama-c -wp [...]
 [kernel] Parsing two-loop-invariants.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] [Valid] Goal main_exits (Cfg) (Unreachable)
 [wp] Warning: Missing RTE guards
 [wp] 6 goals scheduled
-[wp] [Unknown] typed_main_terminates (Qed)
-[wp] [Unknown] typed_main_loop_invariant_I1_preserved (Qed)
+[wp] [Unsuccess] typed_main_terminates (Qed)
+[wp] [Unsuccess] typed_main_loop_invariant_I1_preserved (Qed)
+[wp] [Valid] typed_main_loop_invariant_I1_established (Qed)
+[wp] [Valid] typed_main_loop_invariant_I2_preserved (Qed)
+[wp] [Valid] typed_main_loop_invariant_I2_established (Qed)
+[wp] [Valid] typed_main_loop_assigns (Qed)
 [wp] Proved goals:    5 / 7
   Unreachable:     1
   Qed:             4
-  Unknown:         2
+  Unsuccess:       2
 ------------------------------------------------------------
   Function main
 ------------------------------------------------------------
 
 Goal Termination-condition (generated) in 'main':
 Loop termination at line 12
 Prove: false.
-Prover Qed returns Unknown
+Prover Qed returns Unsuccess
 
 ------------------------------------------------------------
 
@@ -41,7 +47,7 @@ Assume {
   Have: (1 + x_1) = x.
 }
 Prove: 0 <= x.
-Prover Qed returns Unknown
+Prover Qed returns Unsuccess
 
 ------------------------------------------------------------
 

diff --git a/code/statements/loops/two-loop-invariants.c b/code/statements/loops/two-loop-invariants.c
@@ -1,5 +1,5 @@
 /* run.config
-   OPT: -wp -wp-print -wp-no-let -wp-prover qed
+   OPT: -wp -wp-print -wp-no-let -wp-prover qed -wp-msg-key shell
 */
 
 int main(void){

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[5]{c}{ex-2-terminates.c}
 
 
 Explain why termination clauses are verified or not. Modify the specification so

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[5]{c}{ex-2-terminates.c}
 
 
 Expliquer pourquoi les clauses de terminaison sont vérifiées ou pas. Modifier