Using Invariant outside of a loop crashes Nagini

[omkar-ethz]

Minimal example:

from nagini_contracts.contracts import *

def crash() -> None:
    Invariant(True)

Expected output:

Translation failed
Invalid program: invalid.contract.position

Actual output:

  File "/home/omkar/ethz/hs23/prog-ver/nagini-dev/bin/nagini", line 8, in <module>
    sys.exit(main())
  File "/home/omkar/ethz/hs23/prog-ver/nagini-dev/lib/python3.8/site-packages/nagini_translation/main.py", line 375, in main
    success = translate_and_verify(args.python_file, jvm, args, arp=args.arp, base_dir=args.base_dir)
  File "/home/omkar/ethz/hs23/prog-ver/nagini-dev/lib/python3.8/site-packages/nagini_translation/main.py", line 388, in translate_and_verify
    modules, prog = translate(python_file, jvm, selected=selected, sif=args.sif, base_dir=base_dir,
  File "/home/omkar/ethz/hs23/prog-ver/nagini-dev/lib/python3.8/site-packages/nagini_translation/main.py", line 132, in translate
    collect_modules(analyzer, path)
  File "/home/omkar/ethz/hs23/prog-ver/nagini-dev/lib/python3.8/site-packages/nagini_translation/main.py", line 184, in collect_modules
    analyzer.analyze()
  File "/home/omkar/ethz/hs23/prog-ver/nagini-dev/lib/python3.8/site-packages/nagini_translation/analyzer.py", line 250, in analyze
    self.visit_module(self.module)
  File "/home/omkar/ethz/hs23/prog-ver/nagini-dev/lib/python3.8/site-packages/nagini_translation/analyzer.py", line 349, in visit_module
    self.visit(module.node, None)
  File "/home/omkar/ethz/hs23/prog-ver/nagini-dev/lib/python3.8/site-packages/nagini_translation/analyzer.py", line 380, in visit
    visitor(child_node)
  File "/home/omkar/ethz/hs23/prog-ver/nagini-dev/lib/python3.8/site-packages/nagini_translation/analyzer.py", line 364, in visit_Module
    self.visit_default(node)
  File "/home/omkar/ethz/hs23/prog-ver/nagini-dev/lib/python3.8/site-packages/nagini_translation/analyzer.py", line 374, in visit_default
    self.visit(item, node)
  File "/home/omkar/ethz/hs23/prog-ver/nagini-dev/lib/python3.8/site-packages/nagini_translation/analyzer.py", line 380, in visit
    visitor(child_node)
  File "/home/omkar/ethz/hs23/prog-ver/nagini-dev/lib/python3.8/site-packages/nagini_translation/analyzer.py", line 704, in visit_FunctionDef
    self.visit(child, node)
  File "/home/omkar/ethz/hs23/prog-ver/nagini-dev/lib/python3.8/site-packages/nagini_translation/analyzer.py", line 380, in visit
    visitor(child_node)
  File "/home/omkar/ethz/hs23/prog-ver/nagini-dev/lib/python3.8/site-packages/nagini_translation/analyzer.py", line 370, in visit_default
    self.visit(fieldval, node)
  File "/home/omkar/ethz/hs23/prog-ver/nagini-dev/lib/python3.8/site-packages/nagini_translation/analyzer.py", line 380, in visit
    visitor(child_node)
  File "/home/omkar/ethz/hs23/prog-ver/nagini-dev/lib/python3.8/site-packages/nagini_translation/analyzer.py", line 937, in visit_Call
    self.current_loop_invariant.append(
AttributeError: 'NoneType' object has no attribute 'append'

(Tested on both PyPI release and latest build)

[marcoeilers]

Fixed in #187