marcoeilers / nagini

Nagini is a static verifier for Python 3, based on the Viper verification infrastructure.
Mozilla Public License 2.0
233 stars 8 forks source link

Bad error messages for obligation-precondition-failures when calling builtins #112

Closed marcoeilers closed 6 years ago

marcoeilers commented 6 years ago

In the following code

from nagini_contracts.contracts import *
from nagini_contracts.obligations import MustTerminate
from typing import List

def newlist() -> List[int]:
    Requires(MustTerminate(2))
    res = []  # type: List[int]
    return res

def caller() -> None:
    Requires(MustTerminate(2))
    a = newlist()

we get a good error message Obligation leak check failed. Callee newlist might not take all unsatisfied obligations from the caller. (test.py@13.8). When changing the precondition of newlist to MustTerminate(1), we get a bad message that says nothing about obligations instead: The precondition of [] might not hold. (test.py@8.10)

marcoeilers commented 6 years ago

Fixed in PR #116