Bugfix

pyState/BinOp.py

@@ -38,7 +38,6 @@ def _handleNum(state,left,right,op):
         ret = leftZ3Object / rightZ3Object
 
     elif type(op) == ast.Mod:
-        print(type(leftZ3Object),type(rightZ3Object))
         ret = leftZ3Object % rightZ3Object
 
     elif type(op) == ast.BitXor:

pyState/Return.py

@@ -31,15 +31,19 @@ def handle(state,element):
     if len(retObjs) > 0:
         return retObjs
 
+    # Asserting 1 thing to return for now
+    assert len(ret) == 1
+    obj = ret[0]
 
-    # Good to go, pop back down
-    state.popCallStack()
+    state = obj.state if obj is not None else state
+
+    # Pop callstacks until we change context
+    leavingCtx = state.ctx
+
+    # Pop until we've left
+    while leavingCtx == state.ctx:
+
+        state.popCallStack()
 
     return [state]
 
-    """
-    else:
-        err = "Expr: Don't know how to handle expr type {0} at line {1} col {2}".format(type(expr),expr.lineno,expr.col_offset)
-        logger.error(err)
-        raise Exception(err)
-    """

pyState/functions/range.py

@@ -56,7 +56,7 @@ def handle(state,call,a,b=None,c=None,ctx=None):
 
         if type(a) not in [int,type(None)]:
             if a.isStatic():
-                a = a.value
+                a = a.getValue()
 
             # Check if it's a variable that only has one possibility
             elif type(a) in [Int, BitVec] and len(state.any_n_int(a,2)) == 1:
@@ -71,17 +71,15 @@ def handle(state,call,a,b=None,c=None,ctx=None):
         ##############
         # b Concrete #
         ##############
-
         if type(b) not in [int,type(None)]:
             if b.isStatic():
-                b = b.value
+                b = b.getValue()
 
             # Check if it's a variable that only has one possibility
             elif type(b) in [Int, BitVec] and len(state.any_n_int(b,2)) == 1:
                 b = state.any_int(b)
 
             else:
-                print(b.state.solver)
                 err = "handle: Don't know how to handle symbolic integers at the moment"
                 logger.error(err)
                 raise Exception(err)
@@ -93,7 +91,7 @@ def handle(state,call,a,b=None,c=None,ctx=None):
 
         if type(c) not in [int,type(None)]:
             if c.isStatic():
-                c = c.value
+                c = c.getValue()
 
             # Check if it's a variable that only has one possibility
             elif type(c) in [Int, BitVec] and len(state.any_n_int(c,2)) == 1:
@@ -108,7 +106,7 @@ def handle(state,call,a,b=None,c=None,ctx=None):
         # Create the return List object
         out = state.getVar("range",ctx=1,varType=List)
         out.increment()
-        
+
         if b == None:
             rangeOut = range(a)