From 634d36594946e9e667d01c07b1d393af8bc80675 Mon Sep 17 00:00:00 2001 From: zoep Date: Mon, 23 Sep 2024 16:32:04 +0300 Subject: [PATCH] Update tests --- tests/hevm/pass/cast-2/cast.act | 8 ++++++-- tests/hevm/pass/cast-3/cast-3.act | 5 ++++- tests/hevm/pass/cast/cast.act | 10 +++++++--- 3 files changed, 17 insertions(+), 6 deletions(-) diff --git a/tests/hevm/pass/cast-2/cast.act b/tests/hevm/pass/cast-2/cast.act index 7d8ce641..67b8515c 100644 --- a/tests/hevm/pass/cast-2/cast.act +++ b/tests/hevm/pass/cast-2/cast.act @@ -63,13 +63,17 @@ storage constructor of B interface constructor(address x, address y) +pointers + x |-> A + y |-> A + iff CALLVALUE == 0 x =/= y creates - A a1 := x as A - A a2 := y as A + A a1 := x + A a2 := y behaviour upd of B diff --git a/tests/hevm/pass/cast-3/cast-3.act b/tests/hevm/pass/cast-3/cast-3.act index d39a0edf..ff1e072d 100644 --- a/tests/hevm/pass/cast-3/cast-3.act +++ b/tests/hevm/pass/cast-3/cast-3.act @@ -43,6 +43,9 @@ case CALLER == to: constructor of TransferOneToken interface constructor(address _tokenAddress) +pointers + _tokenAddress |-> Token + iff CALLVALUE == 0 @@ -50,7 +53,7 @@ iff creates - Token token := _tokenAddress as Token + Token token := _tokenAddress behaviour transfer of TransferOneToken interface transfer() diff --git a/tests/hevm/pass/cast/cast.act b/tests/hevm/pass/cast/cast.act index 3767b9c6..20c20620 100644 --- a/tests/hevm/pass/cast/cast.act +++ b/tests/hevm/pass/cast/cast.act @@ -32,13 +32,17 @@ storage constructor of B interface constructor(address x, address y) +pointers + x |-> A + y |-> A + iff CALLVALUE == 0 x =/= y creates - A a := x as A - B b := y as A + A a1 := x + A a2 := y behaviour upd of B @@ -50,4 +54,4 @@ iff storage a1.x => 42 - a2.x => 11 + a2.x => 11 \ No newline at end of file