context.py 文件源码

def add_annotation_to_assignments(self, model, solver):
        """Add a type comment for every assignment statement in the context"""
        for node, z3_t in self.assignments:
            if (len(node.targets) == 1 and isinstance(node.targets[0], ast.Name)
               and sys.version_info[0] >= 3 and sys.version_info[1] >= 6):
                # Replace the normal assignment node with annotated assignment
                # Annotated assignment only supports single assignment (no tuples or lists)
                # To unparse the assignment statement into the new syntax of the variable annotation,
                # The class of the nodes needs to be AnnAssign, to be recognized by the unparser
                node.__class__ = ast.AnnAssign
                node.target = node.targets[0]
                node.simple = 1
                annotation_str = solver.annotation_resolver.unparse_annotation(
                    model[self.get_type(node.targets[0].id)])
                node.annotation = ast.parse(annotation_str).body[0].value

        # Add the type comment for assignments in children contexts
        for child in self.children_contexts:
            child.add_annotation_to_assignments(model, solver)