summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>2013-02-12 11:17:44 -0800
committerGravatar Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>2013-02-12 11:17:44 -0800
commit1ca4bdc8652046f902b50820c1c250148e1abe25 (patch)
tree673a1780664f5a656c53f54203c14efbe39e5c8a /Test
parentbbe5109c4ed1b1d1f48b8208e1bcb4fda0513c59 (diff)
Add another test file
Diffstat (limited to 'Test')
-rw-r--r--Test/og/one.bpl13
1 files changed, 13 insertions, 0 deletions
diff --git a/Test/og/one.bpl b/Test/og/one.bpl
new file mode 100644
index 00000000..bb7b1d01
--- /dev/null
+++ b/Test/og/one.bpl
@@ -0,0 +1,13 @@
+var x:int;
+
+procedure A()
+{
+ x := x;
+}
+
+procedure B()
+{
+ x := 5;
+ assert{:yield} x == 5;
+}
+