[kernel] Warning: your preprocessor is not known to handle option `-nostdinc'. If pre-processing fails because of it, please add -no-cpp-frama-c-compliant option to Frama-C's command-line. If you do not want to see this warning again, explicitly use option -cpp-frama-c-compliant.
[kernel] Warning: your preprocessor is not known to handle option `-dD'. If pre-processing fails because of it, please add -no-cpp-frama-c-compliant option to Frama-C's command-line. If you do not want to see this warning again, explicitly use option -cpp-frama-c-compliant.
[kernel] Parsing list.c (with preprocessing)
[kernel] Warning: trying to preprocess annotation with an unknown preprocessor.
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] Computing [100 goals...]
[wp] Computing [200 goals...]
[wp] Computing [300 goals...]
[wp] Computing [400 goals...]
[wp] Computing [500 goals...]
[wp] Computing [600 goals...]
[wp] Computing [700 goals...]
[wp] Computing [800 goals...]
[wp] 817 goals scheduled
[wp] [Qed] Goal typed_list_init_post_GhostSeparation : Valid
[wp] [Qed] Goal typed_list_init_post_ValidArray : Valid
[wp] [Qed] Goal typed_list_init_assign : Valid
[wp] [Qed] Goal typed_list_init_post_3 : Valid
[wp] [Qed] Goal typed_list_head_empty_post : Valid
[wp] [Qed] Goal typed_list_head_assign : Valid
[wp] [Qed] Goal typed_list_tail_complete_not_empty_empty : Valid
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /root/.opam/frama-c/share/frama-c/wp/why3/why3.conf
No prover in /root/.why3.conf corresponds to "cvc4-15"

------------------------------------------------------------
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /root/.opam/frama-c/share/frama-c/wp/why3/why3.conf
No prover in /root/.why3.conf corresponds to "cvc4-15"

------------------------------------------------------------
[wp] [Qed] Goal typed_list_tail_disjoint_not_empty_empty : Valid
[wp] [Alt-Ergo] Goal typed_list_init_post_2 : Valid
[wp] [Alt-Ergo] Goal typed_list_init_post : Valid
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /root/.opam/frama-c/share/frama-c/wp/why3/why3.conf
No prover in /root/.why3.conf corresponds to "cvc4-15"

------------------------------------------------------------
[wp] [Failed] Goal typed_list_head_not_empty_post
   cvc4-15: Failed Why3 exits with status 1.
  Alt-Ergo: Unknown (Qed:7ms) (82ms)
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /root/.opam/frama-c/share/frama-c/wp/why3/why3.conf
No prover in /root/.why3.conf corresponds to "cvc4-15"

------------------------------------------------------------
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /root/.opam/frama-c/share/frama-c/wp/why3/why3.conf
No prover in /root/.why3.conf corresponds to "cvc4-15"

------------------------------------------------------------
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /root/.opam/frama-c/share/frama-c/wp/why3/why3.conf
No prover in /root/.why3.conf corresponds to "cvc4-15"

------------------------------------------------------------
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /root/.opam/frama-c/share/frama-c/wp/why3/why3.conf
No prover in /root/.why3.conf corresponds to "cvc4-15"

------------------------------------------------------------
[wp] [Failed] Goal typed_list_tail_loop_inv_established
   cvc4-15: Failed Why3 exits with status 1.
  Alt-Ergo: Unknown (Qed:0.82ms) (156ms)
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /root/.opam/frama-c/share/frama-c/wp/why3/why3.conf
No prover in /root/.why3.conf corresponds to "cvc4-15"

------------------------------------------------------------
[wp] [Failed] Goal typed_list_tail_loop_inv_2_established
   cvc4-15: Failed Why3 exits with status 1.
  Alt-Ergo: Unknown (Qed:0.95ms) (156ms)
[wp] [Qed] Goal typed_list_tail_loop_inv_4_established : Valid
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /root/.opam/frama-c/share/frama-c/wp/why3/why3.conf
No prover in /root/.why3.conf corresponds to "cvc4-15"

