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

Invalid code generated when iterating over empty list with complex loop target #115

Closed marcoeilers closed 6 years ago

marcoeilers commented 6 years ago

We get an unwanted exception for code like this:

def argh() -> None:
    flags = []  # type: List[Tuple[int, ...]]
    for (flag, *args) in flags:
        pass

We generate the following code that assigns the correct values to the flag variable before the loop, which raises a verification error because the precondition of getitem may not hold:

_cwl_144, loop_target, iter_err := Iterator___next__(_cthread_144, _method_measures_144, _residue_144, iter)
  flag := tuple___getitem__(loop_target, 0)
marcoeilers commented 6 years ago

Fixed in PR #116