diff --git a/test/ci/back-end/forward_trg_assertions.rav b/test/ci/back-end/forward_trg_assertions.rav new file mode 100644 index 0000000..05a5a57 --- /dev/null +++ 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); + } + +} \ No newline at end of file diff --git a/test/ci/back-end/forward_trg_assertions.t b/test/ci/back-end/forward_trg_assertions.t new file mode 100644 index 0000000..c2ffa0e --- /dev/null +++ b/test/ci/back-end/forward_trg_assertions.t @@ -0,0 +1,2 @@ + $ dune exec -- raven --shh ./forward_trg_assertions.rav + Verification successful.