search

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

Fixed issue 117: pure function calls on union receivers crash the verifier #122

Closed fabiopakk closed 6 years ago

fabiopakk commented 6 years ago

This is the pull request regarding issue 117. Additionally to the test case added from the issue report, other 3 test cases were added to fully exercise all possible inputs the modified function is expected to handle.

This change is Reviewable

marcoeilers commented 6 years ago

It seems that the implementation always tries to assign the results of the individual calls to a variable. That's a problem because that would not be possible in a pure context (e.g., inside a pure function). If all options for a call are pure functions, it would be better if the entire resulting translation was an expression, not a statement.

As an example, if you add a @Pure annotation to one of the functions in the new test, Nagini reports an invalid program:

@Pure
def test_union_pure_functions(u: Union[E, F]) -> int:
    Ensures(Result() == 5 or Result() == 7)
    return u.some_int()
fabiopakk commented 6 years ago

Good point, I'll handle this.

fabiopakk commented 6 years ago

Code changed to support @Pure as requested and also added the above example as test case. Please check if those modifications are compliant.

fabiopakk commented 6 years ago

Branch renamed to fabiopakk_issue_117_pure_functions.