------------------------------------------------------------
[wp] [Qed] Goal typed_list_tail_assert : Valid
[wp] [Failed] Goal typed_list_tail_loop_inv_3_established
   cvc4-15: Failed Why3 exits with status 1.
  Alt-Ergo: Unknown (Qed:0.83ms) (160ms)
[wp] [Qed] Goal typed_list_tail_assign_part1 : Valid
[wp] [Qed] Goal typed_list_tail_loop_assign : Valid
[wp] [Qed] Goal typed_list_tail_assign_part3 : Valid
[wp] [Qed] Goal typed_list_tail_assign_part2 : Valid
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /root/.opam/frama-c/share/frama-c/wp/why3/why3.conf
No prover in /root/.why3.conf corresponds to "cvc4-15"

------------------------------------------------------------
[wp] [Qed] Goal typed_list_tail_loop_term_decrease : Valid
[wp] [Qed] Goal typed_list_tail_assign_part4 : Valid
[wp] [Failed] Goal typed_list_tail_loop_inv_preserved
   cvc4-15: Failed Why3 exits with status 1.
  Alt-Ergo: Unknown (Qed:4ms) (568ms)
[wp] [Qed] Goal typed_list_tail_empty_post : Valid
[wp] [Qed] Goal typed_list_tail_loop_term_positive : Valid
[wp] [Failed] Goal typed_list_tail_loop_inv_2_preserved
   cvc4-15: Failed Why3 exits with status 1.
  Alt-Ergo: Unknown (Qed:2ms) (727ms)
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /root/.opam/frama-c/share/frama-c/wp/why3/why3.conf
No prover in /root/.why3.conf corresponds to "cvc4-15"

------------------------------------------------------------
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /root/.opam/frama-c/share/frama-c/wp/why3/why3.conf
No prover in /root/.why3.conf corresponds to "cvc4-15"

------------------------------------------------------------
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /root/.opam/frama-c/share/frama-c/wp/why3/why3.conf
No prover in /root/.why3.conf corresponds to "cvc4-15"

------------------------------------------------------------
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /root/.opam/frama-c/share/frama-c/wp/why3/why3.conf
No prover in /root/.why3.conf corresponds to "cvc4-15"

------------------------------------------------------------
[wp] [Alt-Ergo] Goal typed_list_pop_disjoint_more_empty : Valid
[wp] [Qed] Goal typed_list_pop_post : Valid
[wp] [Failed] Goal typed_list_tail_loop_inv_4_preserved
   cvc4-15: Failed Why3 exits with status 1.
  Alt-Ergo: Unknown (Qed:2ms) (960ms)
[wp] [Qed] Goal typed_list_pop_post_GhostSeparation : Valid
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /root/.opam/frama-c/share/frama-c/wp/why3/why3.conf
No prover in /root/.why3.conf corresponds to "cvc4-15"

------------------------------------------------------------
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /root/.opam/frama-c/share/frama-c/wp/why3/why3.conf
No prover in /root/.why3.conf corresponds to "cvc4-15"

------------------------------------------------------------
[wp] [Qed] Goal typed_list_pop_assert : Valid
[wp] [Qed] Goal typed_list_pop_assert_2 : Valid
[wp] [Qed] Goal typed_list_pop_assert_3 : Valid
[wp] [Failed] Goal typed_list_pop_complete_more_empty
   cvc4-15: Failed Why3 exits with status 1.
  Alt-Ergo: Unknown (Qed:3ms) (916ms)
[wp] [Qed] Goal typed_list_pop_assert_4 : Valid
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /root/.opam/frama-c/share/frama-c/wp/why3/why3.conf
No prover in /root/.why3.conf corresponds to "cvc4-15"

