From 0632eb656af9be8533236c900214da6d31372912 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 21 Jul 2016 13:19:53 +0000 Subject: [PATCH] PrismCL: Catch unhandled Exceptions instead of delegating to default Java handling We are now catching unhandled Exceptions and errorAndExit. Previously, we relied on the Java handling, which would print the stack trace and kill the main thread. However, it seems that in the presence of thread pools (e.g., with the JAS library used by param/exact model checking), an unhandled exception would kill the main thread but not terminate PRISM. This could be triggered e.g. with prism prism-examples/dice/dice.pm -pf 'P>0.5[ F s=7 ]' -exact which generates an unhandled ClassCastException and previously would make PRISM hang indefinitely. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11537 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/PrismCL.java | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 589ce6a7..566bf2ce 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -29,6 +29,8 @@ package prism; import java.io.File; import java.io.FileNotFoundException; import java.io.IOException; +import java.io.PrintWriter; +import java.io.StringWriter; import java.net.UnknownHostException; import java.util.ArrayList; import java.util.List; @@ -211,6 +213,15 @@ public class PrismCL implements PrismModelListener mainLog.println(st); } errorAndExit(e.getMessage() + ".\nTip: Try using the -cuddmaxmem switch to increase the memory available to CUDD"); + } catch (Exception e) { + // We catch Exceptions here ourself to ensure that we actually exit + // In the presence of thread pools (e.g., in the JAS library when using -exact), + // the main thread dying does not necessarily quit the program... + StringWriter sw = new StringWriter(); + sw.append("\n"); + e.printStackTrace(new PrintWriter(sw)); + mainLog.print(sw.toString()); + errorAndExit("Caught unhandled exception, aborting..."); } }