From d8590ea8749937ba29aff47ea74714f687edf3b5 Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Mon, 11 Jun 2018 16:35:10 +0100
Subject: [PATCH] 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.
---
src/main/java/org/cprover/MustNotThrow.java | 8 ++++++++
1 file changed, 8 insertions(+)
create mode 100644 src/main/java/org/cprover/MustNotThrow.java
diff --git a/src/main/java/org/cprover/MustNotThrow.java b/src/main/java/org/cprover/MustNotThrow.java
new file mode 100644
index 0000000..7be14b1
--- /dev/null
+++ b/src/main/java/org/cprover/MustNotThrow.java
@@ -0,0 +1,8 @@
+package org.cprover;
+
+/**
+ * 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.
+ */
+public @interface MustNotThrow { }