Skip to content

Commit

Permalink
Add an assert for exceptional behaviour in scenario
Browse files Browse the repository at this point in the history 
Collect the name of the exception when checking an exceptional
postcondition (not the arguments as they are not always specified).
  • Loading branch information
@n-osborne
n-osborne committed Mar 18, 2024
1 parent 4a9a6c7 commit 172647e
Show file tree
Hide file tree
Showing 12 changed files with 154 additions and 117 deletions.
3 changes: 2 additions & 1 deletion CHANGES.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,8 @@

- Improve test-failure message
[\#202](https://github.com/ocaml-gospel/ortac/pull/202) and
[\#204](https://github.com/ocaml-gospel/ortac/pull/204)
[\#204](https://github.com/ocaml-gospel/ortac/pull/204) and
[\#206](https://github.com/ocaml-gospel/ortac/pull/206)
- Add a comment warning that the file is generated
[\#198](https://github.com/ocaml-gospel/ortac/pull/198)
- Add support for type invariants
Expand Down
20 changes: 10 additions & 10 deletions examples/lwt_dllist_tests.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -337,7 +337,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
else
Some
(Ortac_runtime.report "Lwt_dllist_spec" "create ()"
(Some (Res (Ortac_runtime.dummy, ()))) "is_empty"
(Either.right (Res (Ortac_runtime.dummy, ()))) "is_empty"
[("b <-> s.contents = Sequence.empty",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -386,7 +386,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
else
Some
(Ortac_runtime.report "Lwt_dllist_spec" "create ()"
(Some (Res (Ortac_runtime.dummy, ()))) "length"
(Either.right (Res (Ortac_runtime.dummy, ()))) "length"
[("l = Sequence.length s.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -444,7 +444,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
else
Some
(Ortac_runtime.report "Lwt_dllist_spec" "create ()"
(Some (Res (Ortac_runtime.dummy, ()))) "take_l"
(Either.right (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 =
Expand Down Expand Up @@ -496,8 +496,8 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
then None
else
Some
(Ortac_runtime.report "Lwt_dllist_spec" "create ()" None
"take_l"
(Ortac_runtime.report "Lwt_dllist_spec" "create ()"
(Either.left "Empty") "take_l"
[("old s.contents = Sequence.empty = s.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -558,7 +558,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
else
Some
(Ortac_runtime.report "Lwt_dllist_spec" "create ()"
(Some (Res (Ortac_runtime.dummy, ()))) "take_r"
(Either.right (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 =
Expand Down Expand Up @@ -610,8 +610,8 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
then None
else
Some
(Ortac_runtime.report "Lwt_dllist_spec" "create ()" None
"take_r"
(Ortac_runtime.report "Lwt_dllist_spec" "create ()"
(Either.left "Empty") "take_r"
[("old s.contents = Sequence.empty = s.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -664,7 +664,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
else
Some
(Ortac_runtime.report "Lwt_dllist_spec" "create ()"
(Some (Res (Ortac_runtime.dummy, ()))) "take_opt_l"
(Either.right (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 =
Expand Down Expand Up @@ -716,7 +716,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
else
Some
(Ortac_runtime.report "Lwt_dllist_spec" "create ()"
(Some (Res (Ortac_runtime.dummy, ()))) "take_opt_r"
(Either.right (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 =
Expand Down
56 changes: 35 additions & 21 deletions examples/varray_circular_tests.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -763,7 +763,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
else
Some
(Ortac_runtime.report "Varray_circular_spec" "make 42 'a'"
(Some (Res (Ortac_runtime.dummy, ()))) "pop_back"
(Either.right (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 =
Expand Down Expand Up @@ -816,7 +817,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
else
Some
(Ortac_runtime.report "Varray_circular_spec" "make 42 'a'"
None "pop_back"
(Either.left "Not_found") "pop_back"
[("t.contents = old t.contents = Sequence.empty",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -874,7 +875,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
else
Some
(Ortac_runtime.report "Varray_circular_spec" "make 42 'a'"
(Some (Res (Ortac_runtime.dummy, ()))) "pop_front"
(Either.right (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 =
Expand Down Expand Up @@ -927,7 +929,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
else
Some
(Ortac_runtime.report "Varray_circular_spec" "make 42 'a'"
None "pop_front"
(Either.left "Not_found") "pop_front"
[("t.contents = old t.contents = Sequence.empty",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -984,7 +986,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
else
Some
(Ortac_runtime.report "Varray_circular_spec"
"make 42 'a'" None "insert_at"
"make 42 'a'" (Either.left "Invalid_argument")
"insert_at"
[("0 <= i <= Sequence.length t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1047,7 +1050,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
else
Some
(Ortac_runtime.report "Varray_circular_spec"
"make 42 'a'" None "insert_at"
"make 42 'a'" (Either.left "Invalid_argument")
"insert_at"
[("0 <= i <= Sequence.length t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1096,7 +1100,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
else
Some
(Ortac_runtime.report "Varray_circular_spec"
"make 42 'a'" None "pop_at"
"make 42 'a'" (Either.left "Invalid_argument")
"pop_at"
[("inside i t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1152,7 +1157,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
Some
(Ortac_runtime.report "Varray_circular_spec"
"make 42 'a'"
(Some (Res (Ortac_runtime.dummy, ()))) "pop_at"
(Either.right (Res (Ortac_runtime.dummy, ())))
"pop_at"
[("(proj x) = old t.contents[i]",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1208,7 +1214,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
else
Some
(Ortac_runtime.report "Varray_circular_spec"
"make 42 'a'" None "pop_at"
"make 42 'a'" (Either.left "Invalid_argument")
"pop_at"
[("inside i t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1257,7 +1264,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
else
Some
(Ortac_runtime.report "Varray_circular_spec"
"make 42 'a'" None "delete_at"
"make 42 'a'" (Either.left "Invalid_argument")
"delete_at"
[("inside i t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1315,7 +1323,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
else
Some
(Ortac_runtime.report "Varray_circular_spec"
"make 42 'a'" (Some (Res (unit, ()))) "delete_at"
"make 42 'a'" (Either.right (Res (unit, ())))
"delete_at"
[("Sequence.length t.contents = Sequence.length (old t.contents) - 1",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1371,7 +1380,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
else
Some
(Ortac_runtime.report "Varray_circular_spec"
"make 42 'a'" None "delete_at"
"make 42 'a'" (Either.left "Invalid_argument")
"delete_at"
[("inside i t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1420,7 +1430,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
else
Some
(Ortac_runtime.report "Varray_circular_spec"
"make 42 'a'" None "get"
"make 42 'a'" (Either.left "Invalid_argument") "get"
[("inside i t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1476,7 +1486,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
Some
(Ortac_runtime.report "Varray_circular_spec"
"make 42 'a'"
(Some (Res (Ortac_runtime.dummy, ()))) "get"
(Either.right (Res (Ortac_runtime.dummy, ())))
"get"
[("(proj x) = t.contents[i]",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1532,7 +1543,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
else
Some
(Ortac_runtime.report "Varray_circular_spec"
"make 42 'a'" None "get"
"make 42 'a'" (Either.left "Invalid_argument")
"get"
[("inside i t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1581,7 +1593,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
else
Some
(Ortac_runtime.report "Varray_circular_spec"
"make 42 'a'" None "set"
"make 42 'a'" (Either.left "Invalid_argument") "set"
[("inside i t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1638,7 +1650,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
else
Some
(Ortac_runtime.report "Varray_circular_spec"
"make 42 'a'" None "set"
"make 42 'a'" (Either.left "Invalid_argument")
"set"
[("inside i t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1687,7 +1700,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
else
Some
(Ortac_runtime.report "Varray_circular_spec" "make 42 'a'"
(Some (Res (Ortac_runtime.dummy, ()))) "length"
(Either.right (Res (Ortac_runtime.dummy, ()))) "length"
[("l = Sequence.length t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1736,7 +1749,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
else
Some
(Ortac_runtime.report "Varray_circular_spec" "make 42 'a'"
(Some (Res (Ortac_runtime.dummy, ()))) "is_empty"
(Either.right (Res (Ortac_runtime.dummy, ()))) "is_empty"
[("b <-> t.contents = Sequence.empty",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1800,7 +1813,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
else
Some
(Ortac_runtime.report "Varray_circular_spec"
"make 42 'a'" None "fill"
"make 42 'a'" (Either.left "Invalid_argument") "fill"
[("0 <= pos /\\ 0 <= len /\\ pos + len < Sequence.length t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1873,7 +1886,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
else
Some
(Ortac_runtime.report "Varray_circular_spec"
"make 42 'a'" None "fill"
"make 42 'a'" (Either.left "Invalid_argument")
"fill"
[("0 <= pos /\\ 0 <= len /\\ pos + len < Sequence.length t.contents",
{
Ortac_runtime.start =
Expand Down
Loading

0 comments on commit 172647e

Please sign in to comment.