summaryrefslogtreecommitdiff
path: root/Test/test2/FreeCall.bpl
diff options
context:
space:
mode:
authorGravatar Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>2013-02-23 12:07:20 -0800
committerGravatar Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>2013-02-23 12:07:20 -0800
commitc5c2c9465a53e4b35a20ad5efe73882dc6a5af34 (patch)
tree9336173498839860956d21178bbf622d1bc22e77 /Test/test2/FreeCall.bpl
parentc7f74de7fae661883ca13bb09d557272de659e03 (diff)
removed call forall and * args to calls
Diffstat (limited to 'Test/test2/FreeCall.bpl')
-rw-r--r--Test/test2/FreeCall.bpl14
1 files changed, 0 insertions, 14 deletions
diff --git a/Test/test2/FreeCall.bpl b/Test/test2/FreeCall.bpl
index 06eb737e..a873a4e6 100644
--- a/Test/test2/FreeCall.bpl
+++ b/Test/test2/FreeCall.bpl
@@ -80,17 +80,3 @@ procedure FreeCall4()
free call b := UncallableReturn(-1);
}
-procedure NormalCall5()
-{
- call forall TestCallForall(*);
- assert T(true);
- assert T(false); // error
-}
-
-procedure FreeCall5()
-{
- free call forall TestCallForall(*);
- assert T(true);
- assert T(false);
- assert false;
-}