bench/encoding/template_rc

   1 [tools @BENCH_NAME@]
   2 prover = "@PROVER@"
   3 loadpath = "."
   4 use = "meta.@SELECT_INST@"
   5 use = "meta.@SELECT_LSKEPT@"
   6 use = "meta.@SELECT_LSINST@"
   7 use = "meta.@SELECT_KEPT@"
   8 use = "meta.@ENCO_KEPT@"
   9 use = "meta.@ENCO_POLY@"
  10
  11 [probs caduceus]
  12 file = "why3/caduceus/abs_why.why"
  13 file = "why3/caduceus/alloca_why.why"
  14 file = "why3/caduceus/alloc_why.why"
  15 file = "why3/caduceus/all_why.why"
  16 file = "why3/caduceus/all_zeros_why.why"
  17 file = "why3/caduceus/arith_why.why"
  18 file = "why3/caduceus/array_why.why"
  19 file = "why3/caduceus/assigns2_why.why"
  20 file = "why3/caduceus/assigns_range_right_why.why"
  21 file = "why3/caduceus/assigns_why.why"
  22 file = "why3/caduceus/band_why.why"
  23 file = "why3/caduceus/binary_search_overflows_why.why"
  24 file = "why3/caduceus/binary_search_safety_why.why"
  25 file = "why3/caduceus/binary_search_why.why"
  26 file = "why3/caduceus/blit_why.why"
  27 file = "why3/caduceus/break_why.why"
  28 file = "why3/caduceus/bresenham_why.why"
  29 file = "why3/caduceus/bug_why.why"
  30 file = "why3/caduceus/calloc_why.why"
  31 file = "why3/caduceus/call_why.why"
  32 file = "why3/caduceus/clash_why.why"
  33 file = "why3/caduceus/consts_why.why"
  34 file = "why3/caduceus/const_why.why"
  35 file = "why3/caduceus/continue_why.why"
  36 file = "why3/caduceus/coord_why.why"
  37 file = "why3/caduceus/copy_why.why"
  38 file = "why3/caduceus/count_bits_2_why.why"
  39 file = "why3/caduceus/count_bits_why.why"
  40 file = "why3/caduceus/dassault_1_why.why"
  41 file = "why3/caduceus/Dillon_why.why"
  42 file = "why3/caduceus/division_why.why"
  43 file = "why3/caduceus/dowhile_why.why"
  44 file = "why3/caduceus/enum_why.why"
  45 file = "why3/caduceus/e_why.why"
  46 file = "why3/caduceus/extern_why.why"
  47 file = "why3/caduceus/fact_why.why"
  48 file = "why3/caduceus/false2_why.why"
  49 file = "why3/caduceus/false_why.why"
  50 file = "why3/caduceus/fib_why.why"
  51 file = "why3/caduceus/flag_checkenum_why.why"
  52 file = "why3/caduceus/flag_why.why"
  53 file = "why3/caduceus/float_why.why"
  54 file = "why3/caduceus/gappa_why.why"
  55 file = "why3/caduceus/ghost2_why.why"
  56 file = "why3/caduceus/ghost_why.why"
  57 file = "why3/caduceus/goto_why.why"
  58 file = "why3/caduceus/heapsort_swap_safety_why.why"
  59 file = "why3/caduceus/heapsort_swap_why.why"
  60 file = "why3/caduceus/heapsort_why.why"
  61 file = "why3/caduceus/heap_why.why"
  62 file = "why3/caduceus/ifs_why.why"
  63 file = "why3/caduceus/incr_why.why"
  64 file = "why3/caduceus/init2_why.why"
  65 file = "why3/caduceus/init_why.why"
  66 file = "why3/caduceus/insertion_safety_why.why"
  67 file = "why3/caduceus/insertion_why.why"
  68 file = "why3/caduceus/invariants_why.why"
  69 file = "why3/caduceus/keiko1_why.why"
  70 file = "why3/caduceus/labels_why.why"
  71 file = "why3/caduceus/latespec_why.why"
  72 file = "why3/caduceus/lexico_why.why"
  73 file = "why3/caduceus/linked-list_why.why"
  74 file = "why3/caduceus/logic_cast_why.why"
  75 file = "why3/caduceus/logic_why.why"
  76 file = "why3/caduceus/loop_assigns_why.why"
  77 file = "why3/caduceus/loop_inv_why.why"
  78 file = "why3/caduceus/loops_why.why"
  79 file = "why3/caduceus/malloc_why.why"
  80 file = "why3/caduceus/math_mod_why.why"
  81 file = "why3/caduceus/matrix_why.why"
  82 file = "why3/caduceus/mean_why.why"
  83 file = "why3/caduceus/muller_why.why"
  84 file = "why3/caduceus/negate_why.why"
  85 file = "why3/caduceus/not_assigns_why.why"
  86 file = "why3/caduceus/null_why.why"
  87 file = "why3/caduceus/overflows_why.why"
  88 file = "why3/caduceus/param_why.why"
  89 file = "why3/caduceus/passing_why.why"
  90 file = "why3/caduceus/pi_again_why.why"
  91 file = "why3/caduceus/pi_why.why"
  92 file = "why3/caduceus/pointer_why.why"
  93 file = "why3/caduceus/purse_why.why"
  94 file = "why3/caduceus/queue_jr_why.why"
  95 file = "why3/caduceus/queue_why.why"
  96 file = "why3/caduceus/rc4_why.why"
  97 file = "why3/caduceus/rec2_why.why"
  98 file = "why3/caduceus/rec_why.why"
  99 file = "why3/caduceus/ref_glob_why.why"
 100 file = "why3/caduceus/ref_why.why"
 101 file = "why3/caduceus/russian_why.why"
 102 file = "why3/caduceus/search_why.why"
 103 file = "why3/caduceus/see_why.why"
 104 file = "why3/caduceus/selection_safety_why.why"
 105 file = "why3/caduceus/selection_why.why"
 106 file = "why3/caduceus/separation1_why.why"
 107 file = "why3/caduceus/separation2_why.why"
 108 file = "why3/caduceus/separation3_why.why"
 109 file = "why3/caduceus/separation4_why.why"
 110 file = "why3/caduceus/separation_why.why"
 111 file = "why3/caduceus/shift_why.why"
 112 file = "why3/caduceus/sort_why.why"
 113 file = "why3/caduceus/sqrt_why.why"
 114 file = "why3/caduceus/strcpy_why.why"
 115 file = "why3/caduceus/string_why.why"
 116 file = "why3/caduceus/struct2_why.why"
 117 file = "why3/caduceus/struct3_why.why"
 118 file = "why3/caduceus/struct4_why.why"
 119 file = "why3/caduceus/struct_why.why"
 120 file = "why3/caduceus/sum1_why.why"
 121 file = "why3/caduceus/sum2_why.why"
 122 file = "why3/caduceus/switch_why.why"
 123 file = "why3/caduceus/tracability_why.why"
 124 file = "why3/caduceus/trop_why.why"
 125 file = "why3/caduceus/unsafe_why.why"
 126 file = "why3/caduceus/zones2_why.why"
 127 file = "why3/caduceus/zones_why.why"
 128
 129 [probs caduceus_why]
 130 file = "why3/caduceus_why/algo64_why.why"
 131 file = "why3/caduceus_why/algo65_why.why"
 132 file = "why3/caduceus_why/all_why.why"
 133 file = "why3/caduceus_why/arith_why.why"
 134 file = "why3/caduceus_why/bresenham_why.why"
 135 file = "why3/caduceus_why/bsearch_why.why"
 136 file = "why3/caduceus_why/dijkstra_why.why"
 137 file = "why3/caduceus_why/exns_why.why"
 138 file = "why3/caduceus_why/fib_why.why"
 139 file = "why3/caduceus_why/find_why.why"
 140 file = "why3/caduceus_why/gcd_why.why"
 141 file = "why3/caduceus_why/heapsort_why.why"
 142 file = "why3/caduceus_why/inductive_why.why"
 143 file = "why3/caduceus_why/loop0_why.why"
 144 file = "why3/caduceus_why/loops_why.why"
 145 file = "why3/caduceus_why/mac_carthy_why.why"
 146 file = "why3/caduceus_why/maximumsort_why.why"
 147 file = "why3/caduceus_why/max_why.why"
 148 file = "why3/caduceus_why/mergesort_why.why"
 149 file = "why3/caduceus_why/oldify_why.why"
 150 file = "why3/caduceus_why/opaque_why.why"
 151 file = "why3/caduceus_why/peano_why.why"
 152 file = "why3/caduceus_why/poly_why.why"
 153 file = "why3/caduceus_why/power_why.why"
 154 file = "why3/caduceus_why/po_why.why"
 155 file = "why3/caduceus_why/queens_why.why"
 156 file = "why3/caduceus_why/quicksort2_why.why"
 157 file = "why3/caduceus_why/quicksort_why.why"
 158 file = "why3/caduceus_why/recfun_why.why"
 159 file = "why3/caduceus_why/return_why.why"
 160 file = "why3/caduceus_why/search_why.why"
 161 file = "why3/caduceus_why/see_why.why"
 162 file = "why3/caduceus_why/selection_why.why"
 163 file = "why3/caduceus_why/set_why.why"
 164 file = "why3/caduceus_why/sqrt_dicho_why.why"
 165 file = "why3/caduceus_why/sqrt_why.why"
 166 file = "why3/caduceus_why/swap0_why.why"
 167 file = "why3/caduceus_why/wpcalls_why.why"
 168
 169 [probs dancing_rev]
 170 file = "why3/dancing/bug2_why.why"
 171 file = "why3/dancing/i_behavior.myset_why.why"
 172 file = "why3/dancing/i_behavior_oracle.myset_why.why"
 173 file = "why3/dancing/i_dancing.myset_why.why"
 174 file = "why3/dancing/i_safety_frame_jessie_why.why"
 175 file = "why3/dancing/i_safety.myset_why.why"
 176 file = "why3/dancing/i_safety.notinft2_why.why"
 177 file = "why3/dancing/i_safety.notinft_why.why"
 178 file = "why3/rev/notinc_disj_FT.ft_is_a_pred_why.why"
 179 file = "why3/rev/notinc_disj_FT.with_notin___why.why"
 180 file = "why3/rev/notinc_disj_FT.without_inductive_FT_why.why"
 181 file = "why3/rev/notin.jessie_frame_why.why"
 182
 183 [bench @BENCH_NAME@]
 184 tools = @BENCH_NAME@
 185 probs = caduceus
 186 probs = caduceus_why
 187 probs = dancing_rev
 188 timeline = "@BENCH_NAME@.time"
 189 average = "@BENCH_NAME@.avg"
 190 csv = "@BENCH_NAME@.csv"