summaryrefslogtreecommitdiff
path: root/Test/test0/EmptyCallArgs.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/test0/EmptyCallArgs.bpl
parentc7f74de7fae661883ca13bb09d557272de659e03 (diff)
removed call forall and * args to calls
Diffstat (limited to 'Test/test0/EmptyCallArgs.bpl')
-rw-r--r--Test/test0/EmptyCallArgs.bpl13
1 files changed, 0 insertions, 13 deletions
diff --git a/Test/test0/EmptyCallArgs.bpl b/Test/test0/EmptyCallArgs.bpl
index eb1c43b7..d45633e9 100644
--- a/Test/test0/EmptyCallArgs.bpl
+++ b/Test/test0/EmptyCallArgs.bpl
@@ -9,13 +9,6 @@ procedure CallP() {
var z:C;
call z := P(x, y);
- call * := P(x, y);
- call z := P(*, y);
- call z := P(x, *);
- call * := P(*, y);
- call * := P(x, *);
- call z := P(*, *);
- call * := P(*, *);
}
procedure CallQ() {
@@ -24,10 +17,4 @@ procedure CallQ() {
var z:bool;
call z := Q(x, y);
- call * := Q(x, y);
- call z := Q(*, y);
- call z := Q(x, *);
- call * := Q(*, y);
- call * := Q(x, *); // problem: type parameter cannot be inferred
- call * := Q(*, *); // problem: type parameter cannot be inferred
} \ No newline at end of file