added test for forward_trg_assertions

nyu-acsys · Oct 31, 2024 · 8a6b352 · 8a6b352
1 parent 24e60b3
commit 8a6b352
Show file tree

Hide file tree

Showing 2 changed files with 25 additions and 0 deletions.
diff --git a/test/ci/back-end/forward_trg_assertions.rav b/test/ci/back-end/forward_trg_assertions.rav
@@ -0,0 +1,23 @@
+field f: Int
+
+
+func loc_id(x: Ref) 
+    returns (r: Ref)
+{ x }
+
+func t(x: Ref)
+    returns (r: Bool)
+{ true }
+
+func guard(x: Ref, b: Bool)
+    returns (r: Bool)
+{ true }
+
+proc p() {
+    var b: Bool := true;
+
+    if (b) {
+        inhale forall x: Ref :: { t(x) } guard(x, b) ==> own(loc_id(x), f, 1, 1.0);
+    }
+
+}
diff --git a/test/ci/back-end/forward_trg_assertions.t b/test/ci/back-end/forward_trg_assertions.t
@@ -0,0 +1,2 @@
+  $ dune exec -- raven --shh ./forward_trg_assertions.rav
+  Verification successful.
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		$ dune exec -- raven --shh ./forward_trg_assertions.rav
		Verification successful.