Check counterexamples classification benchmark
This is the list of example files for the classification of counterexamples using the giant-step approach, located in the folder bench/check-ce
and listed in alphabetical order. For each file, we need to check that the counterexamples returned by the provers and their classification are correct.
See also ce-stats.py to compute statistics about the bench for checking CE.
test | CE classification | related issues |
---|---|---|
614.mlw | ||
615.mlw | ||
640_no_loc_failure.mlw | ||
657.mlw | #657 (closed) | |
668_projection.mlw | ||
703_reduce_term.mlw | INCOMPLETE cannot decide | |
algebraic_types_mono.mlw | #640 (closed) | |
algebraic_types_poly.mlw | ||
anonymous1.mlw | ||
anonymous2.mlw | ||
anonymous3.mlw | ||
anonymous4.mlw | ||
anonymous5.mlw | INCOMPLETE many args for exec + cannot decide | |
anonymous6.mlw | ||
anonymous6_mono.mlw | ||
array_mono.mlw | INCOMPLETE cannot decide | |
array_poly.mlw | INCOMPLETE uncaught exception (Cannot instantiate a defined symbol sorted_sub) | |
array_records_mono.mlw | INCOMPLETE cannot decide (only z3 prover) | |
array_records_poly.mlw | INCOMPLETE cannot decide | polymorphism |
attributes.mlw | ||
attributes_mono.mlw | ||
blackbox.mlw | ||
bv32.mlw | INCOMPLETE cannot decide (only z3 prover) | #352 (closed) |
bv32_mono.mlw | ||
bv32_toBig.mlw | #657 (closed) | |
call-val-function.mlw | #734 | |
double_projection.mlw | ||
falseCE.mlw | ||
fide21.mlw | ||
floats.mlw | INCOMPLETE cannot decide | !311 (closed) #640 (closed) |
for.mlw | ||
for_mono.mlw | ||
for1.mlw | ||
for1_mono.mlw | ||
func_call1.mlw | ||
func_call1_mono.mlw | ||
func_call2.mlw | ||
func_call3.mlw | ||
func_call4.mlw | ||
func_call4_mono.mlw | ||
func_call5.mlw | INCOMPLETE missing return value | |
func_call6.mlw | ||
func_call6_mono.mlw | ||
func_call.mlw | ||
func_call_mono.mlw | ||
global_logic_constant.mlw | ||
if_assign.mlw | #353 (closed) | |
if_decision_branch.mlw | ||
int32.mlw | ||
int32_mono.mlw | ||
integers.mlw | #640 (closed) #705 (closed) | |
int_overflow.mlw | INCOMPLETE cannot decide | special case with div by 0 |
jlamp_array_mono.mlw | INCOMPLETE cannot decide | |
jlamp_array_poly.mlw | INCOMPLETE cannot decide | polymorphism |
jlamp_projections.mlw | #351 (closed) | |
jlamp0_mono.mlw | ||
jlamp0_poly.mlw | #348 (closed) | |
let_constant.mlw | ||
let_function_logic.mlw | #734 | |
let_function.mlw | ||
lists.mlw | ||
logic_constant.mlw | ||
logic_function.mlw | ||
loop_ce.mlw | ||
loop_ce_mono.mlw | ||
loop_inv_int.mlw | ||
loop_inv_int_mono.mlw | ||
loop_inv_real.mlw | INCOMPLETE cannot decide | polymorphism |
loop_inv_real_mono.mlw | INCOMPLETE cannot decide | |
manual_map.mlw | ||
maps_mono.mlw | ||
maps_poly.mlw | INCOMPLETE cannot import | #354 (closed) #640 (closed) polymorphism |
multifile1.mlw | ||
multifile2.mlw | ||
polymorphism.mlw | ||
range_type_float.mlw | ||
range_type_int.mlw | ||
real_values.mlw | INCOMPLETE cannot decide | |
record_map.mlw | INCOMPLETE undefined argument + cannot decide | #359 (closed) |
record_nested_one_field.mlw | ||
records_inv.mlw | ||
records_label.mlw | TO DISCUSS (#355?) | |
recursive_model.mlw | #640 (closed) | |
ref1.mlw | ||
ref1_mono.mlw | ||
ref2.mlw | ||
ref2_mono.mlw | ||
ref_ex.mlw | TO DISCUSS (in postcondition of incr , !y is interpreted as old y ?) + see #355
|
|
ref_ex_mono.mlw | ||
ref_mono.mlw | TO DISCUSS (in postcondition of incr , !y is interpreted as old y ) + see #355
|
|
result.mlw | #353 (closed) | |
return_value_below_if_when_vc_sp.mlw | ||
simple_array.mlw | INCOMPLETE cannot decide (only z3 prover) | #640 (closed) |
strings.mlw | INCOMPLETE cannot decide | #640 (closed) + TO DISCUSS (values of strings seem strange?) |
test_result_ce_value0.mlw | ||
test_result_ce_value1.mlw | ||
test_result_ce_value2.mlw | ||
threshold.mlw | ||
tuple1.mlw | INCOMPLETE missing return value (only z3 prover) | |
tuple.mlw | ||
underspec.mlw | ||
val_function.mlw | INCOMPLETE cannot decide | #734 |
var_clones.mlw | ||
while1.mlw | ||
while1_mono.mlw | ||
while.mlw | ||
while_mono.mlw |
Additional files in bench/check-ce/petiot2018
.
test | CE classification | related issues |
---|---|---|
binary_search.mlw | ||
isqrt.mlw | ||
rgf.mlw |