Created
December 17, 2018 00:17
-
-
Save hyarion/dc456b8c4d90b8332827fd6fc3b082a5 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # this is the current state of running the test suite from "ACSL by Example" | |
| # a few goals fails here and there.. I need to figure out how to check exactly | |
| # which one it is | |
| # bumped the env waay up to make sure those wheren't the cause | |
| $ echo $WP_TIMEOUT $WP_COQ_TIMEOUT $WP_ALT_ERGO_STEPS | |
| 80 80 20000 | |
| $ why3 --version | |
| Why3 platform, version 1.1.0 | |
| $ frama-c -wp-detect | |
| [wp] Prover Known provers [Known:provers] | |
| [wp] Prover Alt-Ergo 2.2.0 [Alt-Ergo:2.2.0] | |
| [wp] Prover CVC3 2.4.1 [CVC3:2.4.1] | |
| [wp] Prover CVC4 1.6 [CVC4:1.6] | |
| [wp] Prover Coq 8.7.2 [Coq:8.7.2] | |
| [wp] Prover Eprover 2.2 [Eprover:2.2] | |
| [wp] Prover Gappa 1.3.2 [Gappa:1.3.2] | |
| [wp] Prover Z3 4.8.3 [Z3:4.8.3] | |
| $ make report | |
| report nonmutating | |
| find [19 19 ( 10 9 0 0 0 0 0)] 100% | |
| find2 [19 19 ( 10 9 0 0 0 0 0)] 100% | |
| find_first_of [25 25 ( 16 9 0 0 0 0 0)] 100% | |
| adjacent_find [22 22 ( 10 12 0 0 0 0 0)] 100% | |
| mismatch [20 20 ( 10 10 0 0 0 0 0)] 100% | |
| equal [7 7 ( 6 1 0 0 0 0 0)] 100% | |
| search [30 30 ( 18 12 0 0 0 0 0)] 100% | |
| search_n [29 29 ( 11 18 0 0 0 0 0)] 100% | |
| find_end [28 28 ( 15 13 0 0 0 0 0)] 100% | |
| count [19 19 ( 7 12 0 0 0 0 0)] 100% | |
| report maxmin | |
| operators [6 6 ( 4 2 0 0 0 0 0)] 100% | |
| max_element [24 24 ( 13 11 0 0 0 0 0)] 100% | |
| max_element2 [24 24 ( 12 12 0 0 0 0 0)] 100% | |
| max_seq [8 8 ( 5 3 0 0 0 0 0)] 100% | |
| min_element [24 24 ( 12 12 0 0 0 0 0)] 100% | |
| report binarysearch | |
| lower_bound [19 19 ( 5 14 0 0 0 0 0)] 100% | |
| upper_bound [19 19 ( 7 12 0 0 0 0 0)] 100% | |
| equal_range [20 20 ( 17 3 0 0 0 0 0)] 100% | |
| equal_range2 [64 64 ( 24 35 1 0 0 0 4)] 100% | |
| binary_search [10 10 ( 8 2 0 0 0 0 0)] 100% | |
| binary_search2 [10 10 ( 8 2 0 0 0 0 0)] 100% | |
| report mutating | |
| fill [12 12 ( 4 8 0 0 0 0 0)] 100% | |
| swap [7 7 ( 7 0 0 0 0 0 0)] 100% | |
| swap_ranges [22 22 ( 5 17 0 0 0 0 0)] 100% | |
| copy [15 15 ( 4 11 0 0 0 0 0)] 100% | |
| copy_backward [17 17 ( 7 9 1 0 0 0 0)] 100% | |
| reverse_copy [17 17 ( 4 13 0 0 0 0 0)] 100% | |
| reverse [24 24 ( 5 18 1 0 0 0 0)] 100% | |
| rotate_copy [17 17 ( 5 12 0 0 0 0 0)] 100% | |
| rotate [24 24 ( 10 14 0 0 0 0 0)] 100% | |
| replace_copy [20 20 ( 7 13 0 0 0 0 0)] 100% | |
| replace [15 15 ( 4 11 0 0 0 0 0)] 100% | |
| remove_copy [34 34 ( 10 20 4 0 0 0 0)] 100% | |
| unique_copy [26 26 ( 8 18 0 0 0 0 0)] 100% | |
| unique_copy2 [54 53 ( 9 32 6 0 2 1 3)] 98% | |
| random_shuffle [49 48 ( 22 24 0 0 1 0 1)] 97% | |
| report numeric | |
| iota [16 16 ( 7 9 0 0 0 0 0)] 100% | |
| accumulate [14 14 ( 6 8 0 0 0 0 0)] 100% | |
| inner_product [19 19 ( 6 13 0 0 0 0 0)] 100% | |
| partial_sum [38 38 ( 9 25 4 0 0 0 0)] 100% | |
| adjacent_difference [32 32 ( 11 16 5 0 0 0 0)] 100% | |
| partial_sum_inv [18 18 ( 8 9 1 0 0 0 0)] 100% | |
| adjacent_difference_inv [26 26 ( 7 16 2 0 0 1 0)] 100% | |
| report heap | |
| is_heap [24 24 ( 6 18 0 0 0 0 0)] 100% | |
| push_heap [96 95 ( 33 49 9 0 3 0 1)] 98% | |
| pop_heap [93 92 ( 49 39 3 0 0 0 1)] 98% | |
| make_heap [34 34 ( 15 19 0 0 0 0 0)] 100% | |
| sort_heap [50 50 ( 16 31 2 0 0 0 1)] 100% | |
| report sorting | |
| is_sorted [15 15 ( 7 7 0 0 0 0 1)] 100% | |
| partial_sort [114 114 ( 40 59 3 0 1 0 11)] 100% | |
| report classic-sorting | |
| selection_sort [54 54 ( 17 29 2 0 1 0 5)] 100% | |
| insertion_sort [63 63 ( 18 37 2 0 2 0 4)] 100% | |
| heap_sort [19 19 ( 8 11 0 0 0 0 0)] 100% | |
| report stack | |
| stack_init [14 14 ( 4 10 0 0 0 0 0)] 100% | |
| stack_equal [18 18 ( 7 11 0 0 0 0 0)] 100% | |
| stack_size [6 6 ( 1 5 0 0 0 0 0)] 100% | |
| stack_empty [10 10 ( 5 5 0 0 0 0 0)] 100% | |
| stack_full [11 11 ( 5 6 0 0 0 0 0)] 100% | |
| stack_top [16 16 ( 6 10 0 0 0 0 0)] 100% | |
| stack_push [43 43 ( 28 15 0 0 0 0 0)] 100% | |
| stack_pop [32 32 ( 20 12 0 0 0 0 0)] 100% | |
| report stack_wd | |
| stack_size_wd [12 12 ( 8 4 0 0 0 0 0)] 100% | |
| stack_empty_wd [12 12 ( 8 4 0 0 0 0 0)] 100% | |
| stack_top_wd [12 12 ( 8 4 0 0 0 0 0)] 100% | |
| stack_push_wd [15 15 ( 3 9 3 0 0 0 0)] 100% | |
| stack_pop_wd [12 12 ( 6 5 1 0 0 0 0)] 100% | |
| report stack_axiom | |
| axiom_size_of_init [15 15 ( 11 4 0 0 0 0 0)] 100% | |
| axiom_size_of_push [12 12 ( 9 3 0 0 0 0 0)] 100% | |
| axiom_top_of_push [11 11 ( 8 3 0 0 0 0 0)] 100% | |
| axiom_size_of_pop [11 11 ( 8 3 0 0 0 0 0)] 100% | |
| axiom_pop_of_push [10 10 ( 6 4 0 0 0 0 0)] 100% | |
| axiom_push_of_pop_top [15 15 ( 9 6 0 0 0 0 0)] 100% | |
| # seems like cvc3 doesn't solve anything but disabling all the other provers shows that it _does_ work: | |
| # (with all but cvc3 disabled) | |
| $ make report | |
| report nonmutating | |
| find [19 19 ( 10 0 0 9 0 0 0)] 100% | |
| find2 [19 19 ( 10 0 0 9 0 0 0)] 100% | |
| find_first_of [25 25 ( 16 0 0 9 0 0 0)] 100% | |
| adjacent_find [22 22 ( 10 0 0 12 0 0 0)] 100% | |
| mismatch [20 20 ( 10 0 0 10 0 0 0)] 100% | |
| equal [7 7 ( 6 0 0 1 0 0 0)] 100% | |
| search [30 30 ( 18 0 0 12 0 0 0)] 100% | |
| ^C |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment