Skip to content

Commit

Permalink
Add a regression test.
Browse files Browse the repository at this point in the history
  • Loading branch information
JohnDumbell committed Apr 11, 2018
1 parent c14e907 commit eea76ec
Show file tree
Hide file tree
Showing 3 changed files with 21 additions and 0 deletions.
Binary file not shown.
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
public class AssertionIssue {

public static void throwAssertion() {
throw new AssertionError("Something went terribly wrong.", new ThrowableAssertion());
}

public static class ThrowableAssertion extends Throwable {
@Override
public String getMessage() {
return "How did we get here?";
}
}
}
8 changes: 8 additions & 0 deletions regression/cbmc-java/assertion_error_constructors/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
AssertionIssue.class
--function AssertionIssue.throwAssertion
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring

0 comments on commit eea76ec

Please sign in to comment.