Skip to content

Commit d8590ea

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 d8590ea

File tree

1 file changed

+8
-0
lines changed

1 file changed

+8
-0
lines changed
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
package org.cprover;
2+
3+
/**
4+
* This can be added to methods to indicate they aren't allowed to throw
5+
* exceptions. JBMC and related tools will truncate any execution path on which
6+
* they do with an ASSUME FALSE instruction.
7+
*/
8+
public @interface MustNotThrow { }

0 commit comments

Comments
 (0)