changeset 348:8e4ddc6083df

proof_burden: combine function now takes the right sub-expressions into account when looking for result and input expressions
author Sigurd Meldgaard <stm@daimi.au.dk>
date Mon, 19 Jul 2010 16:35:33 +0200
parents ef9c34427b2b
children b55032f81f15
files pysmcl/proof_burden.py
diffstat 1 files changed, 12 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/pysmcl/proof_burden.py	Mon Jul 19 16:07:07 2010 +0200
+++ b/pysmcl/proof_burden.py	Mon Jul 19 16:35:33 2010 +0200
@@ -55,13 +55,21 @@
         value.
         """
         if not children:
-            return frozenset()
-        return reduce(lambda x, y: x & y.out_values[key], children, init)
+            r = frozenset()
+        else:
+            r = reduce(lambda x, y: x & y.out_values[key], children, init)
+        return r
 
     def combine(node, env):
-        if find_inputs(node):
+        if isinstance(node, ast.If) or isinstance(node, ast.While):
+            subexpressions = node.test
+        elif isinstance(node, ast.For):
+            subexpressions = node.target
+        else:
+            subexpressions = node
+        if find_inputs(subexpressions):
             return frozenset()
-        new_results = find_results(node)
+        new_results = find_results(subexpressions)
         return frozenset(new_results) | env
 
     flow.analyze(f, join, combine, key, init,