Skip to content

Commit f8c3526

Browse files
feat(kani): unit proof for add_used method (sec 2.8.22)
Verify that the add_used method updates the queue on success and does not update on failure. For this (and subsequent proofs), implement a stub region that supports stateful proofs. We add a unit proof to make sure that the stub region itself is working as intended. Signed-off-by: Siddharth Priya <[email protected]>
1 parent 433129f commit f8c3526

File tree

1 file changed

+341
-54
lines changed

1 file changed

+341
-54
lines changed

0 commit comments

Comments
 (0)