From bb5b4a6483d8b0b6a5765e677ad636149cc58030 Mon Sep 17 00:00:00 2001 From: Nicolas Osborne Date: Wed, 24 Jan 2024 16:49:49 +0100 Subject: [PATCH] Read `.gospel` files in `qcheck-stm` plugin This commit also modifies how we handle xpost in the case of exception that doesn't take any argument as it was not working anymore (but I don't know why exactly). --- plugins/qcheck-stm/src/config.ml | 7 ++++++- plugins/qcheck-stm/src/ir_of_gospel.ml | 3 ++- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/plugins/qcheck-stm/src/config.ml b/plugins/qcheck-stm/src/config.ml index 36064d7b..c13ce218 100644 --- a/plugins/qcheck-stm/src/config.ml +++ b/plugins/qcheck-stm/src/config.ml @@ -221,7 +221,12 @@ let init gospel config_module = let open Reserr in try let module_name = Utils.module_name_of_path gospel - and env, sigs = Utils.type_check [] gospel in + and env, sigs = + match Filename.extension gospel with + | ".mli" -> Utils.type_check [] gospel + | ".gospel" -> Utils.read_gospel_file gospel + | _ -> invalid_arg "init" + in assert (List.length env = 1); let namespace = List.hd env in let context = Context.init module_name namespace in diff --git a/plugins/qcheck-stm/src/ir_of_gospel.ml b/plugins/qcheck-stm/src/ir_of_gospel.ml index ef23a296..d56cbc70 100644 --- a/plugins/qcheck-stm/src/ir_of_gospel.ml +++ b/plugins/qcheck-stm/src/ir_of_gospel.ml @@ -212,7 +212,8 @@ let postcond spec = (fun (p, t) -> let open Tterm in match p.p_node with - | Papp (ls, []) when Symbols.(ls_equal ls (fs_tuple 0)) -> + (* When the exception doesn't take any argument, gospel type-checker add a dummy pattern here *) + | Papp (_, []) when Ttypes.(x.xs_type = Exn_tuple []) -> (x, None, Ir.term_val spec t) | _ -> (x, Some p, Ir.term_val spec t)) l)