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

Imprecise handling of implicit type conversion with union type #118

Closed marcoeilers closed 6 years ago

marcoeilers commented 6 years ago

The following code should verify, but at least one assertion fails:

from nagini_contracts.contracts import *
from typing import Union, List

def test_union_function(u: Union[List[int], int]) -> None:
    Requires(Implies(isinstance(u, list), list_pred(u)))
    if not u:
        if isinstance(u, int):
            assert u == 0
        else:
            assert len(u) == 0

The problem seems to be that if not u gets translated to if (!object___bool__(u)) instead of something like if (!(isinstance(u, int) ? int___bool__(u) : list___bool__(u))). My guess would be that we would have a similar problem in other situations where self.get_function_call is used internally.

fabiopakk commented 6 years ago

Problem analyzed and fixed in branch fabiopakk_implicit_type_conversion_on_union. Pull (and peer-review) requested.

fabiopakk commented 6 years ago

Merged.

fabiopakk commented 6 years ago

Branch renamed to: fabiopakk_issue_118_implicit_type_conversion