Skip to content

Commit

Permalink
Make ortac_postcond also return the computed returned value
Browse files Browse the repository at this point in the history 
Also adapt the runtime so that the commit build.
When a returned value can't be computed based on the information
contained in the Gospel specification, a warning is displayed to the
user at generation and a dummy one is placed to inform the message
printer that the expected returned value is unknown.
  • Loading branch information
@n-osborne
n-osborne committed Feb 21, 2024
1 parent 5e69050 commit 1057ca9
Show file tree
Hide file tree
Showing 18 changed files with 340 additions and 95 deletions.
16 changes: 8 additions & 8 deletions examples/lwt_dllist_tests.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -335,7 +335,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
then None
else
Some
("is_empty",
((Some (Res (Ortac_runtime.dummy, ()))), "is_empty",
[("b <-> s.contents = Sequence.empty",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -383,7 +383,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
then None
else
Some
("length",
((Some (Res (Ortac_runtime.dummy, ()))), "length",
[("l = Sequence.length s.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -440,7 +440,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
then None
else
Some
("take_l",
((Some (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 @@ -492,7 +492,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
then None
else
Some
("take_l",
(None, "take_l",
[("old s.contents = Sequence.empty = s.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -552,7 +552,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
then None
else
Some
("take_r",
((Some (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 @@ -604,7 +604,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
then None
else
Some
("take_r",
(None, "take_r",
[("old s.contents = Sequence.empty = s.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -656,7 +656,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
then None
else
Some
("take_opt_l",
((Some (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 @@ -707,7 +707,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
then None
else
Some
("take_opt_r",
((Some (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
42 changes: 21 additions & 21 deletions examples/varray_circular_tests.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -759,7 +759,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("pop_back",
((Some (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 @@ -811,7 +811,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("pop_back",
(None, "pop_back",
[("t.contents = old t.contents = Sequence.empty",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -868,7 +868,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("pop_front",
((Some (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 @@ -920,7 +920,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("pop_front",
(None, "pop_front",
[("t.contents = old t.contents = Sequence.empty",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -976,7 +976,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("insert_at",
(None, "insert_at",
[("0 <= i <= Sequence.length t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1038,7 +1038,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("insert_at",
(None, "insert_at",
[("0 <= i <= Sequence.length t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1086,7 +1086,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("pop_at",
(None, "pop_at",
[("inside i t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1140,7 +1140,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("pop_at",
((Some (Res (Ortac_runtime.dummy, ()))), "pop_at",
[("(proj x) = old t.contents[i]",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1195,7 +1195,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("pop_at",
(None, "pop_at",
[("inside i t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1243,7 +1243,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("delete_at",
(None, "delete_at",
[("inside i t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1300,7 +1300,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("delete_at",
((Some (Res (unit, ()))), "delete_at",
[("Sequence.length t.contents = Sequence.length (old t.contents) - 1",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1355,7 +1355,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("delete_at",
(None, "delete_at",
[("inside i t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1403,7 +1403,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("get",
(None, "get",
[("inside i t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1457,7 +1457,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("get",
((Some (Res (Ortac_runtime.dummy, ()))), "get",
[("(proj x) = t.contents[i]",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1512,7 +1512,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("get",
(None, "get",
[("inside i t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1560,7 +1560,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("set",
(None, "set",
[("inside i t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1616,7 +1616,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("set",
(None, "set",
[("inside i t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1664,7 +1664,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("length",
((Some (Res (Ortac_runtime.dummy, ()))), "length",
[("l = Sequence.length t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1712,7 +1712,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("is_empty",
((Some (Res (Ortac_runtime.dummy, ()))), "is_empty",
[("b <-> t.contents = Sequence.empty",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1775,7 +1775,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("fill",
(None, "fill",
[("0 <= pos /\\ 0 <= len /\\ pos + len < Sequence.length t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1847,7 +1847,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("fill",
(None, "fill",
[("0 <= pos /\\ 0 <= len /\\ pos + len < Sequence.length t.contents",
{
Ortac_runtime.start =
Expand Down
Loading

0 comments on commit 1057ca9

Please sign in to comment.