Fixing crash #285

src/nagini_translation/lib/typeinfo.py

@@ -136,8 +136,8 @@ def visit_name_expr(self, node: mypy.nodes.NameExpr):
                 is_alias = True
                 break
         if (node.name not in LITERALS and not is_alias):
-            name_type = self.type_of(node)
-            if not isinstance(name_type, mypy.types.CallableType):
+            name_type = self.type_of_option(node)
+            if name_type and not isinstance(name_type, mypy.types.CallableType):
                 self.set_type(self.prefix + [node.name], name_type,
                               node.line, col(node))
 
@@ -221,7 +221,7 @@ def visit_call_expr(self, node: mypy.nodes.CallExpr):
             self.visit(a)
         self.visit(node.callee)
 
-    def type_of(self, node):
+    def type_of_option(self, node):
         if hasattr(node, 'node') and isinstance(node.node, mypy.nodes.MypyFile):
             return node.fullname
         if hasattr(node, 'node') and isinstance(node.node, mypy.nodes.TypeInfo):
@@ -253,12 +253,17 @@ def type_of(self, node):
             if tuple(fullname) in self.type_vars:
                 result = self.type_vars[tuple(fullname)]
                 return result
-        msg = self.path + ':' + str(node.get_line()) + ': error: '
-        if isinstance(node, mypy.nodes.FuncDef):
-            msg += 'Encountered Any type. Type annotation missing?'
-        else:
-            msg += 'dead.code'
-        raise TypeException([msg])
+
+    def type_of(self, node):
+        res = self.type_of_option(node)
+        if res is None:
+            msg = self.path + ':' + str(node.get_line()) + ': error: '
+            if isinstance(node, mypy.nodes.FuncDef):
+                msg += 'Encountered Any type. Type annotation missing?'
+            else:
+                msg += 'dead.code'
+            raise TypeException([msg])
+        return res
 
     def visit_comparison_expr(self, o: mypy.nodes.ComparisonExpr):
         # Weird things seem to happen with is-comparisons, so we ignore those.

tests/functional/verification/issues/00285.py

@@ -0,0 +1,18 @@
+# Any copyright is dedicated to the Public Domain.
+# http://creativecommons.org/publicdomain/zero/1.0/
+
+from typing import Generic, List, TypeVar
+from nagini_contracts.contracts import *
+
+T = TypeVar('T')
+
+
+class GenericResult(Generic[T]):
+    def __init__(self, data: T):
+        Ensures(Acc(self.data) and self.data is data)  # type: ignore
+        self.data = data
+
+
+class foo():
+    def bar(self) -> GenericResult[List[int]]:
+        return GenericResult[List[int]]([1, 2, 3])