diff options
| author |  MichalMoskal <unknown> | 2010-02-18 19:58:38 +0000 |
|---|---|---|
| committer | MichalMoskal <unknown> | 2010-02-18 19:58:38 +0000 |
| commit | 2e03ed114503dfa16547c06766fa683c690f9052 (patch) | |
| tree | 7151121512b0e5476caca502bd7e04d0d0701bd9 /Source/VCExpr/Boogie2VCExpr.ssc | |
| parent | 36bda629c0083590c5e4d17f06e769f822617033 (diff) | |
Implement if-then-else expression.
Diffstat (limited to 'Source/VCExpr/Boogie2VCExpr.ssc')
| -rw-r--r-- | Source/VCExpr/Boogie2VCExpr.ssc | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/Source/VCExpr/Boogie2VCExpr.ssc b/Source/VCExpr/Boogie2VCExpr.ssc index f6393679..4698f541 100644 --- a/Source/VCExpr/Boogie2VCExpr.ssc +++ b/Source/VCExpr/Boogie2VCExpr.ssc @@ -738,6 +738,10 @@ namespace Microsoft.Boogie.VCExprAST return this.args[0];
}
+ public VCExpr! Visit(IfThenElse! ite) {
+ return Gen.Function(VCExpressionGenerator.IfThenElseOp, this.args);
+ }
+
///////////////////////////////////////////////////////////////////////////////
private VCExpr! TranslateBinaryOperator(BinaryOperator! app, List<VCExpr!>! args) {
|