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 Feb 27, 2024
1 parent 1d36870 commit fe6aaa3
Show file tree
Hide file tree
Showing 11 changed files with 164 additions and 123 deletions.
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 @@ -338,7 +338,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 @@ -387,7 +387,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 @@ -445,7 +445,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 @@ -497,8 +497,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 @@ -559,7 +559,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 @@ -611,8 +611,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 @@ -665,7 +665,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 @@ -717,7 +717,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 @@ -766,7 +766,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 @@ -819,7 +820,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 @@ -877,7 +878,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 @@ -930,7 +932,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 @@ -987,7 +989,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 @@ -1050,7 +1053,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 @@ -1099,7 +1103,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 @@ -1155,7 +1160,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 @@ -1211,7 +1217,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 @@ -1260,7 +1267,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 @@ -1318,7 +1326,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 @@ -1374,7 +1383,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 @@ -1423,7 +1433,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 @@ -1479,7 +1489,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 @@ -1535,7 +1546,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 @@ -1584,7 +1596,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 @@ -1641,7 +1653,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 @@ -1690,7 +1703,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 @@ -1739,7 +1752,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 @@ -1803,7 +1816,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 @@ -1876,7 +1889,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 fe6aaa3

Please sign in to comment.