Enable safely using doo files that were verified against other doo files #5335
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
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
priority: not yet
Will reconsider working on this when we're looking for work
If I have project A, A*, B and C, where B depends on A, C depends on B, and A and A* have the same type signature. Then if I build a.doo and a*.doo, then b.doo (passing in a.doo), and then c.doo (passing in b.doo, and a*.doo), then I can get Dafny to tell me everything verifies successfully, even though the verification done was not sound because a and a* may have different behavior.
Solution
--library
has that checksum.The text was updated successfully, but these errors were encountered: