Include directives can lead to including unverified code in doo files #4762
Labels
during 3: execution of incorrect program
An bug in the verifier that allows Dafny to run a program that does not correctly implement its spec
part: tools
Tools built on top of Dafny
This is arguably the documented behavior since
include
d files are not verified by default, but given.doo
files are intended to be the safest way to allow skipping verification later on, I say they should not include the source of unverified files.The text was updated successfully, but these errors were encountered: