From e1b39c6e9688105de5998b877e04e03d582595db Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Wed, 14 Nov 2018 23:18:15 +0000 Subject: [PATCH] Update jbmc/lib/java-models-library to #11 (enable-monitor-exceptions) Allows to detect errors related to synchronization on null references, for example. Fixes #1236. --- jbmc/lib/java-models-library | 2 +- jbmc/regression/jbmc/synchronized/test.desc | 5 ++--- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/jbmc/lib/java-models-library b/jbmc/lib/java-models-library index 3163b09a9f43..aeab60a26142 160000 --- a/jbmc/lib/java-models-library +++ b/jbmc/lib/java-models-library @@ -1 +1 @@ -Subproject commit 3163b09a9f43ebe637caf508427b52e41e1993f2 +Subproject commit aeab60a26142d59eb743982fbd8f5786a86fd68f diff --git a/jbmc/regression/jbmc/synchronized/test.desc b/jbmc/regression/jbmc/synchronized/test.desc index 7155ff813750..5921af6c5691 100644 --- a/jbmc/regression/jbmc/synchronized/test.desc +++ b/jbmc/regression/jbmc/synchronized/test.desc @@ -1,10 +1,9 @@ -KNOWNBUG +CORE Sync.class - +--java-threading --throw-runtime-exceptions --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- ^warning: ignoring -- -See #1236 for details of this test.