fixup! motoko-san: add test for arrays + viper lib

serokell · Apr 26, 2024 · 7940973 · 7940973
1 parent dbf0fc1
commit 7940973
Show file tree

Hide file tree

Showing 18 changed files with 17 additions and 17 deletions.
diff --git a/src/viper/trans.ml b/src/viper/trans.ml
@@ -159,7 +159,7 @@ let rec extract_concurrency (seq : seqn) : stmt' list * seqn =
 
 let prelude =
   let (!!) p = !!! Source.no_region p in
-  [ !! (ImportI (!! "lib/array.vpr")) ]
+  [ !! (ImportI (!! "viper_lib/array.vpr")) ]
 
 let rec unit (u : M.comp_unit) : prog Diag.result =
   Diag.(

diff --git a/src/viper/lib/array.vpr → src/viper/viper_lib/array.vpr b/src/viper/lib/array.vpr → src/viper/viper_lib/array.vpr
diff --git a/test/repl/ok/viper.stdout.ok b/test/repl/ok/viper.stdout.ok
@@ -1,4 +1,4 @@
-import "lib/array.vpr"
+import "viper_lib/array.vpr"
 field $message_async: Int
 define $Perm($Self) ((((true && acc(($Self).claimed,write)) && acc(($Self).count,write)) && 
   acc(($Self).$message_async,write)))

diff --git a/test/run.sh b/test/run.sh
@@ -288,7 +288,7 @@ do
   $ECHO -n "$base:"
   [ -d $out ] || mkdir $out
   [ -d $ok ] || mkdir $ok
-  [ -d $out/lib ] ||  ln -s ../../../src/viper/lib/ $out/lib
+  [ -d $out/viper_lib ] ||  ln -s ../../../src/viper/viper_lib/ $out/viper_lib
 
   rm -rf $out/$base $out/$base.*
 

diff --git a/test/viper/ok/array.vpr.ok b/test/viper/ok/array.vpr.ok
@@ -1,4 +1,4 @@
-import "lib/array.vpr"
+import "viper_lib/array.vpr"
 define $Perm($Self) ((((true && (acc(($Self).arr,write) && (array_acc_mut(
                                                             ($Self).arr, int) && (
   size(($Self).arr) == 2)))) && acc(($Self).f,write)) && acc(($Self).count,write)))

diff --git a/test/viper/ok/assertions.vpr.ok b/test/viper/ok/assertions.vpr.ok
@@ -1,4 +1,4 @@
-import "lib/array.vpr"
+import "viper_lib/array.vpr"
 field $message_async: Int
 define $Perm($Self) ((((true && acc(($Self).u,write)) && acc(($Self).v,write)) && 
   acc(($Self).$message_async,write)))

diff --git a/test/viper/ok/async.vpr.ok b/test/viper/ok/async.vpr.ok
@@ -1,4 +1,4 @@
-import "lib/array.vpr"
+import "viper_lib/array.vpr"
 field $message_async_4: Int
 field $message_async_2: Int
 field $message_async: Int

diff --git a/test/viper/ok/claim-broken.vpr.ok b/test/viper/ok/claim-broken.vpr.ok
@@ -1,4 +1,4 @@
-import "lib/array.vpr"
+import "viper_lib/array.vpr"
 field $message_async: Int
 define $Perm($Self) ((((true && acc(($Self).claimed,write)) && acc(($Self).count,write)) && 
   acc(($Self).$message_async,write)))

diff --git a/test/viper/ok/claim-reward-naive.vpr.ok b/test/viper/ok/claim-reward-naive.vpr.ok
@@ -1,4 +1,4 @@
-import "lib/array.vpr"
+import "viper_lib/array.vpr"
 define $Perm($Self) (((true && acc(($Self).claimed,write)) && acc(($Self).count,write)))
 define $Inv($Self) (invariant_5($Self))
 method __init__($Self: Ref)

diff --git a/test/viper/ok/claim-simple.vpr.ok b/test/viper/ok/claim-simple.vpr.ok
@@ -1,4 +1,4 @@
-import "lib/array.vpr"
+import "viper_lib/array.vpr"
 define $Perm($Self) (((true && acc(($Self).claimed,write)) && acc(($Self).count,write)))
 define $Inv($Self) (true)
 method __init__($Self: Ref)

diff --git a/test/viper/ok/claim.vpr.ok b/test/viper/ok/claim.vpr.ok
@@ -1,4 +1,4 @@
-import "lib/array.vpr"
+import "viper_lib/array.vpr"
 field $message_async: Int
 define $Perm($Self) ((((true && acc(($Self).claimed,write)) && acc(($Self).count,write)) && 
   acc(($Self).$message_async,write)))

diff --git a/test/viper/ok/counter.vpr.ok b/test/viper/ok/counter.vpr.ok
@@ -1,4 +1,4 @@
-import "lib/array.vpr"
+import "viper_lib/array.vpr"
 define $Perm($Self) ((true && acc(($Self).count,write)))
 define $Inv($Self) (true)
 method __init__($Self: Ref)

diff --git a/test/viper/ok/invariant.vpr.ok b/test/viper/ok/invariant.vpr.ok
@@ -1,4 +1,4 @@
-import "lib/array.vpr"
+import "viper_lib/array.vpr"
 define $Perm($Self) (((true && acc(($Self).claimed,write)) && acc(($Self).count,write)))
 define $Inv($Self) (((invariant_9($Self) && invariant_10($Self)) && invariant_11($Self)))
 method __init__($Self: Ref)

diff --git a/test/viper/ok/loop-invariant.vpr.ok b/test/viper/ok/loop-invariant.vpr.ok
@@ -1,4 +1,4 @@
-import "lib/array.vpr"
+import "viper_lib/array.vpr"
 define $Perm($Self) (true)
 define $Inv($Self) (true)
 method __init__($Self: Ref)

diff --git a/test/viper/ok/method-call.vpr.ok b/test/viper/ok/method-call.vpr.ok
@@ -1,4 +1,4 @@
-import "lib/array.vpr"
+import "viper_lib/array.vpr"
 define $Perm($Self) (true)
 define $Inv($Self) (true)
 method __init__($Self: Ref)

diff --git a/test/viper/ok/nats.vpr.ok b/test/viper/ok/nats.vpr.ok
@@ -1,4 +1,4 @@
-import "lib/array.vpr"
+import "viper_lib/array.vpr"
 define $Perm($Self) ((true && acc(($Self).x,write)))
 define $Inv($Self) (true)
 method __init__($Self: Ref)

diff --git a/test/viper/ok/private.vpr.ok b/test/viper/ok/private.vpr.ok
@@ -1,4 +1,4 @@
-import "lib/array.vpr"
+import "viper_lib/array.vpr"
 define $Perm($Self) (((true && acc(($Self).claimed,write)) && acc(($Self).count,write)))
 define $Inv($Self) (invariant_7($Self))
 method __init__($Self: Ref)

diff --git a/test/viper/ok/simple-funs.vpr.ok b/test/viper/ok/simple-funs.vpr.ok
@@ -1,4 +1,4 @@
-import "lib/array.vpr"
+import "viper_lib/array.vpr"
 define $Perm($Self) (true)
 define $Inv($Self) (true)
 method __init__($Self: Ref)