adding an infinity catch on "throw null" in symb ex.

Author: mattulbrich

key.core/src/main/java/de/uka/ilkd/key/macros/SymbolicExecutionOnlyMacro.java

@@ -152,12 +152,18 @@ public Name name() {
 
         @Override
         public boolean isApprovedApp(RuleApp app, PosInOccurrence pio, Goal goal) {
-            if(!hasModality(goal)) {
+            if(!hasModality(goal) || isThrowNullBranch(goal)) {
                 return false;
             }
             return isAdmittedRule(app) && super.isApprovedApp(app, pio, goal);
         }
 
+        /// Special case: Avoid infinite recursion on the "throw null" branch of tryCatchThrow
+        /// by forbidding continuation on this branch.
+        private boolean isThrowNullBranch(Goal goal) {
+            return "Null reference in throw".equals(goal.node().getNodeInfo().getBranchLabel());
+        }
+
         private boolean hasModality(Goal goal) {
             return modalityCache.computeIfAbsent(goal.node().sequent(), this::hasModality);
         }

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key

@@ -500,16 +500,26 @@
     tryCatchThrow {
         \find(\modality{#allmodal}{.. try { throw #se; #slist }
                 catch ( #t #v0 ) { #slist1 } ...}\endmodality (post))
-        \replacewith(\modality{#allmodal}{.. if ( #se == null ) {
-                      try { throw new java.lang.NullPointerException (); }
-                      catch ( #t #v0 ) { #slist1 }
-                } else if ( #se instanceof #t ) {
-                      #t #v0;
-                      #v0 = (#t) #se;
-                      #slist1
-                } else {
-                      throw #se;
-                } ...}\endmodality (post))
+
+        // Case NPE: throwing null fails:
+        "Null reference in throw":
+          \replacewith(\modality{#allmodal}{..
+                        try { throw new java.lang.NullPointerException (); }
+                        catch ( #t #v0 ) { #slist1 } ... }\endmodality (post))
+          \add( #se = null ==> ) ;
+
+        // Case catch or throw:
+        "Normal execution" [main]:
+          \replacewith(\modality{#allmodal}{..
+                  if ( #se instanceof #t ) {
+                        #t #v0;
+                        #v0 = (#t) #se;
+                        #slist1
+                  } else {
+                        throw #se;
+                  } ...}\endmodality (post))
+          \add( ==> #se = null )
+
         \heuristics(simplify_prog)
         \displayname "tryCatchThrow"
     };