------------------------------------------------------------
[wp] [Failed] Goal typed_list_pop_empty_post
   cvc4-15: Failed Why3 exits with status 1.
  Alt-Ergo: Unknown (Qed:3ms) (152ms)
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /root/.opam/frama-c/share/frama-c/wp/why3/why3.conf
No prover in /root/.why3.conf corresponds to "cvc4-15"

------------------------------------------------------------
[wp] [Failed] Goal typed_list_tail_loop_inv_3_preserved
   cvc4-15: Failed Why3 exits with status 1.
  Alt-Ergo: Unknown (Qed:2ms) (2.5s)
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /root/.opam/frama-c/share/frama-c/wp/why3/why3.conf
No prover in /root/.why3.conf corresponds to "cvc4-15"

------------------------------------------------------------
[wp] [Alt-Ergo] Goal typed_list_pop_empty_post_3 : Valid
[wp] [Failed] Goal typed_list_pop_empty_post_2
   cvc4-15: Failed Why3 exits with status 1.
  Alt-Ergo: Unknown (Qed:3ms) (410ms)
[wp] [Qed] Goal typed_list_pop_empty_post_Unique : Valid
[wp] [Qed] Goal typed_list_pop_empty_post_Separation : Valid
[wp] [Qed] Goal typed_list_pop_empty_post_Separation_2 : Valid
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /root/.opam/frama-c/share/frama-c/wp/why3/why3.conf
No prover in /root/.why3.conf corresponds to "cvc4-15"

------------------------------------------------------------
[wp] [Qed] Goal typed_list_pop_empty_assign_part1 : Valid
[wp] [Failed] Goal typed_list_pop_empty_post_4
   cvc4-15: Failed Why3 exits with status 1.
  Alt-Ergo: Unknown (Qed:1ms) (152ms)
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /root/.opam/frama-c/share/frama-c/wp/why3/why3.conf
No prover in /root/.why3.conf corresponds to "cvc4-15"

------------------------------------------------------------
[wp] [Failed] Goal typed_list_pop_empty_assign_part2
   cvc4-15: Failed Why3 exits with status 1.
  Alt-Ergo: Unknown (Qed:0.76ms) (154ms)
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /root/.opam/frama-c/share/frama-c/wp/why3/why3.conf
No prover in /root/.why3.conf corresponds to "cvc4-15"

------------------------------------------------------------
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /root/.opam/frama-c/share/frama-c/wp/why3/why3.conf
No prover in /root/.why3.conf corresponds to "cvc4-15"

------------------------------------------------------------
[wp] [Failed] Goal typed_list_tail_not_empty_post_3
   cvc4-15: Failed Why3 exits with status 1.
  Alt-Ergo: Unknown (Qed:3ms) (3.8s)
[wp] [Failed] Goal typed_list_tail_not_empty_post
   cvc4-15: Failed Why3 exits with status 1.
  Alt-Ergo: Unknown (Qed:3ms) (4s)
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /root/.opam/frama-c/share/frama-c/wp/why3/why3.conf
No prover in /root/.why3.conf corresponds to "cvc4-15"

------------------------------------------------------------
[wp] [Failed] Goal typed_list_pop_post_3
   cvc4-15: Failed Why3 exits with status 1.
  Alt-Ergo: Unknown (Qed:5ms) (3.2s)
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /root/.opam/frama-c/share/frama-c/wp/why3/why3.conf
No prover in /root/.why3.conf corresponds to "cvc4-15"

------------------------------------------------------------
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /root/.opam/frama-c/share/frama-c/wp/why3/why3.conf
No prover in /root/.why3.conf corresponds to "cvc4-15"

------------------------------------------------------------
[wp] [Failed] Goal typed_list_pop_more_post
   cvc4-15: Failed Why3 exits with status 1.
  Alt-Ergo: Unknown (Qed:5ms) (1.9s)
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /root/.opam/frama-c/share/frama-c/wp/why3/why3.conf
No prover in /root/.why3.conf corresponds to "cvc4-15"

------------------------------------------------------------
