marcoeilers/nagini
Nagini is a static verifier for Python 3, based on the Viper verification infrastructure.
PythonMPL-2.0
Issues
- 0
Unsoundness involving union types
#196 opened by marcoeilers - 2
Disjunction in Requires / Ensures crashes Nagini
#186 opened by omkar-ethz - 1
Using Invariant outside of a loop crashes Nagini
#185 opened by omkar-ethz - 0
Nested super constructor calls crash Nagini
#176 opened by marcoeilers - 3
"Unsupported type: PartialType" Error
#169 opened by adh1s - 1
Tuple equality is very incomplete
#164 opened by marcoeilers - 3
Floating Point Verification Issues
#158 opened by ifndefJOSH - 0
Unsoundness relating to static fields
#161 opened by marcoeilers - 2
KeyError in `res_strict.graph` in Translator when using external library (`numpy`)
#159 opened by ifndefJOSH - 3
- 1
Static field access mistakenly considered
#119 opened by fabiopakk - 0
Jenkins build nagini-linux-xenial is failing
#80 opened by vakaras - 0
Improve collection axiomatization/triggering
#69 opened by marcoeilers - 2
Verification successful when it should fail
#150 opened by RCoeurjoly - 5
Verification successful when it should fail
#153 opened by nielstron - 0
Docs: Fold and Unfold
#151 opened by amacfie - 1
AssertionError without counterexample
#149 opened by RCoeurjoly - 3
There might be insufficient permission to access marked_execution_tree.children[0].function_name
#148 opened by RCoeurjoly - 2
Design by contract for python
#147 opened by adsharma - 0
- 2
Python 3.8.3 and MacOSx are not supported
#143 opened by sjunges - 2
- 2
Incomplete encoding of break
#141 opened by bobismijnnaam - 2
Install instructions no longer work
#140 opened by bobismijnnaam - 1
Does not compile with Python 3.5
#139 opened by ldanilek - 1
Some flake8 issues
#132 opened by cclauss - 0
- 1
- 1
ADT names could potentially crash
#120 opened by fabiopakk - 1
Subscript not properly working on Union
#127 opened by fabiopakk - 3
- 3
- 2
Verifier crashes when calling a method call that might or not return a value
#124 opened by fabiopakk - 0
Verification succeeds if 'select'ed names do not match anything in the program
#121 opened by marcoeilers - 1
- 1
Invalid code generated when iterating over empty list with complex loop target
#115 opened by marcoeilers - 1
Bad error messages for obligation-precondition-failures when calling builtins
#112 opened by marcoeilers - 0
Verification errors resulting from global constants defined in terms of mutable global state
#113 opened by marcoeilers - 0
- 0
Bad performance on examples
#107 opened by marcoeilers - 0
- 0
Definedness checks incomplete
#95 opened by marcoeilers - 0
- 7
- 0
- 2
Incorrect handling of 'and' and 'or'
#76 opened by marcoeilers - 0
- 0
- 1
- 0
Functions cannot be overridden
#70 opened by marcoeilers