Skip to content

Commit b19bf3e

Browse files
Update LiftImperativeCallsInAssertTest expected outputs for new block formatting
1 parent e22ef71 commit b19bf3e

1 file changed

Lines changed: 33 additions & 7 deletions

File tree

StrataTest/Languages/Laurel/LiftImperativeCallsInAssertTest.lean

Lines changed: 33 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -42,9 +42,17 @@ private def printLifted (input : String) : IO Unit := do
4242

4343
/--
4444
info: procedure impure(): int
45-
{ var x: int := 0; x := x + 1; x };
45+
{
46+
var x: int := 0;
47+
x := x + 1;
48+
x
49+
};
4650
procedure test()
47-
{ var $c_0: int; $c_0 := impure(); assert $c_0 == 1 };
51+
{
52+
var $c_0: int;
53+
$c_0 := impure();
54+
assert $c_0 == 1
55+
};
4856
-/
4957
#guard_msgs in
5058
#eval! printLifted r"
@@ -62,7 +70,10 @@ procedure test() {
6270

6371
/--
6472
info: procedure test()
65-
{ var x: int := 0; assert (x := 2) == 2 };
73+
{
74+
var x: int := 0;
75+
assert (x := 2) == 2
76+
};
6677
-/
6778
#guard_msgs in
6879
#eval! printLifted r"
@@ -76,9 +87,17 @@ procedure test() {
7687

7788
/--
7889
info: procedure impure(): int
79-
{ var x: int := 0; x := x + 1; x };
90+
{
91+
var x: int := 0;
92+
x := x + 1;
93+
x
94+
};
8095
procedure test()
81-
{ var $c_0: int; $c_0 := impure(); assume $c_0 == 1 };
96+
{
97+
var $c_0: int;
98+
$c_0 := impure();
99+
assume $c_0 == 1
100+
};
82101
-/
83102
#guard_msgs in
84103
#eval! printLifted r"
@@ -99,9 +118,16 @@ procedure test() {
99118
/--
100119
info: procedure multi_out(x: int)
101120
returns (r: int, extra: int)
102-
{ r := x + 1; extra := x + 2 };
121+
{
122+
r := x + 1;
123+
extra := x + 2
124+
};
103125
procedure test()
104-
{ var $c_0: BUG_MultiValuedExpr; $c_0 := multi_out(5); assert $c_0 == 6 };
126+
{
127+
var $c_0: BUG_MultiValuedExpr;
128+
$c_0 := multi_out(5);
129+
assert $c_0 == 6
130+
};
105131
-/
106132
#guard_msgs in
107133
#eval! printLifted r"

0 commit comments

Comments
 (0)