Fix false contract assumption encountered on System.Decimal.op_Explicit

microsoft · Aug 11, 2015 · b05a9b4 · b05a9b4
1 parent 0fbc6e0
commit b05a9b4
Showing 1 changed file with 23 additions and 1 deletion.
diff --git a/Microsoft.Research/ControlFlow/ControlFlow.cs b/Microsoft.Research/ControlFlow/ControlFlow.cs
@@ -8320,33 +8320,55 @@ public Result Call<TypeList, ArgList>(APC pc, Method method, bool tail, bool vir
             // special case Decimal methods to operators
             if (mdDecoder.Equal(declaringType, mdDecoder.System_Decimal))
             {
-                Contract.Assume(args.Count >= 2);
                 switch (mdDecoder.Name(method))
                 {
                     case "op_Addition":
+                        Contract.Assume(args.Count >= 2);
                         return visitor.Binary(pc, BinaryOperator.Add, dest, args[0], args[1], data);
+
                     case "op_Division":
+                        Contract.Assume(args.Count >= 2);
                         return visitor.Binary(pc, BinaryOperator.Div, dest, args[0], args[1], data);
+
                     case "op_Equality":
+                        Contract.Assume(args.Count >= 2);
                         return visitor.Binary(pc, BinaryOperator.Ceq, dest, args[0], args[1], data);
+
                     case "op_GreaterThan":
+                        Contract.Assume(args.Count >= 2);
                         return visitor.Binary(pc, BinaryOperator.Cgt, dest, args[0], args[1], data);
+
                     case "op_GreaterThanOrEqual":
+                        Contract.Assume(args.Count >= 2);
                         return visitor.Binary(pc, BinaryOperator.Cge, dest, args[0], args[1], data);
+
                     case "op_Inequality":
+                        Contract.Assume(args.Count >= 2);
                         return visitor.Binary(pc, BinaryOperator.Cne_Un, dest, args[0], args[1], data);
+
                     case "op_LessThan":
+                        Contract.Assume(args.Count >= 2);
                         return visitor.Binary(pc, BinaryOperator.Clt, dest, args[0], args[1], data);
+
                     case "op_LessThanOrEqual":
+                        Contract.Assume(args.Count >= 2);
                         return visitor.Binary(pc, BinaryOperator.Cle, dest, args[0], args[1], data);
+
                     case "op_Modulus":
+                        Contract.Assume(args.Count >= 2);
                         return visitor.Binary(pc, BinaryOperator.Rem, dest, args[0], args[1], data);
+
                     case "op_Multiply":
+                        Contract.Assume(args.Count >= 2);
                         return visitor.Binary(pc, BinaryOperator.Mul, dest, args[0], args[1], data);
+
                     case "op_Subtraction":
+                        Contract.Assume(args.Count >= 2);
                         return visitor.Binary(pc, BinaryOperator.Sub, dest, args[0], args[1], data);
+
                     case "op_UnaryNegation":
                         return visitor.Unary(pc, UnaryOperator.Neg, false, false, dest, args[0], data);
+
                     default:
                         break;
                 }