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

Consistency check should be performed in Viper AST before verification #131

Closed fabiopakk closed 6 years ago

fabiopakk commented 6 years ago

Between analysis and verification (i.e. after translation), a call to silver's checkTransitively should be made, allowing inconsistencies in the generated Viper AST to be spotted before verification starts. Should problems exists verification must halt and a report should be printed listing all issues found.

This would reveal problems that are hidden in the AST and cannot be visualized even if pretty printing the Viper program, for example, missing or wrong localization information.

An earlier attempt to do so revealed error messages with the "_end" label commonly present in Viper programs generated by Nagini. Before committing this fix it is important to clear all error messages, otherwise it will immediately breaks all regression tests.

fabiopakk commented 6 years ago

Issue fixed in branch fabiopakk_issue_131_check_transitively, now merged into master.