Skip to content
Snippets Groups Projects
Commit 7963a687 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] Update tests oracle wrt RTE warning

parent 896cbe58
No related branches found
No related tags found
No related merge requests found
Showing
with 32 additions and 32 deletions
# frama-c -wp -wp-model 'Hoare' [...]
[kernel] Parsing wp_strategy.c (with preprocessing)
[rte] annotating function bts0513
[rte] annotating function bts0513_bis
[rte:annot] annotating function bts0513
[rte:annot] annotating function bts0513_bis
[wp] Running WP plugin...
[wp] 4 goals scheduled
[wp] [Alt-Ergo] Goal hoare_bts0513_ensures_qed_ko_ko1 : Unsuccess
......
# frama-c -wp -wp-rte [...]
[kernel] Parsing chunk_typing.i (no preprocessing)
[wp] Running WP plugin...
[rte] annotating function function
[rte:annot] annotating function function
[wp] 39 goals scheduled
[wp] [Alt-Ergo] Goal typed_function_ensures : Valid
[wp] [Alt-Ergo] Goal typed_function_loop_invariant_preserved : Valid
......
# frama-c -wp -wp-rte [...]
[kernel] Parsing chunk_typing_usable.i (no preprocessing)
[wp] Running WP plugin...
[rte] annotating function usable_axiom
[rte] annotating function usable_lemma
[rte:annot] annotating function usable_axiom
[rte:annot] annotating function usable_lemma
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 3 goals scheduled
[wp] [Coq] Goal typed_lemma_provable_lemma : Saved script
......
# frama-c -wp [...]
[kernel] Parsing gnu_zero_array.i (no preprocessing)
[rte] annotating function main
[rte:annot] annotating function main
[wp] Running WP plugin...
[wp] gnu_zero_array.i:14: Warning:
Cast with incompatible pointers types (source: sint8*) (target: S*)
......
# frama-c -wp -wp-rte [...]
[kernel] Parsing opaque_struct.i (no preprocessing)
[wp] Running WP plugin...
[rte] annotating function assigned_via_pointer
[rte] annotating function assigns
[rte] annotating function assigns_effect
[rte] annotating function chunk_typing
[rte] annotating function initialized_assigns
[rte] annotating function uninitialized_assigns
[rte:annot] annotating function assigned_via_pointer
[rte:annot] annotating function assigns
[rte:annot] annotating function assigns_effect
[rte:annot] annotating function chunk_typing
[rte:annot] annotating function initialized_assigns
[rte:annot] annotating function uninitialized_assigns
[kernel:annot:missing-spec] opaque_struct.i:79: Warning:
Neither code nor specification for function use, generating default assigns from the prototype
[wp] 15 goals scheduled
......
# frama-c -wp -wp-rte [...]
[kernel] Parsing bts779.i (no preprocessing)
[wp] Running WP plugin...
[rte] annotating function f
[rte:annot] annotating function f
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_f_assert : Valid
[wp] [Alt-Ergo] Goal typed_f_assert_rte_mem_access : Unsuccess
......
# frama-c -wp -wp-rte [...]
[kernel] Parsing bts_1360.i (no preprocessing)
[wp] Running WP plugin...
[rte] annotating function foo_correct
[rte] annotating function foo_wrong
[rte:annot] annotating function foo_correct
[rte:annot] annotating function foo_wrong
[wp] 10 goals scheduled
[wp] [Qed] Goal typed_foo_wrong_ensures : Valid
[wp] [Qed] Goal typed_foo_wrong_assert_rte_mem_access : Valid
......
# frama-c -wp -wp-rte -wp-timeout 20 -warn-unsigned-overflow [...]
[kernel] Parsing binary-multiplication-without-overflow.c (with preprocessing)
[wp] Running WP plugin...
[rte] annotating function BinaryMultiplication
[rte:annot] annotating function BinaryMultiplication
[wp] 16 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_half : Valid
[wp] [Qed] Goal typed_lemma_size : Valid
......
# frama-c -wp -wp-rte [...]
[kernel] Parsing binary-multiplication.c (with preprocessing)
[wp] Running WP plugin...
[rte] annotating function BinaryMultiplication
[rte:annot] annotating function BinaryMultiplication
[wp] 17 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_ax4_ok : Valid
[wp] [Alt-Ergo] Goal typed_lemma_ax5_ok : Valid
......
# frama-c -wp -wp-rte [...]
[kernel] Parsing bsearch.c (with preprocessing)
[wp] Running WP plugin...
[rte] annotating function binary_search
[rte:annot] annotating function binary_search
[wp] 28 goals scheduled
[wp] [Passed] Smoke-test typed_binary_search_wp_smoke_default_requires
[wp] [Passed] Smoke-test typed_binary_search_wp_smoke_dead_loop_s3
......
# frama-c -wp -wp-rte [...]
[kernel] Parsing euclid.c (with preprocessing)
[wp] Running WP plugin...
[rte] annotating function euclid_gcd
[rte:annot] annotating function euclid_gcd
[wp] 16 goals scheduled
[wp] [Passed] Smoke-test typed_euclid_euclid_gcd_wp_smoke_default_requires
[wp] [Passed] Smoke-test typed_euclid_euclid_gcd_wp_smoke_dead_loop_s1
......
......@@ -54,9 +54,9 @@
iter_ptr 2 6 8 100%
------------------------------------------------------------
[wp] Running WP plugin...
[rte] annotating function find
[rte] annotating function find_ptr
[rte] annotating function iter_ptr
[rte:annot] annotating function find
[rte:annot] annotating function find_ptr
[rte:annot] annotating function iter_ptr
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_find_assert_rte_mem_access : Valid
[wp] [Alt-Ergo] Goal typed_find_assert_rte_signed_overflow : Valid
......
......@@ -21,7 +21,7 @@
exo1 6 4 10 100%
------------------------------------------------------------
[wp] Running WP plugin...
[rte] annotating function exo1
[rte:annot] annotating function exo1
[wp] 5 goals scheduled
[wp] [Alt-Ergo] Goal typed_exo1_assert_rte_signed_overflow : Valid
[wp] [Alt-Ergo] Goal typed_exo1_assert_rte_mem_access : Valid
......
......@@ -33,7 +33,7 @@
max_subarray 12 10 22 100%
------------------------------------------------------------
[wp] Running WP plugin...
[rte] annotating function max_subarray
[rte:annot] annotating function max_subarray
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_max_subarray_assert_rte_mem_access : Valid
[wp] Proved goals: 1 / 1
......
......@@ -54,7 +54,7 @@
*/
void equal_elements(int *a, int *v1, int *v2);
[wp] Running WP plugin...
[rte] annotating function equal_elements
[rte:annot] annotating function equal_elements
[wp] 16 goals scheduled
[wp] [Qed] Goal typed_ref_equal_elements_assert_rte_mem_access : Valid
[wp] [Qed] Goal typed_ref_equal_elements_assert_rte_mem_access_2 : Valid
......
......@@ -55,7 +55,7 @@
*/
void equal_elements(int *a, int *v1, int *v2);
[wp] Running WP plugin...
[rte] annotating function equal_elements
[rte:annot] annotating function equal_elements
[wp] 16 goals scheduled
[wp] [Qed] Goal typed_ref_equal_elements_assert_rte_mem_access : Valid
[wp] [Qed] Goal typed_ref_equal_elements_assert_rte_mem_access_2 : Valid
......
......@@ -37,7 +37,7 @@
pair 16 10 26 100%
------------------------------------------------------------
[wp] Running WP plugin...
[rte] annotating function pair
[rte:annot] annotating function pair
[wp] 9 goals scheduled
[wp] [Qed] Goal typed_pair_assert_rte_index_bound : Valid
[wp] [Qed] Goal typed_pair_assert_rte_index_bound_2 : Valid
......
......@@ -67,9 +67,9 @@
main 5 2 7 100%
------------------------------------------------------------
[wp] Running WP plugin...
[rte] annotating function main
[rte] annotating function stringCompare
[rte] annotating function stringLength
[rte:annot] annotating function main
[rte:annot] annotating function stringCompare
[rte:annot] annotating function stringLength
[wp] 8 goals scheduled
[wp] [Alt-Ergo] Goal typed_stringCompare_assert_rte_mem_access : Valid
[wp] [Alt-Ergo] Goal typed_stringCompare_assert_rte_mem_access_2 : Valid
......
......@@ -3,7 +3,7 @@
[kernel] Parsing working_dir/swap.c (with preprocessing)
[kernel] Parsing working_dir/swap2.h (with preprocessing)
[wp] Running WP plugin...
[rte] annotating function swap
[rte:annot] annotating function swap
[wp] 8 goals scheduled
[wp] [Alt-Ergo] Goal typed_swap_ensures_A : Valid
[wp] [Qed] Goal typed_swap_ensures_B : Valid
......
# frama-c -wp -wp-rte [...]
[rte] annotating function swap
[rte:annot] annotating function swap
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
swap 5 3 8 100%
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment