diff --git a/examples/lwt_dllist_tests.ml b/examples/lwt_dllist_tests.ml index 867109ab..5ea84593 100644 --- a/examples/lwt_dllist_tests.ml +++ b/examples/lwt_dllist_tests.ml @@ -335,7 +335,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ = then None else Some - ("is_empty", + ((Some (Res (Ortac_runtime.dummy, ()))), "is_empty", [("b <-> s.contents = Sequence.empty", { Ortac_runtime.start = @@ -383,7 +383,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ = then None else Some - ("length", + ((Some (Res (Ortac_runtime.dummy, ()))), "length", [("l = Sequence.length s.contents", { Ortac_runtime.start = @@ -440,7 +440,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ = then None else Some - ("take_l", + ((Some (Res (Ortac_runtime.dummy, ()))), "take_l", [("if old s.contents = Sequence.empty\n then false\n else a = Sequence.hd (old s.contents)", { Ortac_runtime.start = @@ -492,7 +492,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ = then None else Some - ("take_l", + (None, "take_l", [("old s.contents = Sequence.empty = s.contents", { Ortac_runtime.start = @@ -552,7 +552,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ = then None else Some - ("take_r", + ((Some (Res (Ortac_runtime.dummy, ()))), "take_r", [("if old s.contents = Sequence.empty\n then false\n else a = (old s.contents)[Sequence.length (old s.contents) - 1]", { Ortac_runtime.start = @@ -604,7 +604,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ = then None else Some - ("take_r", + (None, "take_r", [("old s.contents = Sequence.empty = s.contents", { Ortac_runtime.start = @@ -656,7 +656,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ = then None else Some - ("take_opt_l", + ((Some (Res (Ortac_runtime.dummy, ()))), "take_opt_l", [("old s.contents = match o with\n | None -> Sequence.empty\n | Some a -> Sequence.cons a s.contents", { Ortac_runtime.start = @@ -707,7 +707,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ = then None else Some - ("take_opt_r", + ((Some (Res (Ortac_runtime.dummy, ()))), "take_opt_r", [("old s.contents = match o with\n | None -> Sequence.empty\n | Some a -> Sequence.snoc s.contents a", { Ortac_runtime.start = diff --git a/examples/varray_circular_tests.ml b/examples/varray_circular_tests.ml index 50ebc7a0..a920c141 100644 --- a/examples/varray_circular_tests.ml +++ b/examples/varray_circular_tests.ml @@ -759,7 +759,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("pop_back", + ((Some (Res (Ortac_runtime.dummy, ()))), "pop_back", [("if old t.contents = Sequence.empty\n then false\n else proj x = (old t.contents)[Sequence.length (old t.contents) - 1]", { Ortac_runtime.start = @@ -811,7 +811,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("pop_back", + (None, "pop_back", [("t.contents = old t.contents = Sequence.empty", { Ortac_runtime.start = @@ -868,7 +868,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("pop_front", + ((Some (Res (Ortac_runtime.dummy, ()))), "pop_front", [("if old t.contents = Sequence.empty\n then false\n else proj x = Sequence.hd (old t.contents)", { Ortac_runtime.start = @@ -920,7 +920,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("pop_front", + (None, "pop_front", [("t.contents = old t.contents = Sequence.empty", { Ortac_runtime.start = @@ -976,7 +976,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("insert_at", + (None, "insert_at", [("0 <= i <= Sequence.length t.contents", { Ortac_runtime.start = @@ -1038,7 +1038,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("insert_at", + (None, "insert_at", [("0 <= i <= Sequence.length t.contents", { Ortac_runtime.start = @@ -1086,7 +1086,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("pop_at", + (None, "pop_at", [("inside i t.contents", { Ortac_runtime.start = @@ -1140,7 +1140,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("pop_at", + ((Some (Res (Ortac_runtime.dummy, ()))), "pop_at", [("(proj x) = old t.contents[i]", { Ortac_runtime.start = @@ -1195,7 +1195,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("pop_at", + (None, "pop_at", [("inside i t.contents", { Ortac_runtime.start = @@ -1243,7 +1243,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("delete_at", + (None, "delete_at", [("inside i t.contents", { Ortac_runtime.start = @@ -1300,7 +1300,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("delete_at", + ((Some (Res (unit, ()))), "delete_at", [("Sequence.length t.contents = Sequence.length (old t.contents) - 1", { Ortac_runtime.start = @@ -1355,7 +1355,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("delete_at", + (None, "delete_at", [("inside i t.contents", { Ortac_runtime.start = @@ -1403,7 +1403,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("get", + (None, "get", [("inside i t.contents", { Ortac_runtime.start = @@ -1457,7 +1457,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("get", + ((Some (Res (Ortac_runtime.dummy, ()))), "get", [("(proj x) = t.contents[i]", { Ortac_runtime.start = @@ -1512,7 +1512,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("get", + (None, "get", [("inside i t.contents", { Ortac_runtime.start = @@ -1560,7 +1560,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("set", + (None, "set", [("inside i t.contents", { Ortac_runtime.start = @@ -1616,7 +1616,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("set", + (None, "set", [("inside i t.contents", { Ortac_runtime.start = @@ -1664,7 +1664,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("length", + ((Some (Res (Ortac_runtime.dummy, ()))), "length", [("l = Sequence.length t.contents", { Ortac_runtime.start = @@ -1712,7 +1712,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("is_empty", + ((Some (Res (Ortac_runtime.dummy, ()))), "is_empty", [("b <-> t.contents = Sequence.empty", { Ortac_runtime.start = @@ -1775,7 +1775,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("fill", + (None, "fill", [("0 <= pos /\\ 0 <= len /\\ pos + len < Sequence.length t.contents", { Ortac_runtime.start = @@ -1847,7 +1847,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("fill", + (None, "fill", [("0 <= pos /\\ 0 <= len /\\ pos + len < Sequence.length t.contents", { Ortac_runtime.start = diff --git a/examples/varray_tests.ml b/examples/varray_tests.ml index 9f3a22e4..9c3c66d9 100644 --- a/examples/varray_tests.ml +++ b/examples/varray_tests.ml @@ -759,7 +759,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("pop_back", + ((Some (Res (Ortac_runtime.dummy, ()))), "pop_back", [("if old t.contents = Sequence.empty\n then false\n else proj x = (old t.contents)[Sequence.length (old t.contents) - 1]", { Ortac_runtime.start = @@ -811,7 +811,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("pop_back", + (None, "pop_back", [("t.contents = old t.contents = Sequence.empty", { Ortac_runtime.start = @@ -868,7 +868,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("pop_front", + ((Some (Res (Ortac_runtime.dummy, ()))), "pop_front", [("if old t.contents = Sequence.empty\n then false\n else proj x = Sequence.hd (old t.contents)", { Ortac_runtime.start = @@ -920,7 +920,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("pop_front", + (None, "pop_front", [("t.contents = old t.contents = Sequence.empty", { Ortac_runtime.start = @@ -976,7 +976,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("insert_at", + (None, "insert_at", [("0 <= i <= Sequence.length t.contents", { Ortac_runtime.start = @@ -1036,7 +1036,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("insert_at", + (None, "insert_at", [("0 <= i <= Sequence.length t.contents", { Ortac_runtime.start = @@ -1084,7 +1084,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("pop_at", + (None, "pop_at", [("inside i t.contents", { Ortac_runtime.start = @@ -1136,7 +1136,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("pop_at", + ((Some (Res (Ortac_runtime.dummy, ()))), "pop_at", [("(proj x) = old t.contents[i]", { Ortac_runtime.start = @@ -1189,7 +1189,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("pop_at", + (None, "pop_at", [("inside i t.contents", { Ortac_runtime.start = @@ -1237,7 +1237,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("delete_at", + (None, "delete_at", [("inside i t.contents", { Ortac_runtime.start = @@ -1292,7 +1292,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("delete_at", + ((Some (Res (unit, ()))), "delete_at", [("Sequence.length t.contents = Sequence.length (old t.contents) - 1", { Ortac_runtime.start = @@ -1345,7 +1345,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("delete_at", + (None, "delete_at", [("inside i t.contents", { Ortac_runtime.start = @@ -1393,7 +1393,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("get", + (None, "get", [("inside i t.contents", { Ortac_runtime.start = @@ -1445,7 +1445,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("get", + ((Some (Res (Ortac_runtime.dummy, ()))), "get", [("(proj x) = t.contents[i]", { Ortac_runtime.start = @@ -1498,7 +1498,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("get", + (None, "get", [("inside i t.contents", { Ortac_runtime.start = @@ -1546,7 +1546,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("set", + (None, "set", [("inside i t.contents", { Ortac_runtime.start = @@ -1600,7 +1600,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("set", + (None, "set", [("inside i t.contents", { Ortac_runtime.start = @@ -1648,7 +1648,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("length", + ((Some (Res (Ortac_runtime.dummy, ()))), "length", [("l = Sequence.length t.contents", { Ortac_runtime.start = @@ -1696,7 +1696,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("is_empty", + ((Some (Res (Ortac_runtime.dummy, ()))), "is_empty", [("b <-> t.contents = Sequence.empty", { Ortac_runtime.start = @@ -1759,7 +1759,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("fill", + (None, "fill", [("0 <= pos /\\ 0 <= len /\\ pos + len < Sequence.length t.contents", { Ortac_runtime.start = @@ -1829,7 +1829,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("fill", + (None, "fill", [("0 <= pos /\\ 0 <= len /\\ pos + len < Sequence.length t.contents", { Ortac_runtime.start = diff --git a/plugins/qcheck-stm/doc/index.mld b/plugins/qcheck-stm/doc/index.mld index 435f5df8..0b6e20fd 100644 --- a/plugins/qcheck-stm/doc/index.mld +++ b/plugins/qcheck-stm/doc/index.mld @@ -263,6 +263,10 @@ val type_not_supported : new_type -> 'a t -> new_type {@sh[ $ ortac qcheck-stm example_unknown_type.mli "make 42 'a'" "char t" -o foo.ml +File "example_unknown_type.mli", line 15, characters 0-87: +15 | val type_not_supported : new_type -> 'a t -> new_type +16 | (*@ y = type_not_supported x t *) +Warning: Incomplete computation of the returned value in the specification of type_not_supported. Failure message won't be able to display the expected returned value. $ grep -A 1 "type cmd" foo.ml type cmd = | Type_not_supported of new_type @@ -348,6 +352,11 @@ the command will generate the following warning: {@sh[ $ ortac qcheck-stm example_ill_formed_quantification.mli "make 42 'a'" "char t" -o foo.ml +File "example_ill_formed_quantification.mli", line 13, characters 0-142: +13 | val unsupported_quantification : 'a t -> bool +14 | (*@ b = unsupported_quantification t +15 | ensures b = forall a. List.mem a t.contents -> a = a *) +Warning: Incomplete computation of the returned value in the specification of unsupported_quantification. Failure message won't be able to display the expected returned value. File "example_ill_formed_quantification.mli", line 15, characters 16-56: 15 | ensures b = forall a. List.mem a t.contents -> a = a *) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ @@ -422,6 +431,10 @@ File "example_limitations.mli", line 28, characters 15-25: 28 | val for_all : ('a -> bool) -> 'a t -> bool ^^^^^^^^^^ Warning: Skipping for_all: functions are not supported yet as arguments. +File "example_limitations.mli", line 22, characters 0-50: +22 | val g : int * int -> 'a t -> bool +23 | (*@ b = g x t *) +Warning: Incomplete computation of the returned value in the specification of g. Failure message won't be able to display the expected returned value. File "example_limitations.mli", line 22, characters 8-17: 22 | val g : int * int -> 'a t -> bool ^^^^^^^^^ diff --git a/plugins/qcheck-stm/src/runtime/ortac_runtime_qcheck_stm.ml b/plugins/qcheck-stm/src/runtime/ortac_runtime_qcheck_stm.ml index d0030338..26b832e2 100644 --- a/plugins/qcheck-stm/src/runtime/ortac_runtime_qcheck_stm.ml +++ b/plugins/qcheck-stm/src/runtime/ortac_runtime_qcheck_stm.ml @@ -4,36 +4,50 @@ include Ortac_runtime let ( ++ ) a b = match (a, b) with | None, None -> None - | Some (_, _), None -> a - | None, Some (_, _) -> b - | Some (cmd0, terms0), Some (cmd1, terms1) -> + | Some (_, _, _), None -> a + | None, Some (_, _, _) -> b + | Some (ret, cmd0, terms0), Some (_, cmd1, terms1) -> assert (cmd0 = cmd1); - Some (cmd0, terms0 @ terms1) + Some (ret, cmd0, terms0 @ terms1) + +type _ ty += Dummy : _ ty + +let dummy = (Dummy, fun _ -> Printf.sprintf "unknown value") module Make (Spec : Spec) = struct open QCheck module Internal = Internal.Make (Spec) [@alert "-internal"] - let pp_trace ppf trace = + let pp_trace ppf (trace, ret) = let open Fmt in - let pp_aux ppf (c, r) = - pf ppf "ignore (%s); (* returned %s *)" (Spec.show_cmd c) (show_res r) + let pp_expected ppf = function + | Some ret -> pf ppf ", expected %s" (show_res ret) + | None -> () + in + let rec aux ppf = function + | [ (c, r) ] -> + pf ppf "ignore (%s); (* returned %s%a *)" + (Spec.show_cmd c) (show_res r) pp_expected ret + | (c, r) :: xs -> + pf ppf "ignore (%s); (* returned %s *)" (Spec.show_cmd c) (show_res r); + aux ppf xs + | _ -> assert false in - pf ppf "@[let sut = init_sut in@\n%a@]" (list ~sep:(any "@\n") pp_aux) trace + pf ppf "@[let sut = init_sut in@\n%a@]" aux trace let pp_terms ppf err = let open Fmt in let pp_aux ppf (term, l) = pf ppf "@[%a@\n @[%s@]@]@\n" pp_loc l term in pf ppf "%a" (list ~sep:(any "@\n") pp_aux) err - let message trace cmd terms = + let message trace ret cmd terms = Test.fail_reportf "Gospel specification violation in function %s\n\ @;\ \ @[%a@]@\n\ when executing the following sequence of operations:@\n\ @;\ - \ @[%a@]@." cmd pp_terms terms pp_trace trace + \ @[%a@]@." cmd pp_terms terms pp_trace (trace, ret) let rec check_disagree postcond s sut cs = match cs with @@ -48,8 +62,9 @@ module Make (Spec : Spec) = struct let s' = Spec.next_state c s in match check_disagree postcond s' sut cs with | None -> None - | Some (rest, cmd, terms) -> Some ((c, res) :: rest, cmd, terms)) - | Some (cmd, terms) -> Some ([ (c, res) ], cmd, terms)) + | Some (rest, ret, cmd, terms) -> + Some ((c, res) :: rest, ret, cmd, terms)) + | Some (ret, cmd, terms) -> Some ([ (c, res) ], ret, cmd, terms)) let agree_prop wrapped_init_state postcond cs = let _ = wrapped_init_state () in @@ -64,7 +79,7 @@ module Make (Spec : Spec) = struct let res = match res with Ok res -> res | Error exn -> raise exn in match res with | None -> true - | Some (trace, cmd, terms) -> message trace cmd terms + | Some (trace, ret, cmd, terms) -> message trace ret cmd terms let agree_test ~count ~name wrapped_init_state postcond = Test.make ~name ~count diff --git a/plugins/qcheck-stm/src/stm_of_ir.ml b/plugins/qcheck-stm/src/stm_of_ir.ml index 2b7766b2..22648de6 100644 --- a/plugins/qcheck-stm/src/stm_of_ir.ml +++ b/plugins/qcheck-stm/src/stm_of_ir.ml @@ -9,6 +9,7 @@ let pat_default = ppat_construct (lident "Char") None let exp_default = evar "char" let res_default = Ident.create ~loc:Location.none "res" let list_mappend = list_fold_expr "++" "None" +let res = lident "Res" let may_raise_exception v = match (v.postcond.exceptional, v.postcond.checks) with @@ -282,7 +283,6 @@ let run_case config sut_name value = let lhs = mk_cmd_pattern value in let open Reserr in let* rhs = - let res = lident "Res" in let* ty_show = exp_of_core_type value.inst (Ir.get_return_type value) in let ty_show = if may_raise_exception value then @@ -432,6 +432,30 @@ let precond config ir = in pstr_value Nonrecursive [ value_binding ~pat ~expr ] |> ok +let returned_value translate_postcond value = + let open Reserr in + let ty_ret = Ir.get_return_type value in + let ret_val = + match (ty_ret.ptyp_desc, value.ret_values) with + | Ptyp_constr ({ txt = Lident "unit"; _ }, _), _ -> Some eunit + | Ptyp_tuple _, _ -> + failwith + "shouldn't happen (functions returning tuples are filtered out \ + before)" + | _, [ xs ] -> + Option.bind + (to_option @@ map translate_postcond xs) + (Fun.flip List.nth_opt 0) + (* type of the returned value will be checked later with a proper error *) + | _, _ -> None + in + let ty_show = to_option @@ exp_of_core_type value.inst ty_ret in + match (ty_show, ret_val) with + | Some ty_show, Some ret_values -> + let args = pexp_tuple_opt [ ty_show; ret_values ] in + Some (pexp_construct res args) + | _, _ -> None + let postcond_case config state invariants idx state_ident new_state_ident value = let open Reserr in @@ -443,12 +467,37 @@ let postcond_case config state invariants idx state_ident new_state_ident value subst_term state ~gos_t:id ~old_t:None ~new_t:(Some new_state_ident) ~new_lz:true t >>= ocaml_of_term config - and wrap_check t e = + and dummy = + let ty_show = qualify [ "Ortac_runtime" ] "dummy" and value = eunit in + let args = pexp_tuple_opt [ ty_show; value ] in + pexp_construct res args + in + let* ret_val = + (* simply warn the user if we can't compute the expected returned value, + don't skip the function *) + match returned_value translate_postcond value with + | None -> + let* () = + warn + ( Incomplete_ret_val_computation (Fmt.str "%a" Ident.pp value.id), + value.id.id_loc ) + in + ok @@ esome dummy + | Some e -> ok @@ esome e + in + let wrap_check ?(normal = false) t e = let term = estring t.text and cmd = Fmt.str "%a" Ident.pp value.id |> estring and l = t.Ir.term.Gospel.Tterm.t_loc |> elocation in pexp_ifthenelse e enone - (Some (esome @@ pexp_tuple [ cmd; elist [ pexp_tuple [ term; l ] ] ])) + (Some + (esome + @@ pexp_tuple + [ + (if normal then ret_val else enone); + cmd; + elist [ pexp_tuple [ term; l ] ]; + ])) in let idx = List.sort Int.compare idx in let lhs0 = mk_cmd_pattern value in @@ -499,11 +548,15 @@ let postcond_case config state invariants idx state_ident new_state_ident value in aux idx value.postcond.normal in - let* postcond = map (fun t -> wrap_check t <$> translate_postcond t) normal + let* postcond = + map (fun t -> wrap_check ~normal:true t <$> translate_postcond t) normal and* invariants = Option.fold ~none:(ok []) ~some:(fun (id, xs) -> - map (fun t -> wrap_check t <$> translate_invariants id t.term) xs) + map + (fun t -> + wrap_check ~normal:true t <$> translate_invariants id t.term) + xs) invariants in list_mappend (postcond @ invariants) |> ok diff --git a/plugins/qcheck-stm/test/all_warnings_errors.expected b/plugins/qcheck-stm/test/all_warnings_errors.expected index 81df1242..55ada85b 100644 --- a/plugins/qcheck-stm/test/all_warnings_errors.expected +++ b/plugins/qcheck-stm/test/all_warnings_errors.expected @@ -68,10 +68,32 @@ Warning: Skipping term_refer_to_returned_value_next_state: model contents is was found. Specifications should contain at least one "ensures x.contents = expr" where x is the SUT and expr can refer to the SUT only under an old operator and can't refer to the returned value. +File "all_warnings.mli", line 39, characters 0-66: +39 | val type_not_supported : 'a t -> s +40 | (*@ s = type_not_supported t *) +Warning: Incomplete computation of the returned value in the specification of type_not_supported. Failure message won't be able to display the expected returned value. +File "all_warnings.mli", line 51, characters 0-140: +51 | val unsupported_quantification : 'a t -> bool +52 | (*@ b = unsupported_quantification t +53 | ensures b = forall a. List.mem a t.contents -> p a *) +Warning: Incomplete computation of the returned value in the specification of unsupported_quantification. Failure message won't be able to display the expected returned value. File "all_warnings.mli", line 53, characters 16-54: 53 | ensures b = forall a. List.mem a t.contents -> p a *) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: Skipping clause: unsupported quantification. +File "all_warnings.mli", line 55, characters 0-111: +55 | val record_not_model_field : 'a t -> bool +56 | (*@ b = record_not_model_field t +57 | requires Array.length t.v > 0 *) +Warning: Incomplete computation of the returned value in the specification of record_not_model_field. Failure message won't be able to display the expected returned value. +File "all_warnings.mli", line 62, characters 0-278: +62 | val term_refer_to_returned_value_next_state : 'a t -> 'a option +63 | (*@ o = term_refer_to_returned_value_next_state t +64 | modifies t.contents +65 | ensures t.contents = match o with +66 | | None -> old t.contents +67 | | Some _ -> old t.contents *) +Warning: Incomplete computation of the returned value in the specification of term_refer_to_returned_value_next_state. Failure message won't be able to display the expected returned value. File "all_warnings.mli", line 57, characters 26-29: 57 | requires Array.length t.v > 0 *) ^^^ diff --git a/plugins/qcheck-stm/test/array_errors.expected b/plugins/qcheck-stm/test/array_errors.expected index e69de29b..6e8d89c1 100644 --- a/plugins/qcheck-stm/test/array_errors.expected +++ b/plugins/qcheck-stm/test/array_errors.expected @@ -0,0 +1,5 @@ +File "array.mli", line 38, characters 0-85: +38 | val mem : 'a -> 'a t -> bool +39 | (*@ b = mem a t +40 | ensures b = List.mem a t.contents *) +Warning: Incomplete computation of the returned value in the specification of mem. Failure message won't be able to display the expected returned value. diff --git a/plugins/qcheck-stm/test/array_stm_tests.expected.ml b/plugins/qcheck-stm/test/array_stm_tests.expected.ml index 7d900008..609c124e 100644 --- a/plugins/qcheck-stm/test/array_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/array_stm_tests.expected.ml @@ -364,7 +364,31 @@ let ortac_postcond cmd__008_ state__009_ res__010_ = then None else Some - ("length", + ((Some + (Res + (int, + ((try (Lazy.force new_state__011_).size + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 7; + pos_bol = 238; + pos_cnum = 254 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 7; + pos_bol = 238; + pos_cnum = 260 + } + }))))))), "length", [("i = t.size", { Ortac_runtime.start = @@ -419,7 +443,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ = then None else Some - ("get", + (None, "get", [("0 <= i < t.size", { Ortac_runtime.start = @@ -471,7 +495,35 @@ let ortac_postcond cmd__008_ state__009_ res__010_ = then None else Some - ("get", + ((Some + (Res + (char, + ((try + Ortac_runtime.Gospelstdlib.List.nth + (Lazy.force new_state__011_).contents + (Ortac_runtime.Gospelstdlib.integer_of_int + i) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 12; + pos_bol = 405; + pos_cnum = 421 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 12; + pos_bol = 405; + pos_cnum = 442 + } + }))))))), "get", [("a = List.nth t.contents i", { Ortac_runtime.start = @@ -530,7 +582,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ = then None else Some - ("get", + (None, "get", [("0 <= i < t.size", { Ortac_runtime.start = @@ -585,7 +637,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ = then None else Some - ("set", + (None, "set", [("0 <= i < t.size", { Ortac_runtime.start = @@ -645,7 +697,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ = then None else Some - ("set", + (None, "set", [("0 <= i < t.size", { Ortac_runtime.start = @@ -693,7 +745,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ = then None else Some - ("fill", + (None, "fill", [("0 <= i", { Ortac_runtime.start = @@ -741,7 +793,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ = then None else Some - ("fill", + (None, "fill", [("0 <= j", { Ortac_runtime.start = @@ -793,7 +845,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ = then None else Some - ("fill", + (None, "fill", [("i + j <= t.size", { Ortac_runtime.start = @@ -846,7 +898,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ = then None else Some - ("fill", + (None, "fill", [("0 <= i", { Ortac_runtime.start = @@ -894,7 +946,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ = then None else Some - ("fill", + (None, "fill", [("0 <= j", { Ortac_runtime.start = @@ -947,7 +999,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ = then None else Some - ("fill", + (None, "fill", [("i + j <= t.size", { Ortac_runtime.start = @@ -992,7 +1044,31 @@ let ortac_postcond cmd__008_ state__009_ res__010_ = then None else Some - ("to_list", + ((Some + (Res + ((list char), + ((try (Lazy.force new_state__011_).contents + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 36; + pos_bol = 1559; + pos_cnum = 1575 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 36; + pos_bol = 1559; + pos_cnum = 1585 + } + }))))))), "to_list", [("l = t.contents", { Ortac_runtime.start = @@ -1040,7 +1116,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ = then None else Some - ("mem", + ((Some (Res (Ortac_runtime.dummy, ()))), "mem", [("b = List.mem a t.contents", { Ortac_runtime.start = diff --git a/plugins/qcheck-stm/test/conjunctive_clauses_stm_tests.expected.ml b/plugins/qcheck-stm/test/conjunctive_clauses_stm_tests.expected.ml index 3e78a989..1668fa1e 100644 --- a/plugins/qcheck-stm/test/conjunctive_clauses_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/conjunctive_clauses_stm_tests.expected.ml @@ -198,7 +198,7 @@ let ortac_postcond cmd__006_ state__007_ res__008_ = then None else Some - ("set", + (None, "set", [("0 <= i < List.length t.contents", { Ortac_runtime.start = @@ -258,7 +258,7 @@ let ortac_postcond cmd__006_ state__007_ res__008_ = then None else Some - ("set", + (None, "set", [("0 <= i < List.length t.contents", { Ortac_runtime.start = diff --git a/plugins/qcheck-stm/test/hashtbl_errors.expected b/plugins/qcheck-stm/test/hashtbl_errors.expected index 66a3dfee..05e6eee9 100644 --- a/plugins/qcheck-stm/test/hashtbl_errors.expected +++ b/plugins/qcheck-stm/test/hashtbl_errors.expected @@ -115,7 +115,36 @@ File "hashtbl.mli", line 106, characters 0-54: ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: Skipping seeded_hash_param: functions without specifications cannot be tested. +File "hashtbl.mli", line 28, characters 0-226: +28 | val find : ('a, 'b) t -> 'a -> 'b +29 | (*@ b = find h a +30 | raises Not_found -> forall x. not (List.mem (a, x) h.contents) +31 | raises Not_found -> not (List.mem a (List.map fst h.contents)) +32 | ensures List.mem (a, b) h.contents *) +Warning: Incomplete computation of the returned value in the specification of find. Failure message won't be able to display the expected returned value. File "hashtbl.mli", line 30, characters 24-66: 30 | raises Not_found -> forall x. not (List.mem (a, x) h.contents) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: Skipping clause: unsupported quantification. +File "hashtbl.mli", line 34, characters 0-197: +34 | val find_opt : ('a, 'b) t -> 'a -> 'b option +35 | (*@ o = find_opt h a +36 | ensures match o with +37 | | None -> not (List.mem a (List.map fst h.contents)) +38 | | Some b -> List.mem (a, b) h.contents *) +Warning: Incomplete computation of the returned value in the specification of find_opt. Failure message won't be able to display the expected returned value. +File "hashtbl.mli", line 40, characters 0-162: +40 | val find_all : ('a, 'b) t -> 'a -> 'b list +41 | (*@ bs = find_all h a +42 | ensures bs = Sequence.filter_map (fun (x, y) -> if x = a then Some y else None) h.contents *) +Warning: Incomplete computation of the returned value in the specification of find_all. Failure message won't be able to display the expected returned value. +File "hashtbl.mli", line 44, characters 0-106: +44 | val mem : ('a, 'b) t -> 'a -> bool +45 | (*@ b = mem h a +46 | ensures b = List.mem a (List.map fst h.contents) *) +Warning: Incomplete computation of the returned value in the specification of mem. Failure message won't be able to display the expected returned value. +File "hashtbl.mli", line 74, characters 0-89: +74 | val length : ('a, 'b) t -> int +75 | (*@ i = length h +76 | ensures i = List.length h.contents *) +Warning: Incomplete computation of the returned value in the specification of length. Failure message won't be able to display the expected returned value. diff --git a/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml b/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml index 31b3a6d8..bfffb7c0 100644 --- a/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml @@ -322,7 +322,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ = then None else Some - ("find", + ((Some (Res (Ortac_runtime.dummy, ()))), "find", [("List.mem (a, b) h.contents", { Ortac_runtime.start = @@ -372,7 +372,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ = then None else Some - ("find", + (None, "find", [("not (List.mem a (List.map fst h.contents))", { Ortac_runtime.start = @@ -435,7 +435,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ = then None else Some - ("find_opt", + ((Some (Res (Ortac_runtime.dummy, ()))), "find_opt", [("match o with\n | None -> not (List.mem a (List.map fst h.contents))\n | Some b -> List.mem (a, b) h.contents", { Ortac_runtime.start = @@ -485,7 +485,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ = then None else Some - ("find_all", + ((Some (Res (Ortac_runtime.dummy, ()))), "find_all", [("bs = Sequence.filter_map (fun (x, y) -> if x = a then Some y else None) h.contents", { Ortac_runtime.start = @@ -535,7 +535,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ = then None else Some - ("mem", + ((Some (Res (Ortac_runtime.dummy, ()))), "mem", [("b = List.mem a (List.map fst h.contents)", { Ortac_runtime.start = @@ -585,7 +585,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ = then None else Some - ("length", + ((Some (Res (Ortac_runtime.dummy, ()))), "length", [("i = List.length h.contents", { Ortac_runtime.start = diff --git a/plugins/qcheck-stm/test/invariants_stm_tests.expected.ml b/plugins/qcheck-stm/test/invariants_stm_tests.expected.ml index d55ab075..cdd134c1 100644 --- a/plugins/qcheck-stm/test/invariants_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/invariants_stm_tests.expected.ml @@ -148,7 +148,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ = then None else Some - ("push", + ((Some (Res (unit, ()))), "push", [("List.length x.contents > 0", { Ortac_runtime.start = diff --git a/plugins/qcheck-stm/test/record_errors.expected b/plugins/qcheck-stm/test/record_errors.expected index 2ca04f5c..6f13fc75 100644 --- a/plugins/qcheck-stm/test/record_errors.expected +++ b/plugins/qcheck-stm/test/record_errors.expected @@ -6,6 +6,15 @@ File "record.mli", line 15, characters 12-22: 15 | val plus2 : int -> int ^^^^^^^^^^ Warning: Skipping plus2: functions with no SUT argument cannot be tested. +File "record.mli", line 20, characters 0-144: +20 | val get : t -> int +21 | (*@ i = get r +22 | pure +23 | ensures i = r.value +24 | ensures i = r.c +25 | ensures plus1 i = i + 1 +26 | ensures plus2 i = i + 2 *) +Warning: Incomplete computation of the returned value in the specification of get. Failure message won't be able to display the expected returned value. File "record.mli", line 24, characters 16-19: 24 | ensures i = r.c ^^^ diff --git a/plugins/qcheck-stm/test/record_stm_tests.expected.ml b/plugins/qcheck-stm/test/record_stm_tests.expected.ml index 836e4388..b493fadc 100644 --- a/plugins/qcheck-stm/test/record_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/record_stm_tests.expected.ml @@ -116,7 +116,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ = then None else Some - ("get", + ((Some (Res (Ortac_runtime.dummy, ()))), "get", [("i = r.value", { Ortac_runtime.start = @@ -165,7 +165,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ = then None else Some - ("get", + ((Some (Res (Ortac_runtime.dummy, ()))), "get", [("plus1 i = i + 1", { Ortac_runtime.start = @@ -215,7 +215,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ = then None else Some - ("get", + ((Some (Res (Ortac_runtime.dummy, ()))), "get", [("plus2 i = i + 2", { Ortac_runtime.start = diff --git a/plugins/qcheck-stm/test/ref_errors.expected b/plugins/qcheck-stm/test/ref_errors.expected index 4dc8c349..b11e35f5 100644 --- a/plugins/qcheck-stm/test/ref_errors.expected +++ b/plugins/qcheck-stm/test/ref_errors.expected @@ -1,3 +1,10 @@ +File "ref.mli", line 8, characters 0-96: + 8 | val get : t -> int + 9 | (*@ i = get r +10 | pure +11 | ensures i = r.value +12 | ensures i + 1 = succ !r *) +Warning: Incomplete computation of the returned value in the specification of get. Failure message won't be able to display the expected returned value. File "ref.mli", line 12, characters 26-27: 12 | ensures i + 1 = succ !r *) ^ diff --git a/plugins/qcheck-stm/test/ref_stm_tests.expected.ml b/plugins/qcheck-stm/test/ref_stm_tests.expected.ml index 0b65aa4f..a9fed368 100644 --- a/plugins/qcheck-stm/test/ref_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/ref_stm_tests.expected.ml @@ -87,7 +87,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ = then None else Some - ("get", + ((Some (Res (Ortac_runtime.dummy, ()))), "get", [("i = r.value", { Ortac_runtime.start = diff --git a/plugins/qcheck-stm/test/sequence_model_errors.expected b/plugins/qcheck-stm/test/sequence_model_errors.expected index e69de29b..643f43a9 100644 --- a/plugins/qcheck-stm/test/sequence_model_errors.expected +++ b/plugins/qcheck-stm/test/sequence_model_errors.expected @@ -0,0 +1,16 @@ +File "sequence_model.mli", line 17, characters 0-253: +17 | val remove : 'a t -> 'a option +18 | (*@ o = remove t +19 | modifies t.contents +20 | ensures t.contents = match Sequence.length (old t.contents) with +21 | | 0 -> Sequence.empty +22 | | _ -> Sequence.tl (old t.contents) *) +Warning: Incomplete computation of the returned value in the specification of remove. Failure message won't be able to display the expected returned value. +File "sequence_model.mli", line 24, characters 0-255: +24 | val remove_ : 'a t -> 'a option +25 | (*@ o = remove_ t +26 | modifies t.contents +27 | ensures t.contents = match length_opt (old t.contents) with +28 | | Some 0 -> Sequence.empty +29 | | _ -> Sequence.tl (old t.contents) *) +Warning: Incomplete computation of the returned value in the specification of remove_. Failure message won't be able to display the expected returned value.