occurrences_of.0.res.oracle

# frama-c -wp -wp-rte [...]
[kernel] Parsing occurrences_of.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 occurrences_of
[wp] [Valid] Goal occurrences_of_exits (Cfg) (Unreachable)
[wp] [Valid] Goal occurrences_of_terminates (Cfg) (Trivial)
[wp] 12 goals scheduled
[wp] [Valid] typed_occurrences_of_ensures (Qed)
[wp] [Valid] typed_occurrences_of_loop_invariant_established (Qed)
[wp] [Valid] typed_occurrences_of_loop_invariant_preserved (Alt-Ergo) (Cached)
[wp] [Valid] typed_occurrences_of_loop_invariant_2_established (Alt-Ergo) (Cached)
[wp] [Valid] typed_occurrences_of_loop_invariant_2_preserved (Alt-Ergo) (Cached)
[wp] [Valid] typed_occurrences_of_assert_rte_mem_access (Alt-Ergo) (Cached)
[wp] [Valid] typed_occurrences_of_loop_assigns_part1 (Qed)
[wp] [Valid] typed_occurrences_of_loop_assigns_part2 (Qed)
[wp] [Valid] typed_occurrences_of_loop_assigns_part3 (Qed)
[wp] [Valid] typed_occurrences_of_assigns (Qed)
[wp] [Valid] typed_occurrences_of_loop_variant_positive (Qed)
[wp] [Valid] typed_occurrences_of_loop_variant_decrease (Alt-Ergo) (Cached)
[wp] Proved goals:   14 / 14
  Terminating:     1
  Unreachable:     1
  Qed:             7
  Alt-Ergo:        5