Improve handling of Kind 2 exit codes

ge-high-assurance · May 22, 2023 · c4c0c51 · c4c0c51
1 parent 1a60d83
commit c4c0c51
Showing 1 changed file with 20 additions and 21 deletions.
diff --git a/...-back-ends/verdict-bundle/verdict-bundle-app/src/main/java/com/ge/verdict/bundle/App.java b/...-back-ends/verdict-bundle/verdict-bundle-app/src/main/java/com/ge/verdict/bundle/App.java
@@ -1034,9 +1034,8 @@ public static void runCrv(
                         func_cong_val);
             }
         } catch (Binary.ExecutionException e) {
-            // Kind2 does some weird things with exit codes
+            // The SWITCH below uses the exit code convention followed by Kind 2 v1.9.0 and later
             if (e.getCode().isPresent()) {
-                // The switch below uses the exit code convention followed by Kind 2 v1.9.0 and later
                 switch (e.getCode().get()) {
                     case 0: // Former convention: 20
                         // Success
@@ -1046,40 +1045,40 @@ public static void runCrv(
                         if (atg) {
                             // Some properties invalid, but those might just be the ATG negative
                             // properties
-                            log("Kind2 finished");
+                            log("Kind 2 finished");
                         } else {
                             // Some properties invalid
                             log("Some properties are invalid");
                         }
                         break;
+                    case 30: // Former convention: 0
+                        log("Kind 2 timed out");
+                        break;
                     case 1: // Former convention: 2
-                        log("Kind2 terminated with a general error");
+                        logError("Kind 2 terminated with a general error");
                         XMLProcessor.parseLog(new File(outputPath));
-                        // Terminate the process?
-                        break;
+                        System.exit(2);
                     case 2:
-                        log("Kind2 terminated with an error: incorrect command-line argument");
+                        logError("Kind 2 received an invalid command-line argument");
                         XMLProcessor.parseLog(new File(outputPath));
-                        // Terminate the process?
-                        break;
+                        System.exit(2);
                     case 3:
-                        log("Kind2 terminated with a parse error");
+                        logError("Kind 2 terminated with a parse error");
                         XMLProcessor.parseLog(new File(outputPath));
-                        // Terminate the process?
-                        break;
+                        System.exit(2);
                     case 4:
-                        log("Kind2 could not find an SMT solver on the PATH");
+                        logError("Kind 2 could not find an SMT solver on the PATH");
                         XMLProcessor.parseLog(new File(outputPath));
-                        // Terminate the process?
-                        break;
+                        System.exit(2);
                     case 5:
-                        log("Kind2 detected an unknown or unsupported version of an SMT solver");
+                        logError("Kind 2 detected an unknown or unsupported SMT solver version");
                         XMLProcessor.parseLog(new File(outputPath));
-                        // Terminate the process?
-                        break;
-                    case 30: // Former convention: 0
-                        log("Kind2 timed out");
-                        break;
+                        System.exit(2);
+                    case 10:
+                    case 20:
+                        logError(
+                                "Detected an old version of Kind 2. Please update kind2 binary to v1.9.0 or later");
+                        System.exit(2);
                     default:
                         throw new VerdictRunException("Failed to execute kind2", e);
                 }