search

mattulbrich / dive

Dafny Interactive Verification Environment (DIVE)
GNU General Public License v3.0
4 stars 0 forks source link

New proof script language #171

Closed mattulbrich closed 3 years ago

mattulbrich commented 4 years ago

The old script engine has lots of unneeded code from proof script debugger for KeY.

JonasKlamroth commented 4 years ago

i hope i fixed most of the NPEs. They came basically all from the same problem that node.getChildren may return null. I dont know if that is the intended behaviour or if it is more intuitive to just return an empty list. @mattulbrich what are your thoughts on that? the proofnodecheckpoints creation needs further adaptation but a rudimentary solution is working now. I could look into that if this PR is approved in general