tutoriel_wp/code/acsl-logic-definitions/axiomatic/oracle/reset-1.0.res.oracle at bc7e5d6b7fe7f57bbc4342bf1aabd7e369e21c3e · AllanBlanchard/tutoriel_wp · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
# frama-c -wp -wp-rte [...]
[kernel] Parsing reset-1.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
[rte:annot] annotating function reset
[wp] [Valid] Goal reset_exits (Cfg) (Unreachable)
[wp] [Valid] Goal reset_terminates (Cfg) (Trivial)
[wp] 14 goals scheduled
[wp] [Valid] typed_lemma_no_changes (Coq) (Cached)
[wp] [Valid] typed_reset_ensures (Qed)
[wp] [Valid] typed_reset_loop_invariant_established (Qed)
[wp] [Valid] typed_reset_loop_invariant_preserved (Alt-Ergo) (Cached)
[wp] [Valid] typed_reset_loop_invariant_2_established (Alt-Ergo) (Cached)
[wp] [Valid] typed_reset_loop_invariant_2_preserved (Alt-Ergo) (Cached)
[wp] [Valid] typed_reset_assert_rte_mem_access (Alt-Ergo) (Cached)
[wp] [Valid] typed_reset_assert (Alt-Ergo) (Cached)
[wp] [Valid] typed_reset_loop_assigns_part1 (Qed)
[wp] [Valid] typed_reset_loop_assigns_part2 (Qed)
[wp] [Valid] typed_reset_loop_assigns_part3 (Alt-Ergo) (Cached)
[wp] [Valid] typed_reset_assigns (Qed)
[wp] [Valid] typed_reset_loop_variant_positive (Qed)
[wp] [Valid] typed_reset_loop_variant_decrease (Alt-Ergo) (Cached)
[wp] Proved goals:   16 / 16
  Terminating:     1
  Unreachable:     1
  Qed:             6
  Alt-Ergo:        7
  Coq:             1