Skip to content

Commit

Permalink
Modify ghost model test
Browse files Browse the repository at this point in the history
Without the previous fix, the model access is ill-translated (without
its tag). Now we can use the same name as the type itself (or any
other already used name).
  • Loading branch information
n-osborne committed Jun 26, 2024
1 parent 55d3624 commit dc02e11
Show file tree
Hide file tree
Showing 2 changed files with 16 additions and 16 deletions.
8 changes: 4 additions & 4 deletions plugins/qcheck-stm/test/ghost_as_model.mli
Original file line number Diff line number Diff line change
@@ -1,13 +1,13 @@
(*@ type m = A of integer *)

type t
(*@ mutable model view : m *)
(*@ mutable model m : m *)

val create : unit -> t
(*@ t = create ()
ensures t.view = A 0 *)
ensures t.m = A 0 *)

val use : t -> unit
(*@ use t
modifies t.view
ensures t.view = match old t.view with A x -> A (succ x) *)
modifies t.m
ensures t.m = match old t.m with A x -> A (succ x) *)
24 changes: 12 additions & 12 deletions plugins/qcheck-stm/test/ghost_as_model_stm_tests.expected.ml
Original file line number Diff line number Diff line change
Expand Up @@ -14,11 +14,11 @@ module Spec =
let show_cmd cmd__001_ =
match cmd__001_ with | Use -> Format.asprintf "%s sut" "use"
type nonrec state = {
view: m }
m_1: m }
let init_state =
let () = () in
{
view =
m_1 =
(try A (Ortac_runtime.Gospelstdlib.integer_of_int 0)
with
| e ->
Expand All @@ -30,15 +30,15 @@ module Spec =
{
pos_fname = "ghost_as_model.mli";
pos_lnum = 8;
pos_bol = 349;
pos_cnum = 370
pos_bol = 343;
pos_cnum = 361
};
Ortac_runtime.stop =
{
pos_fname = "ghost_as_model.mli";
pos_lnum = 8;
pos_bol = 349;
pos_cnum = 371
pos_bol = 343;
pos_cnum = 362
}
})))
}
Expand All @@ -51,9 +51,9 @@ module Spec =
match cmd__002_ with
| Use ->
{
view =
m_1 =
((try
match state__003_.view with
match state__003_.m_1 with
| A x -> A (Ortac_runtime.Gospelstdlib.succ x)
with
| e ->
Expand All @@ -65,15 +65,15 @@ module Spec =
{
pos_fname = "ghost_as_model.mli";
pos_lnum = 13;
pos_bol = 517;
pos_cnum = 538
pos_bol = 502;
pos_cnum = 520
};
Ortac_runtime.stop =
{
pos_fname = "ghost_as_model.mli";
pos_lnum = 13;
pos_bol = 517;
pos_cnum = 577
pos_bol = 502;
pos_cnum = 556
}
}))))
}
Expand Down

0 comments on commit dc02e11

Please sign in to comment.