diff options
author | 2010-02-18 19:58:38 +0000 | |
---|---|---|
committer | 2010-02-18 19:58:38 +0000 | |
commit | 2e03ed114503dfa16547c06766fa683c690f9052 (patch) | |
tree | 7151121512b0e5476caca502bd7e04d0d0701bd9 /Source/VCExpr/VCExprAST.ssc | |
parent | 36bda629c0083590c5e4d17f06e769f822617033 (diff) |
Implement if-then-else expression.
Diffstat (limited to 'Source/VCExpr/VCExprAST.ssc')
-rw-r--r-- | Source/VCExpr/VCExprAST.ssc | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/Source/VCExpr/VCExprAST.ssc b/Source/VCExpr/VCExprAST.ssc index 5a9063cc..e08e6138 100644 --- a/Source/VCExpr/VCExprAST.ssc +++ b/Source/VCExpr/VCExprAST.ssc @@ -221,6 +221,7 @@ namespace Microsoft.Boogie // ternary version of the subtype operator, the first argument of which gives
// the type of the compared terms
public static readonly VCExprOp! Subtype3Op = new VCExprNAryOp (3, Type.Bool);
+ public static readonly VCExprOp! IfThenElseOp = new VCExprIfThenElseOp();
public VCExprOp! BoogieFunctionOp(Function! func) {
return new VCExprBoogieFunctionOp(func);
@@ -990,6 +991,34 @@ namespace Microsoft.Boogie.VCExprAST }
}
+ public class VCExprIfThenElseOp : VCExprOp {
+ public override int Arity { get { return 3; } }
+ public override int TypeParamArity { get { return 0; } }
+ public override Type! InferType(List<VCExpr!>! args, List<Type!>! typeArgs) {
+ return args[1].Type;
+ }
+
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object that) {
+ if (Object.ReferenceEquals(this, that))
+ return true;
+ if (that is VCExprIfThenElseOp)
+ return true;
+ return false;
+ }
+ [Pure]
+ public override int GetHashCode() {
+ return 1;
+ }
+
+ internal VCExprIfThenElseOp() {
+ }
+ public override Result Accept<Result, Arg>
+ (VCExprNAry! expr, IVCExprOpVisitor<Result, Arg>! visitor, Arg arg) {
+ return visitor.VisitIfThenElseOp(expr, arg);
+ }
+ }
+
/////////////////////////////////////////////////////////////////////////////////
// Bitvector operators
|