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

@@ -79,7 +79,12 @@ let init path init_sut_txt sut_str =
   let open Reserr in
   try
     let module_name = Utils.module_name_of_path path
-    and env, sigs = Utils.type_check [] path in
+    and env, sigs =
+      match Filename.extension path with
+      | ".mli" -> Utils.type_check [] path
+      | ".gospel" -> Utils.read_gospel_file path
+      | _ -> invalid_arg "init"
+    in
     assert (List.length env = 1);
     let namespace = List.hd env in
     let context = Context.init module_name namespace in

plugins/qcheck-stm/src/ir_of_gospel.ml

@@ -207,7 +207,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)