Boogie: Added boolean code expressions (sans well-formedness checks on the input).

1 files changed, 18 insertions, 8 deletions

diff --git a/Source/AIFramework/VariableMap/VariableMapLattice.ssc b/Source/AIFramework/VariableMap/VariableMapLattice.ssc
index c0293493..ab030b59 100644
--- a/Source/AIFramework/VariableMap/VariableMapLattice.ssc
+++ b/Source/AIFramework/VariableMap/VariableMapLattice.ssc
@@ -78,7 +78,7 @@ namespace Microsoft.AbstractInterpretationFramework
 

             public bool IsBottom { 

                  get { 

-                   return this.constraints == null;
+                   return this.constraints == null;

                  } 

             }

 

@@ -89,7 +89,7 @@ namespace Microsoft.AbstractInterpretationFramework
                   requires !this.IsBottom;

                 { 

                   assume this.constraints != null;

-                  return (!) this.constraints.Keys;
+                  return (!) this.constraints.Keys;

                 } 

             }

 

@@ -117,7 +117,7 @@ namespace Microsoft.AbstractInterpretationFramework
                 requires !this.IsBottom;

                 { 

                   assume this.constraints != null;

-                  return (Element)constraints[key];
+                  return (Element)constraints[key];

                 } 

             }

 

@@ -303,7 +303,7 @@ namespace Microsoft.AbstractInterpretationFramework
             }

             Elt! join = new Elt(newMap);

         

-            // System.Console.WriteLine("{0} join {1} = {2} ", this.ToString(a), ToString(b), ToString(join));
+            // System.Console.WriteLine("{0} join {1} = {2} ", this.ToString(a), ToString(b), ToString(join));

 

             return join;

         }

@@ -368,9 +368,9 @@ namespace Microsoft.AbstractInterpretationFramework
             }

             Element! widen= new Elt(newMap);

       

-            // System.Console.WriteLine("{0} widen {1} = {2} ", this.ToString(a), ToString(b), ToString(widen));
+            // System.Console.WriteLine("{0} widen {1} = {2} ", this.ToString(a), ToString(b), ToString(widen));

 

-            return widen;
+            return widen;

         }

 

         internal static ISet/*<IVariable!>*/! VariablesInExpression(IExpr! e, ISet/*<IVariable!>*/! ignoreVars)

@@ -400,6 +400,10 @@ namespace Microsoft.AbstractInterpretationFramework
                 // Ignore the bound variable

                 s.AddAll(VariablesInExpression(lambda.Body, (!) Set.Union(ignoreVars, x)));

             }

+            else if (e is IUnknown)

+            {

+                // skip (actually, it would be appropriate to return the universal set of all variables)

+            }

             else

             {

                 Debug.Assert(false, "case not handled: " + e);

@@ -482,7 +486,7 @@ namespace Microsoft.AbstractInterpretationFramework
           else 

           {

             IExpr! left = (IExpr!) fun.Arguments[0];

-            IExpr! right = (IExpr!) fun.Arguments[1];
+            IExpr! right = (IExpr!) fun.Arguments[1];

 

             if(!(left is IVariable || right is IVariable))    // At least one of the two operands must be a variable

               return false;

@@ -493,7 +497,7 @@ namespace Microsoft.AbstractInterpretationFramework
                 || fun.FunctionSymbol.Equals(Int.Mul)

                 || fun.FunctionSymbol.Equals(Int.Div)

                 || fun.FunctionSymbol.Equals(Int.Mod))

-              return IsArithmeticExpr(left) && IsArithmeticExpr(right);
+              return IsArithmeticExpr(left) && IsArithmeticExpr(right);

             else 

               return false;

           } 

@@ -592,6 +596,12 @@ namespace Microsoft.AbstractInterpretationFramework
                        );

             }

 

+            // else

+            

+            if (expr is IUnknown) {

+              return expr;

+            }

+

             else

             {

                 throw