AttributeError: 'NoneType' object has no attribute 'to_string'

[polgreen]

Hi,

I'm running Nagini on this example (taken from here, with one of the ensures statement of write_string changed:

from nagini_contracts.contracts import *
from nagini_contracts.io_contracts import *
from typing import Tuple, Callable

@IOOperation
def write_string_io(
        t_pre: Place,
        value: str,
        t_post: Place = Result(),
        ) -> bool:
    Terminates(True)

@ContractOnly   
def write_string(t1: Place, value: str) -> Place:
    IOExists1(Place)(
        lambda t2: (   
        Requires(
            token(t1, 1) and
            write_string_io(t1, value, t2)
        ),
        Ensures(
            not(token(t2))
            # token(t2) and
            # t2 == Result()
        ),
        )
    )

def hello(t1: Place) -> Place:
    IOExists1(Place)(
        lambda t2: (
        Requires(
            token(t1, 2) and
            write_string_io(t1, "Hello World!", t2)
        ),
        Ensures(
            token(t2) and
            t2 == Result()
        )
        )
    )

    t2 = write_string(t1, "Hello World!")

    return t2

Command: nagini test.py --z3 "/Users/elipol/Z3/build/z3" z3 version: Z3 version 4.8.9 - 64 bit OS: MacOS 10.15.5 python: Python 3.7.3 java: openjdk 11.0.6 2020-01-14

The error I get is:

Traceback (most recent call last):
  File "/Users/elipol/Library/Python/3.7/lib/python/site-packages/nagini_translation/main.py", line 188, in verify
    vresult = verifier.verify(prog, arp=arp)
  File "/Users/elipol/Library/Python/3.7/lib/python/site-packages/nagini_translation/verifier.py", line 128, in verify
    result = self.silicon.verify(prog)
jpype._jexception.java.util.concurrent.ExecutionExceptionPyRaisable: java.util.concurrent.ExecutionException: java.util.concurrent.ExecutionException: scala.MatchError: acc(MustInvokeUnbounded(old(get__write_string_io__t_post(t1, value_0))), write) (of class viper.silver.ast.PredicateAccessPredicate)
Traceback (most recent call last):
  File "/Users/elipol/Library/Python/3.7/bin/nagini", line 8, in <module>
    sys.exit(main())
  File "/Users/elipol/Library/Python/3.7/lib/python/site-packages/nagini_translation/main.py", line 329, in main
    translate_and_verify(args.python_file, jvm, args, arp=args.arp)
  File "/Users/elipol/Library/Python/3.7/lib/python/site-packages/nagini_translation/main.py", line 364, in translate_and_verify
    print(vresult.to_string(args.ide_mode, args.show_viper_errors))
AttributeError: 'NoneType' object has no attribute 'to_string'

[marcoeilers]

Thanks for filing the issue. The input program should be rejected, it should not be possible to negate permissions of any kind, including tokens and IO permissions.

[marcoeilers]

Fixed in commit f15319e6c12c9f0aa0b08378e2a6f9dc356fc76c.