Check counterexamples benchmark
This is the list of example files for counterexamples, located in the folder bench/ce
and listed in alphabetical order.
For each file, we need to check that provers give counterexamples.
When possible, we would like to migrate those files to bench/check-ce
.
(See #623 for files in bench/check-ce
.)
test | CE generation OK ? | CE classification ? |
---|---|---|
algebraic_types_poly.mlw | TO DISCUSS (file located in bench/ce_xfail ) |
|
array_mono.mlw | OK | both RAC terminated because cannot import value from model: type with not exactly one constructors array/0 |
array_records.mlw | OK | cannot be evaluated |
arrays.mlw | TO DISCUSS (no CE, because of polymorphism) | |
double_projection.mlw | OK | cannot be evaluated |
floats.mlw | OK !311 (closed) |
#640 (closed), both RAC terminated because cannot import value from model (not implemented for floats) |
if_decision_branch.mlw | OK | a priori OK - TODO move to check-ce |
int.mlw | OK |
#640 (closed), cannot be evaluated
|
int_overflow.mlw | OK |
FAILURE (postcondition at unknown location) might be related to #640 (closed)? |
jlamp_array.mlw | TO DISCUSS (CE not complete, polymorphism?) | cannot be evaluated |
list.mlw | TO DISCUSS (no CE, because of polymorphism) | |
loop_inv_real.mlw | OK | fails with anomaly: "Assert_failure src/mlw/pinterp_core.ml:1185:52"
|
map.mlw | OK #354 (closed) |
#640 (closed), both RAC terminated because cannot import value from model (not implemented for fractions) |
polymorphism.mlw | TO DISCUSS (no CE, because of polymorphism) | |
range_type_float.mlw | OK | cannot import value from model: not implemented for value 10.0 |
real.mlw | OK |
#640 (closed), cannot import value from model
|
ref_ex.mlw | TO DISCUSS (in postcondition of incr , !y is interpreted as old y ?) + see #355
|
|
ref_mono.mlw | TO DISCUSS (in postcondition of incr , !y is interpreted as old y ) + see #355
|
|
strings.mlw | TO DISCUSS (values of strings seem strange?) |
#640 (closed), cannot be evaluated
|