Skip to content

Commit f6bb383

Browse files
committed
Add MustNotThrow annotation
This can be added to methods to indicate they aren't allowed to throw exceptions. JBMC and related tools will truncate any execution path on which they do with an ASSUME FALSE instruction.
1 parent dbaaca5 commit f6bb383

File tree

1 file changed

+3
-0
lines changed

1 file changed

+3
-0
lines changed
Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
package org.cprover;
2+
3+
public @interface MustNotThrow { }

0 commit comments

Comments
 (0)