Commit cd1ec6e2 by MARCHE Claude

### CE/records: remove useless labels + new tests

parent 4543a604
 (***************************************** ** Getting counterexamples for records ** *****************************************) module M use import ref.Ref use import list.List use import int.Int (***************************************** ** Getting counterexamples for records ** *****************************************) (*** In all cases, records are decomposed using match eval ***) type r = {f "model_trace:.field_f" :int; g:bool} (* Projection functions *) function projf_r_f "model_trace:.f" (x : r) : int = x.f function projf_r_g "model_trace:.g" (x : r) : bool = x.g meta "inline : no" function projf_r_f meta "model_projection" function projf_r_f meta "inline : no" function projf_r_g meta "model_projection" function projf_r_g type r = {f "model_trace:.my_field_f" :int; g:bool} let record_match_eval_test1 (x : r) : int ensures { result = 1 } ensures { result = 1 } = if x.g then x.f else 1 let record_match_eval_test2 (x "model_projected" : r ) : int ensures { result = 1 } let record_match_eval_test2 (x : r ) : int ensures { result = 1 } = x.f x.f let record_match_eval_test3 (x : ref r) : unit ensures { !x.g } ensures { !x.g } = x := { !x with f = 6} x := { !x with f = 6} let record_match_eval_test4 (x : ref r) : r ensures { result.g } ensures { result.g } = x := { !x with f = 6 }; !x x := { !x with f = 6 }; !x val re "model_projected" : ref r val re : ref r let test_record_match_eval_test5 (x : ref r) : r ensures { result = !re } ensures { result = !re } = x := { !x with f = 6 }; !x end module Mutable use import int.Int type r = {mutable f "model_trace:.my_field_f" :int; mutable g:bool} let record_match_eval_test1 (x : r) : int ensures { result = 1 } = if x.g then x.f else 1 let record_match_eval_test2 (x : r ) : int ensures { result = 1 } = x.f let record_match_eval_test3 (x : r) : unit ensures { x.g } = x.f <- 6 let record_match_eval_test4 (x : r) : r ensures { result.g } = x := { !x with f = 6 }; !x x.f <- 6; x end
 bench/ce/records.mlw M WP_parameter record_match_eval_test1 : Unknown (other) Counter-example model:File records.mlw: Line 27: x.field_f = {"type" : "Integer" , "val" : "0" } Line 14: x.my_field_f = {"type" : "Integer" , "val" : "0" } x.g = {"type" : "Boolean" , "val" : true } Line 28: Line 15: old x.g = {"type" : "Boolean" , "val" : true } old x.field_f = {"type" : "Integer" , old x.my_field_f = {"type" : "Integer" , "val" : "0" } bench/ce/records.mlw M WP_parameter record_match_eval_test2 : Unknown (other) Counter-example model:File records.mlw: Line 35: x.field_f = {"type" : "Integer" , Line 22: x.my_field_f = {"type" : "Integer" , "val" : "0" } Line 36: old x.field_f = {"type" : "Integer" , Line 23: old x.my_field_f = {"type" : "Integer" , "val" : "0" } bench/ce/records.mlw M WP_parameter record_match_eval_test3 : Unknown (other) Counter-example model:File records.mlw: Line 40: Line 27: x.g = {"type" : "Boolean" , "val" : false } Line 43: x.field_f = {"type" : "Integer" , "val" : "6" } Line 30: x.my_field_f = {"type" : "Integer" , "val" : "6" } x.g = {"type" : "Boolean" , "val" : false } bench/ce/records.mlw M WP_parameter record_match_eval_test4 : Unknown (other) Counter-example model:File records.mlw: Line 45: Line 32: x.g = {"type" : "Boolean" , "val" : false } Line 48: x.field_f = {"type" : "Integer" , "val" : "6" } Line 35: x.my_field_f = {"type" : "Integer" , "val" : "6" } x.g = {"type" : "Boolean" , "val" : false } bench/ce/records.mlw M WP_parameter test_record_match_eval_test5 : Unknown (other) Counter-example model:File ref.mlw: Line 18: old re.field_f = {"type" : "Integer" , old re.my_field_f = {"type" : "Integer" , "val" : "0" } old re.g = {"type" : "Boolean" , "val" : false } x.field_f = {"type" : "Integer" , x.my_field_f = {"type" : "Integer" , "val" : "6" } x.g = {"type" : "Boolean" , "val" : false } File records.mlw: Line 51: re.field_f = {"type" : "Integer" , "val" : "0" } Line 38: re.my_field_f = {"type" : "Integer" , "val" : "0" } re.g = {"type" : "Boolean" , "val" : false } Line 53: Line 40: x.g = {"type" : "Boolean" , "val" : false } Line 43: x.my_field_f = {"type" : "Integer" , "val" : "6" } x.g = {"type" : "Boolean" , "val" : false } bench/ce/records.mlw Mutable WP_parameter record_match_eval_test1 : Unknown (other) Counter-example model:File records.mlw: Line 55: x.my_field_f = {"type" : "Integer" , "val" : "0" } x.g = {"type" : "Boolean" , "val" : true } Line 56: x.field_f = {"type" : "Integer" , "val" : "6" } old x.g = {"type" : "Boolean" , "val" : true } old x.my_field_f = {"type" : "Integer" , "val" : "0" } bench/ce/records.mlw Mutable WP_parameter record_match_eval_test2 : Unknown (other) Counter-example model:File records.mlw: Line 63: x.my_field_f = {"type" : "Integer" , "val" : "0" } Line 64: old x.my_field_f = {"type" : "Integer" , "val" : "0" } bench/ce/records.mlw Mutable WP_parameter record_match_eval_test3 : Unknown (other) Counter-example model:File records.mlw: Line 68: x.g = {"type" : "Boolean" , "val" : false } bench/ce/records.mlw Mutable WP_parameter record_match_eval_test4 : Unknown (other) Counter-example model:File records.mlw: Line 73: x.g = {"type" : "Boolean" , "val" : false } bench/ce/records.mlw M WP_parameter record_match_eval_test1 : Unknown (other) Counter-example model:File records.mlw: Line 27: x.field_f = {"type" : "Integer" , "val" : "0" } Line 14: x.my_field_f = {"type" : "Integer" , "val" : "0" } x.g = {"type" : "Boolean" , "val" : true } Line 28: Line 15: the check fails with all inputs bench/ce/records.mlw M WP_parameter record_match_eval_test2 : Unknown (other) Counter-example model:File records.mlw: Line 35: x.field_f = {"type" : "Integer" , Line 22: x.my_field_f = {"type" : "Integer" , "val" : "0" } Line 36: old x.field_f = {"type" : "Integer" , Line 23: old x.my_field_f = {"type" : "Integer" , "val" : "0" } bench/ce/records.mlw M WP_parameter record_match_eval_test3 : Unknown (other) Counter-example model:File records.mlw: Line 40: Line 27: x.g = {"type" : "Boolean" , "val" : false } Line 43: x.field_f = {"type" : "Integer" , "val" : "6" } Line 30: x.my_field_f = {"type" : "Integer" , "val" : "6" } x.g = {"type" : "Boolean" , "val" : false } bench/ce/records.mlw M WP_parameter record_match_eval_test4 : Unknown (other) Counter-example model:File records.mlw: Line 45: Line 32: x.g = {"type" : "Boolean" , "val" : false } Line 48: x.field_f = {"type" : "Integer" , "val" : "6" } Line 35: x.my_field_f = {"type" : "Integer" , "val" : "6" } x.g = {"type" : "Boolean" , "val" : false } bench/ce/records.mlw M WP_parameter test_record_match_eval_test5 : Unknown (other) Counter-example model:File records.mlw: Line 51: re.field_f = {"type" : "Integer" , "val" : "7" } Line 38: re.my_field_f = {"type" : "Integer" , "val" : "7" } re.g = {"type" : "Boolean" , "val" : false } Line 53: Line 40: x.g = {"type" : "Boolean" , "val" : false } Line 54: old re.field_f = {"type" : "Integer" , Line 41: old re.my_field_f = {"type" : "Integer" , "val" : "7" } old re.g = {"type" : "Boolean" , "val" : false } Line 43: x.my_field_f = {"type" : "Integer" , "val" : "6" } x.g = {"type" : "Boolean" , "val" : false } bench/ce/records.mlw Mutable WP_parameter record_match_eval_test1 : Unknown (other) Counter-example model:File records.mlw: Line 55: x.my_field_f = {"type" : "Integer" , "val" : "0" } x.g = {"type" : "Boolean" , "val" : true } Line 56: x.field_f = {"type" : "Integer" , "val" : "6" } the check fails with all inputs bench/ce/records.mlw Mutable WP_parameter record_match_eval_test2 : Unknown (other) Counter-example model:File records.mlw: Line 63: x.my_field_f = {"type" : "Integer" , "val" : "0" } Line 64: old x.my_field_f = {"type" : "Integer" , "val" : "0" } bench/ce/records.mlw Mutable WP_parameter record_match_eval_test3 : Unknown (other) Counter-example model:File records.mlw: Line 68: x.my_field_f = {"type" : "Integer" , "val" : "0" } x.g = {"type" : "Boolean" , "val" : false } Line 71: x.my_field_f = {"type" : "Integer" , "val" : "6" } x.g = {"type" : "Boolean" , "val" : false } bench/ce/records.mlw Mutable WP_parameter record_match_eval_test4 : Unknown (other) Counter-example model:File records.mlw: Line 73: x.my_field_f = {"type" : "Integer" , "val" : "0" } x.g = {"type" : "Boolean" , "val" : false } Line 76: x.my_field_f = {"type" : "Integer" , "val" : "6" } x.g = {"type" : "Boolean" , "val" : false }
 bench/ce/records.mlw M WP_parameter record_match_eval_test1 : Unknown (other) Counter-example model:File records.mlw: Line 27: x.field_f = {"type" : "Integer" , "val" : "3" } Line 14: x.my_field_f = {"type" : "Integer" , "val" : "3" } x.g = {"type" : "Boolean" , "val" : true } Line 28: Line 15: old x.g = {"type" : "Boolean" , "val" : true } old x.field_f = {"type" : "Integer" , old x.my_field_f = {"type" : "Integer" , "val" : "3" } bench/ce/records.mlw M WP_parameter record_match_eval_test2 : Unknown (other) Counter-example model:File records.mlw: Line 35: x.field_f = {"type" : "Integer" , Line 22: x.my_field_f = {"type" : "Integer" , "val" : "3" } Line 36: old x.field_f = {"type" : "Integer" , Line 23: old x.my_field_f = {"type" : "Integer" , "val" : "3" } bench/ce/records.mlw M WP_parameter record_match_eval_test3 : Unknown (other) Counter-example model:File records.mlw: Line 40: Line 27: x.g = {"type" : "Boolean" , "val" : false } Line 43: x.field_f = {"type" : "Integer" , "val" : "6" } Line 30: x.my_field_f = {"type" : "Integer" , "val" : "6" } x.g = {"type" : "Boolean" , "val" : false } bench/ce/records.mlw M WP_parameter record_match_eval_test4 : Unknown (other) Counter-example model:File records.mlw: Line 45: Line 32: x.g = {"type" : "Boolean" , "val" : false } Line 48: x.field_f = {"type" : "Integer" , "val" : "6" } Line 35: x.my_field_f = {"type" : "Integer" , "val" : "6" } x.g = {"type" : "Boolean" , "val" : false } bench/ce/records.mlw M WP_parameter test_record_match_eval_test5 : Unknown (other) Counter-example model:File ref.mlw: Line 18: old re.field_f = {"type" : "Integer" , old re.my_field_f = {"type" : "Integer" , "val" : "3" } old re.g = {"type" : "Boolean" , "val" : false } x.field_f = {"type" : "Integer" , x.my_field_f = {"type" : "Integer" , "val" : "6" } x.g = {"type" : "Boolean" , "val" : false } File records.mlw: Line 51: re.field_f = {"type" : "Integer" , "val" : "3" } Line 38: re.my_field_f = {"type" : "Integer" , "val" : "3" } re.g = {"type" : "Boolean" , "val" : false } Line 53: Line 40: x.g = {"type" : "Boolean" , "val" : false } Line 43: x.my_field_f = {"type" : "Integer" , "val" : "6" } x.g = {"type" : "Boolean" , "val" : false } bench/ce/records.mlw Mutable WP_parameter record_match_eval_test1 : Unknown (other) Counter-example model:File records.mlw: Line 55: x.my_field_f = {"type" : "Integer" , "val" : "0" } x.g = {"type" : "Boolean" , "val" : true } Line 56: x.field_f = {"type" : "Integer" , "val" : "6" } old x.g = {"type" : "Boolean" , "val" : true } old x.my_field_f = {"type" : "Integer" , "val" : "0" } bench/ce/records.mlw Mutable WP_parameter record_match_eval_test2 : Unknown (other) Counter-example model:File records.mlw: Line 63: x.my_field_f = {"type" : "Integer" , "val" : "0" } Line 64: old x.my_field_f = {"type" : "Integer" , "val" : "0" } bench/ce/records.mlw Mutable WP_parameter record_match_eval_test3 : Unknown (other) Counter-example model:File records.mlw: Line 68: x.g = {"type" : "Boolean" , "val" : false } bench/ce/records.mlw Mutable WP_parameter record_match_eval_test4 : Unknown (other) Counter-example model:File records.mlw: Line 73: x.g = {"type" : "Boolean" , "val" : false } bench/ce/records.mlw M WP_parameter record_match_eval_test1 : Unknown (other) Counter-example model:File records.mlw: Line 27: x.field_f = {"type" : "Integer" , "val" : "3" } Line 14: x.my_field_f = {"type" : "Integer" , "val" : "3" } x.g = {"type" : "Boolean" , "val" : true } Line 28: Line 15: the check fails with all inputs bench/ce/records.mlw M WP_parameter record_match_eval_test2 : Unknown (other) Counter-example model:File records.mlw: Line 35: x.field_f = {"type" : "Integer" , Line 22: x.my_field_f = {"type" : "Integer" , "val" : "3" } Line 36: old x.field_f = {"type" : "Integer" , Line 23: old x.my_field_f = {"type" : "Integer" , "val" : "3" } bench/ce/records.mlw M WP_parameter record_match_eval_test3 : Unknown (other) Counter-example model:File records.mlw: Line 40: Line 27: x.g = {"type" : "Boolean" , "val" : false } Line 43: x.field_f = {"type" : "Integer" , "val" : "6" } Line 30: x.my_field_f = {"type" : "Integer" , "val" : "6" } x.g = {"type" : "Boolean" , "val" : false } bench/ce/records.mlw M WP_parameter record_match_eval_test4 : Unknown (other) Counter-example model:File records.mlw: Line 45: Line 32: x.g = {"type" : "Boolean" , "val" : false } Line 48: x.field_f = {"type" : "Integer" , "val" : "6" } Line 35: x.my_field_f = {"type" : "Integer" , "val" : "6" } x.g = {"type" : "Boolean" , "val" : false } bench/ce/records.mlw M WP_parameter test_record_match_eval_test5 : Unknown (other) Counter-example model:File records.mlw: Line 51: re.field_f = {"type" : "Integer" , "val" : "2" } Line 38: re.my_field_f = {"type" : "Integer" , "val" : "2" } re.g = {"type" : "Boolean" , "val" : false } Line 53: Line 40: x.g = {"type" : "Boolean" , "val" : false } Line 54: old re.field_f = {"type" : "Integer" , Line 41: old re.my_field_f = {"type" : "Integer" , "val" : "2" } old re.g = {"type" : "Boolean" , "val" : false } Line 43: x.my_field_f = {"type" : "Integer" , "val" : "6" } x.g = {"type" : "Boolean" , "val" : false } bench/ce/records.mlw Mutable WP_parameter record_match_eval_test1 : Unknown (other) Counter-example model:File records.mlw: Line 55: x.my_field_f = {"type" : "Integer" , "val" : "0" } x.g = {"type" : "Boolean" , "val" : true } Line 56: x.field_f = {"type" : "Integer" , "val" : "6" } the check fails with all inputs bench/ce/records.mlw Mutable WP_parameter record_match_eval_test2 : Unknown (other) Counter-example model:File records.mlw: Line 63: x.my_field_f = {"type" : "Integer" , "val" : "0" } Line 64: old x.my_field_f = {"type" : "Integer" , "val" : "0" } bench/ce/records.mlw Mutable WP_parameter record_match_eval_test3 : Unknown (other) Counter-example model:File records.mlw: Line 68: x.g = {"type" : "Boolean" , "val" : false } Line 71: x.my_field_f = {"type" : "Integer" , "val" : "6" } x.g = {"type" : "Boolean" , "val" : false } bench/ce/records.mlw Mutable WP_parameter record_match_eval_test4 : Unknown (other) Counter-example model:File records.mlw: Line 73: x.g = {"type" : "Boolean" , "val" : false } Line 76: x.my_field_f = {"type" : "Integer" , "val" : "6" } x.g = {"type" : "Boolean" , "val" : false }
 bench/ce/records.mlw M WP_parameter record_match_eval_test1 : Unknown (other) Counter-example model:File records.mlw: Line 27: x.field_f = {"type" : "Integer" , "val" : "3" } Line 14: x.my_field_f = {"type" : "Integer" , "val" : "3" } x.g = {"type" : "Boolean" , "val" : true } Line 28: Line 15: old x.g = {"type" : "Boolean" , "val" : true } old x.field_f = {"type" : "Integer" , old x.my_field_f = {"type" : "Integer" , "val" : "3" } bench/ce/records.mlw M WP_parameter record_match_eval_test2 : Unknown (other) Counter-example model:File records.mlw: Line 35: x.field_f = {"type" : "Integer" , Line 22: x.my_field_f = {"type" : "Integer" , "val" : "3" } Line 36: old x.field_f = {"type" : "Integer" , Line 23: old x.my_field_f = {"type" : "Integer" , "val" : "3" } bench/ce/records.mlw M WP_parameter record_match_eval_test3 : Unknown (other) Counter-example model:File records.mlw: Line 40: Line 27: x.g = {"type" : "Boolean" , "val" : false } Line 43: x.field_f = {"type" : "Integer" , "val" : "6" } Line 30: x.my_field_f = {"type" : "Integer" , "val" : "6" } x.g = {"type" : "Boolean" , "val" : false } bench/ce/records.mlw M WP_parameter record_match_eval_test4 : Unknown (other) Counter-example model:File records.mlw: Line 45: