From 5fb4f45117588850743010bf43bbb8486051d5f8 Mon Sep 17 00:00:00 2001 From: Golovin Pavel Date: Thu, 25 Apr 2024 16:23:05 +0200 Subject: [PATCH] fixup! motoko-san: add test for arrays + viper lib --- test/viper/ok/nats.silicon.ok | 2 +- test/viper/ok/nats.vpr.ok | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/test/viper/ok/nats.silicon.ok b/test/viper/ok/nats.silicon.ok index 1671de8e2f8..da5ef00f4ad 100644 --- a/test/viper/ok/nats.silicon.ok +++ b/test/viper/ok/nats.silicon.ok @@ -1 +1 @@ -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (nats.vpr@2.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (array.vpr@3.1) diff --git a/test/viper/ok/nats.vpr.ok b/test/viper/ok/nats.vpr.ok index 472e810081c..d663adcaa7a 100644 --- a/test/viper/ok/nats.vpr.ok +++ b/test/viper/ok/nats.vpr.ok @@ -1,3 +1,4 @@ +import "lib/array.vpr" define $Perm($Self) ((true && acc(($Self).x,write))) define $Inv($Self) (true) method __init__($Self: Ref)