Merge pull request #1579 from goblint/issue-1576

Add "ERROR (both branches dead)" verdict for SV-COMP

src/common/framework/analysisState.ml

@@ -36,3 +36,8 @@ let postsolving = ref false
 
 (* None if verification is disabled, Some true if verification succeeded, Some false if verification failed *)
 let verified : bool option ref = ref None
+
+let unsound_both_branches_dead: bool option ref = ref None
+(** [Some true] if unsound both branches dead occurs in analysis results.
+    [Some false] if it doesn't occur.
+    [None] if [ana.dead-code.branches] option is disabled and this isn't checked. *)

src/goblint.ml

@@ -65,6 +65,7 @@ let main () =
       do_gobview file;
       do_stats ();
       Goblint_timing.teardown_tef ();
+      (* TODO: generalize exit codes for AnalysisState.unsound_both_branches_dead? *)
       if !AnalysisState.verified = Some false then exit 3 (* verifier failed! *)
     )
   with

src/lifters/specLifters.ml

@@ -695,6 +695,10 @@ struct
       | x -> BatPrintf.fprintf f "<analysis name=\"dead-branch-lifter\">%a</analysis>" printXml x
   end
 
+  let init marshal =
+    init marshal;
+    AnalysisState.unsound_both_branches_dead := Some false
+
   let conv (ctx: (_, G.t, _, V.t) ctx): (_, S.G.t, _, S.V.t) ctx =
     { ctx with
       global = (fun v -> G.s (ctx.global (V.s v)));
@@ -717,6 +721,7 @@ struct
                 let cilinserted = if loc.synthetic then "(possibly inserted by CIL) " else "" in
                 M.warn ~loc:(Node g) ~tags:[CWE (if tv then 571 else 570)] ~category:Deadcode "condition '%a' %sis always %B" d_exp exp cilinserted tv
               | `Bot when not (CilType.Exp.equal exp one) -> (* all branches dead *)
+                AnalysisState.unsound_both_branches_dead := Some true;
                 M.msg_final Error ~category:Analyzer ~tags:[Category Unsound] "Both branches dead";
                 M.error ~loc:(Node g) ~category:Analyzer ~tags:[Category Unsound] "both branches over condition '%a' are dead" d_exp exp
               | `Bot (* all branches dead, fine at our inserted Neg(1)-s because no Pos(1) *)

src/util/server.ml

@@ -320,6 +320,7 @@ let () =
     let process { reset } serve =
       try
         analyze serve ~reset;
+        (* TODO: generalize VerifyError for AnalysisState.unsound_both_branches_dead *)
         {status = if !AnalysisState.verified = Some false then VerifyError else Success}
       with
       | Sys.Break ->

src/witness/witness.ml

@@ -691,9 +691,10 @@ struct
     )
 
   let write yaml_validate_result entrystates =
-    match !AnalysisState.verified with
-    | Some false -> print_svcomp_result "ERROR (verify)"
-    | _ ->
+    match !AnalysisState.verified, !AnalysisState.unsound_both_branches_dead with
+    | _, Some true -> print_svcomp_result "ERROR (both branches dead)"
+    | Some false, _ -> print_svcomp_result "ERROR (verify)"
+    | _, _ ->
       match yaml_validate_result with
       | Some (Stdlib.Error msg) ->
         print_svcomp_result ("ERROR (" ^ msg ^ ")")