-------------------------------------------------------------
TEST:  push_pop_empty
[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 user_code_tests/valid.c (with preprocessing)
[kernel] Warning: trying to preprocess annotation with an unknown preprocessor.
[kernel:typing:implicit-function-declaration] user_code_tests/valid.c:32: Warning: 
  Calling undeclared function array_find. Old style K&R code?
[wp] Running WP plugin...
[kernel:annot:missing-spec] user_code_tests/valid.c:468: Warning: 
  Neither code nor specification for function array_find, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 33 goals scheduled
[wp] [Qed] Goal typed_push_pop_empty_assert : Valid
[wp] [Qed] Goal typed_push_pop_empty_call_list_push_pre : Valid
[wp] [Qed] Goal typed_push_pop_empty_call_list_push_pre_3 : Valid
[wp] [Qed] Goal typed_push_pop_empty_call_list_push_pre_ValidArray : Valid
[wp] [Qed] Goal typed_push_pop_empty_call_list_push_pre_GhostSeparation : Valid
[wp] [Qed] Goal typed_push_pop_empty_call_list_push_pre_EnoughSpace : Valid
[wp] [Qed] Goal typed_push_pop_empty_call_list_push_pre_Item_Separation : Valid
[wp] [Qed] Goal typed_push_pop_empty_call_list_push_pre_GhostSeparation_2 : Valid
[wp] [Qed] Goal typed_push_pop_empty_call_list_push_pre_Separation_2 : Valid
[wp] [Qed] Goal typed_push_pop_empty_call_list_push_pre_Separation : Valid
[wp] [Qed] Goal typed_push_pop_empty_call_list_pop_pre_Linked : Valid
[wp] [Qed] Goal typed_push_pop_empty_call_list_pop_pre : Valid
[wp] [Qed] Goal typed_push_pop_empty_call_list_push_pre_Unique : Valid
[wp] [Qed] Goal typed_push_pop_empty_call_list_pop_pre_GhostSeparation : Valid
[wp] [Qed] Goal typed_push_pop_empty_call_list_pop_pre_2 : Valid
[wp] [Qed] Goal typed_push_pop_empty_call_list_pop_pre_ValidArray : Valid
[wp] [Qed] Goal typed_push_pop_empty_call_list_pop_pre_Separation : Valid
[wp] [Qed] Goal typed_push_pop_empty_call_list_pop_pre_4 : Valid
[wp] [Qed] Goal typed_push_pop_empty_call_list_pop_pre_3 : Valid
[wp] 33 goals generated
-------------------------------------------------------------
TEST:  push_chop_empty
[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 user_code_tests/valid.c (with preprocessing)
[kernel] Warning: trying to preprocess annotation with an unknown preprocessor.
[kernel:typing:implicit-function-declaration] user_code_tests/valid.c:32: Warning: 
  Calling undeclared function array_find. Old style K&R code?
[wp] Running WP plugin...
[kernel:annot:missing-spec] user_code_tests/valid.c:468: Warning: 
  Neither code nor specification for function array_find, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 32 goals scheduled
[wp] [Qed] Goal typed_push_chop_empty_assert : Valid
[wp] [Qed] Goal typed_push_chop_empty_post_TEST_3 : Valid
[wp] [Qed] Goal typed_push_chop_empty_call_list_push_pre : Valid
[wp] [Qed] Goal typed_push_chop_empty_call_list_push_pre_3 : Valid
[wp] [Qed] Goal typed_push_chop_empty_call_list_push_pre_ValidArray : Valid
[wp] [Qed] Goal typed_push_chop_empty_call_list_push_pre_GhostSeparation_2 : Valid
[wp] [Qed] Goal typed_push_chop_empty_call_list_push_pre_GhostSeparation : Valid
[wp] [Qed] Goal typed_push_chop_empty_call_list_push_pre_EnoughSpace : Valid
[wp] [Qed] Goal typed_push_chop_empty_call_list_push_pre_Separation : Valid
[wp] [Qed] Goal typed_push_chop_empty_call_list_push_pre_Item_Separation : Valid
[wp] [Qed] Goal typed_push_chop_empty_call_list_push_pre_Unique : Valid
[wp] [Qed] Goal typed_push_chop_empty_call_list_push_pre_Separation_2 : Valid
[wp] [Qed] Goal typed_push_chop_empty_call_list_chop_pre_3 : Valid
[wp] [Qed] Goal typed_push_chop_empty_call_list_chop_pre_2 : Valid
[wp] [Qed] Goal typed_push_chop_empty_call_list_chop_pre : Valid
[wp] [Qed] Goal typed_push_chop_empty_call_list_chop_pre_GhostSeparation_3 : Valid
[wp] [Qed] Goal typed_push_chop_empty_call_list_chop_pre_GhostSeparation_2 : Valid
[wp] [Qed] Goal typed_push_chop_empty_call_list_chop_pre_GhostSeparation : Valid
[wp] [Qed] Goal typed_push_chop_empty_call_list_chop_pre_Separation : Valid
[wp] 32 goals generated
-------------------------------------------------------------
TEST:  push_remove_empty
[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 user_code_tests/valid.c (with preprocessing)
[kernel] Warning: trying to preprocess annotation with an unknown preprocessor.
[kernel:typing:implicit-function-declaration] user_code_tests/valid.c:32: Warning: 
  Calling undeclared function array_find. Old style K&R code?
[wp] Running WP plugin...
[kernel:annot:missing-spec] user_code_tests/valid.c:468: Warning: 
  Neither code nor specification for function array_find, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 36 goals scheduled
[wp] [Qed] Goal typed_push_remove_empty_assert : Valid
[wp] [Qed] Goal typed_push_remove_empty_assert_2 : Valid
[wp] [Qed] Goal typed_push_remove_empty_call_list_push_pre_ValidArray : Valid
[wp] [Qed] Goal typed_push_remove_empty_call_list_push_pre : Valid
[wp] [Qed] Goal typed_push_remove_empty_call_list_push_pre_EnoughSpace : Valid
[wp] [Qed] Goal typed_push_remove_empty_call_list_push_pre_3 : Valid
[wp] [Qed] Goal typed_push_remove_empty_call_list_push_pre_GhostSeparation_2 : Valid
[wp] [Qed] Goal typed_push_remove_empty_call_list_push_pre_GhostSeparation : Valid
[wp] [Qed] Goal typed_push_remove_empty_call_list_push_pre_Separation : Valid
[wp] [Qed] Goal typed_push_remove_empty_call_list_push_pre_Item_Separation : Valid
[wp] [Qed] Goal typed_push_remove_empty_call_list_push_pre_Unique : Valid
[wp] [Qed] Goal typed_push_remove_empty_call_list_push_pre_Separation_2 : Valid
[wp] [Qed] Goal typed_push_remove_empty_call_list_remove_pre_ValidArray : Valid
[wp] [Qed] Goal typed_push_remove_empty_call_list_remove_pre_GhostSeparation : Valid
[wp] [Qed] Goal typed_push_remove_empty_call_list_remove_pre_2 : Valid
[wp] 36 goals generated
-------------------------------------------------------------
TEST:  add_pop_empty
[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 user_code_tests/valid.c (with preprocessing)
[kernel] Warning: trying to preprocess annotation with an unknown preprocessor.
[kernel:typing:implicit-function-declaration] user_code_tests/valid.c:32: Warning: 
  Calling undeclared function array_find. Old style K&R code?
[wp] Running WP plugin...
[kernel:annot:missing-spec] user_code_tests/valid.c:468: Warning: 
  Neither code nor specification for function array_find, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 33 goals scheduled
[wp] [Qed] Goal typed_add_pop_empty_assert : Valid
[wp] [Qed] Goal typed_add_pop_empty_call_list_add_pre : Valid
[wp] [Qed] Goal typed_add_pop_empty_call_list_add_pre_3 : Valid
[wp] [Qed] Goal typed_add_pop_empty_call_list_add_pre_ValidArray : Valid
[wp] [Qed] Goal typed_add_pop_empty_call_list_add_pre_GhostSeparation : Valid
[wp] [Qed] Goal typed_add_pop_empty_call_list_add_pre_4 : Valid
[wp] [Qed] Goal typed_add_pop_empty_call_list_add_pre_Item_Separation : Valid
[wp] [Qed] Goal typed_add_pop_empty_call_list_add_pre_GhostSeparation_2 : Valid
[wp] [Qed] Goal typed_add_pop_empty_call_list_add_pre_Separation_2 : Valid
[wp] [Qed] Goal typed_add_pop_empty_call_list_add_pre_Separation : Valid
[wp] [Qed] Goal typed_add_pop_empty_call_list_pop_pre_Linked : Valid
[wp] [Qed] Goal typed_add_pop_empty_call_list_pop_pre : Valid
[wp] [Qed] Goal typed_add_pop_empty_call_list_add_pre_Unique : Valid
[wp] [Qed] Goal typed_add_pop_empty_call_list_pop_pre_GhostSeparation : Valid
[wp] [Qed] Goal typed_add_pop_empty_call_list_pop_pre_2 : Valid
[wp] [Qed] Goal typed_add_pop_empty_call_list_pop_pre_ValidArray : Valid
[wp] [Qed] Goal typed_add_pop_empty_call_list_pop_pre_Separation : Valid
[wp] [Qed] Goal typed_add_pop_empty_call_list_pop_pre_4 : Valid
[wp] [Qed] Goal typed_add_pop_empty_call_list_pop_pre_3 : Valid
[wp] 33 goals generated
-------------------------------------------------------------
TEST:  add_chop_empty
[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 user_code_tests/valid.c (with preprocessing)
[kernel] Warning: trying to preprocess annotation with an unknown preprocessor.
[kernel:typing:implicit-function-declaration] user_code_tests/valid.c:32: Warning: 
  Calling undeclared function array_find. Old style K&R code?
[wp] Running WP plugin...
[kernel:annot:missing-spec] user_code_tests/valid.c:468: Warning: 
  Neither code nor specification for function array_find, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 32 goals scheduled
[wp] [Qed] Goal typed_add_chop_empty_assert : Valid
[wp] [Qed] Goal typed_add_chop_empty_post_TEST_3 : Valid
[wp] [Qed] Goal typed_add_chop_empty_call_list_add_pre : Valid
[wp] [Qed] Goal typed_add_chop_empty_call_list_add_pre_3 : Valid
[wp] [Qed] Goal typed_add_chop_empty_call_list_add_pre_ValidArray : Valid
[wp] [Qed] Goal typed_add_chop_empty_call_list_add_pre_GhostSeparation_2 : Valid
[wp] [Qed] Goal typed_add_chop_empty_call_list_add_pre_GhostSeparation : Valid
[wp] [Qed] Goal typed_add_chop_empty_call_list_add_pre_4 : Valid
[wp] [Qed] Goal typed_add_chop_empty_call_list_add_pre_Separation : Valid
[wp] [Qed] Goal typed_add_chop_empty_call_list_add_pre_Item_Separation : Valid
[wp] [Qed] Goal typed_add_chop_empty_call_list_add_pre_Unique : Valid
[wp] [Qed] Goal typed_add_chop_empty_call_list_add_pre_Separation_2 : Valid
[wp] [Qed] Goal typed_add_chop_empty_call_list_chop_pre_3 : Valid
[wp] [Qed] Goal typed_add_chop_empty_call_list_chop_pre_2 : Valid
[wp] [Qed] Goal typed_add_chop_empty_call_list_chop_pre : Valid
[wp] [Qed] Goal typed_add_chop_empty_call_list_chop_pre_GhostSeparation_3 : Valid
[wp] [Qed] Goal typed_add_chop_empty_call_list_chop_pre_GhostSeparation_2 : Valid
[wp] [Qed] Goal typed_add_chop_empty_call_list_chop_pre_GhostSeparation : Valid
[wp] [Qed] Goal typed_add_chop_empty_call_list_chop_pre_Separation : Valid
[wp] 32 goals generated
-------------------------------------------------------------
TEST:  add_remove_empty
[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 user_code_tests/valid.c (with preprocessing)
[kernel] Warning: trying to preprocess annotation with an unknown preprocessor.
[kernel:typing:implicit-function-declaration] user_code_tests/valid.c:32: Warning: 
  Calling undeclared function array_find. Old style K&R code?
[wp] Running WP plugin...
[kernel:annot:missing-spec] user_code_tests/valid.c:468: Warning: 
  Neither code nor specification for function array_find, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 36 goals scheduled
[wp] [Qed] Goal typed_add_remove_empty_assert : Valid
[wp] [Qed] Goal typed_add_remove_empty_assert_2 : Valid
[wp] [Qed] Goal typed_add_remove_empty_call_list_add_pre_ValidArray : Valid
[wp] [Qed] Goal typed_add_remove_empty_call_list_add_pre : Valid
[wp] [Qed] Goal typed_add_remove_empty_call_list_add_pre_4 : Valid
[wp] [Qed] Goal typed_add_remove_empty_call_list_add_pre_3 : Valid
[wp] [Qed] Goal typed_add_remove_empty_call_list_add_pre_GhostSeparation_2 : Valid
[wp] [Qed] Goal typed_add_remove_empty_call_list_add_pre_GhostSeparation : Valid
[wp] [Qed] Goal typed_add_remove_empty_call_list_add_pre_Separation : Valid
[wp] [Qed] Goal typed_add_remove_empty_call_list_add_pre_Item_Separation : Valid
[wp] [Qed] Goal typed_add_remove_empty_call_list_add_pre_Unique : Valid
[wp] [Qed] Goal typed_add_remove_empty_call_list_add_pre_Separation_2 : Valid
[wp] [Qed] Goal typed_add_remove_empty_call_list_remove_pre_ValidArray : Valid
[wp] [Qed] Goal typed_add_remove_empty_call_list_remove_pre_GhostSeparation : Valid
[wp] [Qed] Goal typed_add_remove_empty_call_list_remove_pre_2 : Valid
[wp] 36 goals generated
-------------------------------------------------------------
TEST:  push_push_pop
[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 user_code_tests/valid.c (with preprocessing)
[kernel] Warning: trying to preprocess annotation with an unknown preprocessor.
[kernel:typing:implicit-function-declaration] user_code_tests/valid.c:32: Warning: 
  Calling undeclared function array_find. Old style K&R code?
[wp] Running WP plugin...
[kernel:annot:missing-spec] user_code_tests/valid.c:468: Warning: 
  Neither code nor specification for function array_find, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 49 goals scheduled
[wp] [Qed] Goal typed_push_push_pop_assert : Valid
[wp] [Qed] Goal typed_push_push_pop_assert_2 : Valid
[wp] [Qed] Goal typed_push_push_pop_call_list_push_pre_ValidArray : Valid
[wp] [Qed] Goal typed_push_push_pop_call_list_push_pre_3 : Valid
[wp] [Qed] Goal typed_push_push_pop_call_list_push_pre_GhostSeparation_2 : Valid
[wp] [Qed] Goal typed_push_push_pop_call_list_push_pre_GhostSeparation : Valid
[wp] [Qed] Goal typed_push_push_pop_call_list_push_pre_EnoughSpace : Valid
[wp] [Qed] Goal typed_push_push_pop_call_list_push_pre_Separation : Valid
[wp] [Qed] Goal typed_push_push_pop_call_list_push_pre_Item_Separation : Valid
[wp] [Qed] Goal typed_push_push_pop_call_list_push_pre_4 : Valid
[wp] [Qed] Goal typed_push_push_pop_call_list_push_pre_6 : Valid
[wp] [Qed] Goal typed_push_push_pop_call_list_push_pre_Unique : Valid
[wp] [Qed] Goal typed_push_push_pop_call_list_push_pre_Separation_2 : Valid
[wp] [Qed] Goal typed_push_push_pop_call_list_push_pre_ValidArray_2 : Valid
[wp] [Qed] Goal typed_push_push_pop_call_list_push_pre_EnoughSpace_2 : Valid
[wp] [Qed] Goal typed_push_push_pop_call_list_push_pre_3_2 : Valid
[wp] [Qed] Goal typed_push_push_pop_call_list_push_pre_GhostSeparation_4 : Valid
[wp] [Qed] Goal typed_push_push_pop_call_list_pop_pre_ValidArray : Valid
[wp] [Qed] Goal typed_push_push_pop_call_list_pop_pre : Valid
[wp] [Qed] Goal typed_push_push_pop_call_list_pop_pre_GhostSeparation : Valid
[wp] [Qed] Goal typed_push_push_pop_call_list_pop_pre_2 : Valid
[wp] [Qed] Goal typed_push_push_pop_call_list_pop_pre_4 : Valid
[wp] 49 goals generated
-------------------------------------------------------------
TEST:  push_push_chop
[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 user_code_tests/valid.c (with preprocessing)
[kernel] Warning: trying to preprocess annotation with an unknown preprocessor.
[kernel:typing:implicit-function-declaration] user_code_tests/valid.c:32: Warning: 
  Calling undeclared function array_find. Old style K&R code?
[wp] Running WP plugin...
[kernel:annot:missing-spec] user_code_tests/valid.c:468: Warning: 
  Neither code nor specification for function array_find, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 48 goals scheduled
[wp] [Qed] Goal typed_push_push_chop_assert : Valid
[wp] [Qed] Goal typed_push_push_chop_assert_2 : Valid
[wp] [Qed] Goal typed_push_push_chop_call_list_push_pre_ValidArray : Valid
[wp] [Qed] Goal typed_push_push_chop_call_list_push_pre : Valid
[wp] [Qed] Goal typed_push_push_chop_call_list_push_pre_EnoughSpace : Valid
[wp] [Qed] Goal typed_push_push_chop_call_list_push_pre_3 : Valid
[wp] [Qed] Goal typed_push_push_chop_call_list_push_pre_GhostSeparation_2 : Valid
[wp] [Qed] Goal typed_push_push_chop_call_list_push_pre_GhostSeparation : Valid
[wp] [Qed] Goal typed_push_push_chop_call_list_push_pre_Separation : Valid
[wp] [Qed] Goal typed_push_push_chop_call_list_push_pre_Item_Separation : Valid
[wp] [Qed] Goal typed_push_push_chop_call_list_push_pre_Unique : Valid
[wp] [Qed] Goal typed_push_push_chop_call_list_push_pre_Separation_2 : Valid
[wp] [Qed] Goal typed_push_push_chop_call_list_push_pre_3_2 : Valid
[wp] [Qed] Goal typed_push_push_chop_call_list_push_pre_ValidArray_2 : Valid
[wp] [Qed] Goal typed_push_push_chop_call_list_push_pre_GhostSeparation_4 : Valid
[wp] [Qed] Goal typed_push_push_chop_call_list_push_pre_EnoughSpace_2 : Valid
[wp] [Qed] Goal typed_push_push_chop_call_list_push_pre_4_2 : Valid
[wp] [Qed] Goal typed_push_push_chop_call_list_chop_pre_2 : Valid
[wp] [Qed] Goal typed_push_push_chop_call_list_chop_pre : Valid
[wp] [Qed] Goal typed_push_push_chop_call_list_chop_pre_GhostSeparation_3 : Valid
[wp] [Qed] Goal typed_push_push_chop_call_list_chop_pre_GhostSeparation : Valid
[wp] 48 goals generated
-------------------------------------------------------------
TEST:  push_add_on_single
[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 user_code_tests/valid.c (with preprocessing)
[kernel] Warning: trying to preprocess annotation with an unknown preprocessor.
[kernel:typing:implicit-function-declaration] user_code_tests/valid.c:32: Warning: 
  Calling undeclared function array_find. Old style K&R code?
[wp] Running WP plugin...
[kernel:annot:missing-spec] user_code_tests/valid.c:468: Warning: 
  Neither code nor specification for function array_find, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 38 goals scheduled
[wp] [Qed] Goal typed_push_add_on_single_assert_2 : Valid
[wp] [Qed] Goal typed_push_add_on_single_assert : Valid
[wp] [Qed] Goal typed_push_add_on_single_call_list_push_pre : Valid
[wp] [Qed] Goal typed_push_add_on_single_call_list_push_pre_3 : Valid
[wp] [Qed] Goal typed_push_add_on_single_call_list_push_pre_ValidArray : Valid
[wp] [Qed] Goal typed_push_add_on_single_call_list_push_pre_EnoughSpace : Valid
[wp] [Qed] Goal typed_push_add_on_single_call_list_push_pre_4 : Valid
[wp] [Qed] Goal typed_push_add_on_single_call_list_add_pre : Valid
[wp] [Qed] Goal typed_push_add_on_single_call_list_add_pre_ValidArray : Valid
[wp] [Qed] Goal typed_push_add_on_single_call_list_add_pre_GhostSeparation : Valid
[wp] [Qed] Goal typed_push_add_on_single_call_list_add_pre_4 : Valid
[wp] [Qed] Goal typed_push_add_on_single_call_list_add_pre_3 : Valid
[wp] [Qed] Goal typed_push_add_on_single_call_list_add_pre_5 : Valid
[wp] 38 goals generated
-------------------------------------------------------------
TEST:  add_push_on_single
[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 user_code_tests/valid.c (with preprocessing)
[kernel] Warning: trying to preprocess annotation with an unknown preprocessor.
[kernel:typing:implicit-function-declaration] user_code_tests/valid.c:32: Warning: 
  Calling undeclared function array_find. Old style K&R code?
[wp] Running WP plugin...
[kernel:annot:missing-spec] user_code_tests/valid.c:468: Warning: 
  Neither code nor specification for function array_find, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 40 goals scheduled
[wp] [Qed] Goal typed_add_push_on_single_assert_2 : Valid
[wp] [Qed] Goal typed_add_push_on_single_assert : Valid
[wp] [Qed] Goal typed_add_push_on_single_assert_4 : Valid
[wp] [Qed] Goal typed_add_push_on_single_assert_3 : Valid
[wp] [Qed] Goal typed_add_push_on_single_call_list_add_pre_ValidArray : Valid
[wp] [Qed] Goal typed_add_push_on_single_call_list_add_pre : Valid
[wp] [Qed] Goal typed_add_push_on_single_call_list_add_pre_4 : Valid
[wp] [Qed] Goal typed_add_push_on_single_call_list_add_pre_3 : Valid
[wp] [Qed] Goal typed_add_push_on_single_call_list_add_pre_5 : Valid
[wp] [Qed] Goal typed_add_push_on_single_call_list_push_pre : Valid
[wp] [Qed] Goal typed_add_push_on_single_call_list_push_pre_3 : Valid
[wp] [Qed] Goal typed_add_push_on_single_call_list_push_pre_ValidArray : Valid
[wp] [Qed] Goal typed_add_push_on_single_call_list_push_pre_GhostSeparation : Valid
[wp] [Qed] Goal typed_add_push_on_single_call_list_push_pre_EnoughSpace : Valid
[wp] [Qed] Goal typed_add_push_on_single_call_list_push_pre_4 : Valid
[wp] 40 goals generated
-------------------------------------------------------------
TEST:  push_remove_on_single
[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 user_code_tests/valid.c (with preprocessing)
[kernel] Warning: trying to preprocess annotation with an unknown preprocessor.
[kernel:typing:implicit-function-declaration] user_code_tests/valid.c:32: Warning: 
  Calling undeclared function array_find. Old style K&R code?
[wp] Running WP plugin...
[kernel:annot:missing-spec] user_code_tests/valid.c:468: Warning: 
  Neither code nor specification for function array_find, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 34 goals scheduled
[wp] [Qed] Goal typed_push_remove_on_single_call_list_push_pre : Valid
[wp] [Qed] Goal typed_push_remove_on_single_assert_3 : Valid
[wp] [Qed] Goal typed_push_remove_on_single_assert_2 : Valid
[wp] [Qed] Goal typed_push_remove_on_single_assert : Valid
[wp] [Qed] Goal typed_push_remove_on_single_call_list_push_pre_3 : Valid
[wp] [Qed] Goal typed_push_remove_on_single_call_list_push_pre_ValidArray : Valid
[wp] [Qed] Goal typed_push_remove_on_single_call_list_push_pre_EnoughSpace : Valid
[wp] [Qed] Goal typed_push_remove_on_single_call_list_push_pre_4 : Valid
[wp] [Qed] Goal typed_push_remove_on_single_call_list_remove_pre_ValidArray : Valid
[wp] [Qed] Goal typed_push_remove_on_single_call_list_remove_pre_GhostSeparation : Valid
[wp] [Qed] Goal typed_push_remove_on_single_call_list_remove_pre_2 : Valid
[wp] 34 goals generated
-------------------------------------------------------------
TEST:  push_add_add_remove
[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 user_code_tests/valid.c (with preprocessing)
[kernel] Warning: trying to preprocess annotation with an unknown preprocessor.
[kernel:typing:implicit-function-declaration] user_code_tests/valid.c:32: Warning: 
  Calling undeclared function array_find. Old style K&R code?
[wp] Running WP plugin...
[kernel:annot:missing-spec] user_code_tests/valid.c:468: Warning: 
  Neither code nor specification for function array_find, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 70 goals scheduled
[wp] [Qed] Goal typed_push_add_add_remove_assert_3 : Valid
[wp] [Qed] Goal typed_push_add_add_remove_assert_2 : Valid
[wp] [Qed] Goal typed_push_add_add_remove_assert : Valid
[wp] [Qed] Goal typed_push_add_add_remove_call_list_init_pre_ValidArray : Valid
[wp] [Qed] Goal typed_push_add_add_remove_call_list_init_pre : Valid
[wp] [Qed] Goal typed_push_add_add_remove_assert_4 : Valid
[wp] [Qed] Goal typed_push_add_add_remove_call_list_push_pre : Valid
[wp] [Qed] Goal typed_push_add_add_remove_call_list_push_pre_EnoughSpace : Valid
[wp] [Qed] Goal typed_push_add_add_remove_call_list_push_pre_3 : Valid
[wp] [Qed] Goal typed_push_add_add_remove_call_list_push_pre_ValidArray : Valid
[wp] [Qed] Goal typed_push_add_add_remove_call_list_push_pre_4 : Valid
[wp] [Qed] Goal typed_push_add_add_remove_call_list_push_pre_GhostSeparation_2 : Valid
[wp] [Qed] Goal typed_push_add_add_remove_call_list_push_pre_GhostSeparation : Valid
[wp] [Qed] Goal typed_push_add_add_remove_call_list_push_pre_Separation_2 : Valid
[wp] [Qed] Goal typed_push_add_add_remove_call_list_push_pre_Separation : Valid
[wp] [Qed] Goal typed_push_add_add_remove_call_list_push_pre_Item_Separation : Valid
[wp] [Qed] Goal typed_push_add_add_remove_call_list_add_pre : Valid
[wp] [Qed] Goal typed_push_add_add_remove_call_list_push_pre_Unique : Valid
[wp] [Qed] Goal typed_push_add_add_remove_call_list_add_pre_ValidArray : Valid
[wp] [Qed] Goal typed_push_add_add_remove_call_list_add_pre_GhostSeparation : Valid
[wp] [Qed] Goal typed_push_add_add_remove_call_list_add_pre_4 : Valid
[wp] [Qed] Goal typed_push_add_add_remove_call_list_add_pre_3 : Valid
[wp] [Qed] Goal typed_push_add_add_remove_call_list_add_pre_5 : Valid
[wp] [Qed] Goal typed_push_add_add_remove_call_list_add_pre_7 : Valid
[wp] [Qed] Goal typed_push_add_add_remove_call_list_add_pre_3_2 : Valid
[wp] [Qed] Goal typed_push_add_add_remove_call_list_add_pre_ValidArray_2 : Valid
[wp] [Qed] Goal typed_push_add_add_remove_call_list_add_pre_GhostSeparation_4 : Valid
[wp] [Qed] Goal typed_push_add_add_remove_call_list_add_pre_4_2 : Valid
[wp] [Qed] Goal typed_push_add_add_remove_call_list_add_pre_5_2 : Valid
[wp] [Qed] Goal typed_push_add_add_remove_call_list_remove_pre_2 : Valid
[wp] [Qed] Goal typed_push_add_add_remove_call_list_remove_pre_ValidArray : Valid
[wp] [Qed] Goal typed_push_add_add_remove_call_list_remove_pre_GhostSeparation : Valid
[wp] 70 goals generated
-------------------------------------------------------------
TEST:  push_add_remove_add
[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 user_code_tests/valid.c (with preprocessing)
[kernel] Warning: trying to preprocess annotation with an unknown preprocessor.
[kernel:typing:implicit-function-declaration] user_code_tests/valid.c:32: Warning: 
  Calling undeclared function array_find. Old style K&R code?
[wp] Running WP plugin...
[kernel:annot:missing-spec] user_code_tests/valid.c:468: Warning: 
  Neither code nor specification for function array_find, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 70 goals scheduled
[wp] [Qed] Goal typed_push_add_remove_add_assert_3 : Valid
[wp] [Qed] Goal typed_push_add_remove_add_assert_2 : Valid
[wp] [Qed] Goal typed_push_add_remove_add_assert : Valid
[wp] [Qed] Goal typed_push_add_remove_add_call_list_init_pre_ValidArray : Valid
[wp] [Qed] Goal typed_push_add_remove_add_call_list_init_pre : Valid
[wp] [Qed] Goal typed_push_add_remove_add_assert_4 : Valid
[wp] [Qed] Goal typed_push_add_remove_add_call_list_push_pre : Valid
[wp] [Qed] Goal typed_push_add_remove_add_call_list_push_pre_EnoughSpace : Valid
[wp] [Qed] Goal typed_push_add_remove_add_call_list_push_pre_3 : Valid
[wp] [Qed] Goal typed_push_add_remove_add_call_list_push_pre_ValidArray : Valid
[wp] [Qed] Goal typed_push_add_remove_add_call_list_push_pre_4 : Valid
[wp] [Qed] Goal typed_push_add_remove_add_call_list_push_pre_GhostSeparation_2 : Valid
[wp] [Qed] Goal typed_push_add_remove_add_call_list_push_pre_GhostSeparation : Valid
[wp] [Qed] Goal typed_push_add_remove_add_call_list_push_pre_Separation_2 : Valid
[wp] [Qed] Goal typed_push_add_remove_add_call_list_push_pre_Separation : Valid
[wp] [Qed] Goal typed_push_add_remove_add_call_list_push_pre_Item_Separation : Valid
[wp] [Qed] Goal typed_push_add_remove_add_call_list_add_pre : Valid
[wp] [Qed] Goal typed_push_add_remove_add_call_list_push_pre_Unique : Valid
[wp] [Qed] Goal typed_push_add_remove_add_call_list_add_pre_ValidArray : Valid
[wp] [Qed] Goal typed_push_add_remove_add_call_list_add_pre_GhostSeparation : Valid
[wp] [Qed] Goal typed_push_add_remove_add_call_list_add_pre_4 : Valid
[wp] [Qed] Goal typed_push_add_remove_add_call_list_add_pre_3 : Valid
[wp] [Qed] Goal typed_push_add_remove_add_call_list_add_pre_5 : Valid
[wp] [Qed] Goal typed_push_add_remove_add_call_list_remove_pre_2 : Valid
[wp] [Qed] Goal typed_push_add_remove_add_call_list_remove_pre_ValidArray : Valid
[wp] [Qed] Goal typed_push_add_remove_add_call_list_remove_pre_GhostSeparation : Valid
[wp] [Qed] Goal typed_push_add_remove_add_call_list_add_pre_7 : Valid
[wp] [Qed] Goal typed_push_add_remove_add_call_list_add_pre_ValidArray_2 : Valid
[wp] [Qed] Goal typed_push_add_remove_add_call_list_add_pre_4_2 : Valid
[wp] [Qed] Goal typed_push_add_remove_add_call_list_add_pre_3_2 : Valid
[wp] [Qed] Goal typed_push_add_remove_add_call_list_add_pre_5_2 : Valid
[wp] [Qed] Goal typed_push_add_remove_add_call_list_add_pre_GhostSeparation_4 : Valid
[wp] 70 goals generated
-------------------------------------------------------------
TEST:  push_add_same_single
[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 user_code_tests/valid.c (with preprocessing)
[kernel] Warning: trying to preprocess annotation with an unknown preprocessor.
[kernel:typing:implicit-function-declaration] user_code_tests/valid.c:32: Warning: 
  Calling undeclared function array_find. Old style K&R code?
[wp] Running WP plugin...
[kernel:annot:missing-spec] user_code_tests/valid.c:468: Warning: 
  Neither code nor specification for function array_find, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 37 goals scheduled
[wp] [Qed] Goal typed_push_add_same_single_call_list_push_pre : Valid
[wp] [Qed] Goal typed_push_add_same_single_assert_2 : Valid
[wp] [Qed] Goal typed_push_add_same_single_assert : Valid
[wp] [Qed] Goal typed_push_add_same_single_call_list_push_pre_ValidArray : Valid
[wp] [Qed] Goal typed_push_add_same_single_call_list_push_pre_EnoughSpace : Valid
[wp] [Qed] Goal typed_push_add_same_single_call_list_push_pre_3 : Valid
[wp] [Qed] Goal typed_push_add_same_single_call_list_push_pre_4 : Valid
[wp] [Qed] Goal typed_push_add_same_single_call_list_add_pre_2 : Valid
[wp] [Qed] Goal typed_push_add_same_single_call_list_add_pre : Valid
[wp] [Qed] Goal typed_push_add_same_single_call_list_add_pre_4 : Valid
[wp] [Qed] Goal typed_push_add_same_single_call_list_add_pre_3 : Valid
[wp] [Qed] Goal typed_push_add_same_single_call_list_add_pre_ValidArray : Valid
[wp] [Qed] Goal typed_push_add_same_single_call_list_add_pre_5 : Valid
[wp] [Qed] Goal typed_push_add_same_single_call_list_add_pre_GhostSeparation : Valid
[wp] 37 goals generated
-------------------------------------------------------------
TEST:  add_push_same_single
[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 user_code_tests/valid.c (with preprocessing)
[kernel] Warning: trying to preprocess annotation with an unknown preprocessor.
[kernel:typing:implicit-function-declaration] user_code_tests/valid.c:32: Warning: 
  Calling undeclared function array_find. Old style K&R code?
[wp] Running WP plugin...
[kernel:annot:missing-spec] user_code_tests/valid.c:468: Warning: 
  Neither code nor specification for function array_find, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 37 goals scheduled
[wp] [Qed] Goal typed_add_push_same_single_call_list_add_pre : Valid
[wp] [Qed] Goal typed_add_push_same_single_assert_2 : Valid
[wp] [Qed] Goal typed_add_push_same_single_assert : Valid
[wp] [Qed] Goal typed_add_push_same_single_call_list_add_pre_ValidArray : Valid
[wp] [Qed] Goal typed_add_push_same_single_call_list_add_pre_4 : Valid
[wp] [Qed] Goal typed_add_push_same_single_call_list_add_pre_3 : Valid
[wp] [Qed] Goal typed_add_push_same_single_call_list_add_pre_5 : Valid
[wp] [Qed] Goal typed_add_push_same_single_call_list_push_pre_2 : Valid
[wp] [Qed] Goal typed_add_push_same_single_call_list_push_pre : Valid
[wp] [Qed] Goal typed_add_push_same_single_call_list_push_pre_EnoughSpace : Valid
[wp] [Qed] Goal typed_add_push_same_single_call_list_push_pre_3 : Valid
[wp] [Qed] Goal typed_add_push_same_single_call_list_push_pre_ValidArray : Valid
[wp] [Qed] Goal typed_add_push_same_single_call_list_push_pre_4 : Valid
[wp] [Qed] Goal typed_add_push_same_single_call_list_push_pre_GhostSeparation : Valid
[wp] 37 goals generated
