Skip to content

Commit e77e490

Browse files
AllanBlanchardAllanBlanchard
authored
Merge pull request #73 from AllanBlanchard/33-arsenic
Update tests for 33 arsenic (dev version)
2 parents 278370d + 2c81b4e commit e77e490

299 files changed

Lines changed: 728 additions & 846 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/workflows/ci.yml‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -42,8 +42,6 @@ jobs:
4242
runs-on: ubuntu-latest
4343
container: allanblanchardgh/tutoriel_wp:frama-c
4444
steps:
45-
- name: Check Why3
46-
run: cat /root/.why3.conf && why3 config detect
4745
- name: retrieve sources
4846
uses: actions/checkout@v4
4947
- name: execute

‎code/Dockerfile‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,8 @@ RUN apt-get update && apt-get install -y \
1717
tar \
1818
unzip \
1919
wget \
20-
which
20+
which \
21+
z3
2122

2223
RUN opam init -c 4.14.2 --disable-sandboxing
2324

@@ -37,7 +38,8 @@ RUN opam install --confirm-level=unsafe-yes \
3738
zarith \
3839
ppx_deriving \
3940
ppx_deriving_yojson \
40-
ppx_deriving_yaml
41+
ppx_deriving_yaml \
42+
ppx_inline_test
4143

4244
ENV HOME="/root"
4345

@@ -49,5 +51,3 @@ ENV PATH="$OPAM_SWITCH_PREFIX/bin:$PATH"
4951
RUN wget https://git.frama-c.com/pub/frama-c/-/archive/master/frama-c-master.tar.gz
5052
RUN tar xzf frama-c-master.tar.gz
5153
RUN make PREFIX=$OPAM_SWITCH_PREFIX RELEASE=yes -C frama-c-master install
52-
53-
RUN why3 config detect

code/acsl-logic-definitions/answers/oracle/max_subarray-1.res.oracle renamed to code/acsl-logic-definitions/answers/oracle/max_subarray-1.0.res.oracle

File renamed without changes.

code/acsl-logic-definitions/answers/oracle/sort-1.res.oracle renamed to code/acsl-logic-definitions/answers/oracle/sort-1.0.res.oracle

File renamed without changes.

code/acsl-logic-definitions/axiomatic/oracle/all-zeroes-bad.res.oracle renamed to code/acsl-logic-definitions/axiomatic/oracle/all-zeroes-bad.0.res.oracle

File renamed without changes.

code/acsl-logic-definitions/axiomatic/oracle/cluster.res.oracle renamed to code/acsl-logic-definitions/axiomatic/oracle/cluster.0.res.oracle

File renamed without changes.

code/acsl-logic-definitions/axiomatic/oracle/ex-1-occurrences_of-answer.res.oracle renamed to code/acsl-logic-definitions/axiomatic/oracle/ex-1-occurrences_of-answer.0.res.oracle

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -6,19 +6,19 @@
66
[wp] [Valid] Goal occurrences_of_terminates (Cfg) (Trivial)
77
[wp] 14 goals scheduled
88
[wp] [Valid] typed_occurrences_of_ensures (Qed)
9-
[wp] [Valid] typed_occurrences_of_loop_invariant_preserved (Alt-Ergo) (Cached)
109
[wp] [Valid] typed_occurrences_of_loop_invariant_established (Qed)
11-
[wp] [Valid] typed_occurrences_of_loop_invariant_2_preserved (Alt-Ergo) (Cached)
10+
[wp] [Valid] typed_occurrences_of_loop_invariant_preserved (Alt-Ergo) (Cached)
1211
[wp] [Valid] typed_occurrences_of_loop_invariant_2_established (Qed)
13-
[wp] [Valid] typed_occurrences_of_loop_invariant_3_preserved (Alt-Ergo) (Cached)
12+
[wp] [Valid] typed_occurrences_of_loop_invariant_2_preserved (Alt-Ergo) (Cached)
1413
[wp] [Valid] typed_occurrences_of_loop_invariant_3_established (Alt-Ergo) (Cached)
14+
[wp] [Valid] typed_occurrences_of_loop_invariant_3_preserved (Alt-Ergo) (Cached)
1515
[wp] [Valid] typed_occurrences_of_assert_rte_mem_access (Alt-Ergo) (Cached)
1616
[wp] [Valid] typed_occurrences_of_loop_assigns_part1 (Qed)
1717
[wp] [Valid] typed_occurrences_of_loop_assigns_part2 (Qed)
1818
[wp] [Valid] typed_occurrences_of_loop_assigns_part3 (Qed)
1919
[wp] [Valid] typed_occurrences_of_assigns (Qed)
20-
[wp] [Valid] typed_occurrences_of_loop_variant_decrease (Alt-Ergo) (Cached)
2120
[wp] [Valid] typed_occurrences_of_loop_variant_positive (Qed)
21+
[wp] [Valid] typed_occurrences_of_loop_variant_decrease (Alt-Ergo) (Cached)
2222
[wp] Proved goals: 16 / 16
2323
Terminating: 1
2424
Unreachable: 1

code/acsl-logic-definitions/axiomatic/oracle/ex-1-occurrences_of.res.oracle renamed to code/acsl-logic-definitions/axiomatic/oracle/ex-1-occurrences_of.0.res.oracle

File renamed without changes.

code/acsl-logic-definitions/inductive/oracle/ex-2-gcd-answer.res.oracle renamed to code/acsl-logic-definitions/axiomatic/oracle/ex-2-gcd-answer.0.res.oracle

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,16 +6,16 @@
66
[wp] [Valid] Goal gcd_terminates (Cfg) (Trivial)
77
[wp] 11 goals scheduled
88
[wp] [Valid] typed_gcd_ensures (Alt-Ergo) (Cached)
9-
[wp] [Valid] typed_gcd_loop_invariant_preserved (Alt-Ergo) (Cached)
109
[wp] [Valid] typed_gcd_loop_invariant_established (Qed)
11-
[wp] [Valid] typed_gcd_loop_invariant_2_preserved (Alt-Ergo) (Cached)
10+
[wp] [Valid] typed_gcd_loop_invariant_preserved (Alt-Ergo) (Cached)
1211
[wp] [Valid] typed_gcd_loop_invariant_2_established (Qed)
12+
[wp] [Valid] typed_gcd_loop_invariant_2_preserved (Alt-Ergo) (Cached)
1313
[wp] [Valid] typed_gcd_assert_rte_division_by_zero (Qed)
1414
[wp] [Valid] typed_gcd_assert_rte_signed_overflow (Alt-Ergo) (Cached)
1515
[wp] [Valid] typed_gcd_loop_assigns (Qed)
1616
[wp] [Valid] typed_gcd_assigns (Qed)
17-
[wp] [Valid] typed_gcd_loop_variant_decrease (Alt-Ergo) (Cached)
1817
[wp] [Valid] typed_gcd_loop_variant_positive (Qed)
18+
[wp] [Valid] typed_gcd_loop_variant_decrease (Alt-Ergo) (Cached)
1919
[wp] Proved goals: 13 / 13
2020
Terminating: 1
2121
Unreachable: 1

code/acsl-logic-definitions/axiomatic/oracle/ex-2-gcd.res.oracle renamed to code/acsl-logic-definitions/axiomatic/oracle/ex-2-gcd.0.res.oracle

File renamed without changes.

0 commit comments

Comments
 (0)