diff options
| author |  wuestholz <unknown> | 2011-09-14 16:28:25 +0200 |
|---|---|---|
| committer | wuestholz <unknown> | 2011-09-14 16:28:25 +0200 |
| commit | c250f55e7af88a3671262e2c0522664f299ef2f2 (patch) | |
| tree | 26755b6bff316c4d656d70cf69dc6ca6bdfbe589 /Source/Core/BoogiePL.atg | |
| parent | 23a94e0bbd32c8c612cb79a6745b5bee4dd667dd (diff) | |
Added "free call" statements that don't check the precondition in the caller.
Diffstat (limited to 'Source/Core/BoogiePL.atg')
| -rw-r--r-- | Source/Core/BoogiePL.atg | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index b1fbd609..7519fb4c 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -905,7 +905,10 @@ CallCmd<out Cmd/*!*/ c> QKeyValue kv = null;
Expr en; List<Expr> args;
c = dummyCmd;
+ bool isFree = false;
.)
+ [ "free" (. isFree = true; .)
+ ]
"call" (. x = t; .)
{ Attribute<ref kv> }
( Ident<out first>
@@ -914,7 +917,7 @@ CallCmd<out Cmd/*!*/ c> { "," CallForallArg<out en> (. es.Add(en); .)
}
]
- ")" (. c = new CallCmd(x, first.val, es, ids, kv); .)
+ ")" (. c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; .)
|
(. ids.Add(new IdentifierExpr(first, first.val)); .)
[ "," CallOutIdent<out p> (.
@@ -938,7 +941,7 @@ CallCmd<out Cmd/*!*/ c> { "," CallForallArg<out en> (. es.Add(en); .)
}
]
- ")" (. c = new CallCmd(x, first.val, es, ids, kv); .)
+ ")" (. c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; .)
)
| "forall"
Ident<out first> "(" (. args = new List<Expr>(); .)
@@ -946,7 +949,7 @@ CallCmd<out Cmd/*!*/ c> { "," CallForallArg<out en> (. args.Add(en); .)
}
]
- ")" (. c = new CallForallCmd(x, first.val, args, kv); .)
+ ")" (. c = new CallForallCmd(x, first.val, args, kv); ((CallForallCmd) c).IsFree = isFree; .)
| "*"
(. ids.Add(null); .)
[ "," CallOutIdent<out p> (.
@@ -970,7 +973,7 @@ CallCmd<out Cmd/*!*/ c> { "," CallForallArg<out en> (. es.Add(en); .)
}
]
- ")" (. c = new CallCmd(x, first.val, es, ids, kv); .)
+ ")" (. c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; .)
)
.
|