Automate manual tests

scripts/update_suite.rb

@@ -203,6 +203,8 @@ def compare_warnings
         check.call warnings[idx] != "race"
       when "nodeadlock"
         check.call warnings[idx] != "deadlock"
+      when "nocrash", "fixpoint", "notimeout", "cram"
+        check.call true
       end
     end
   end
@@ -281,6 +283,15 @@ def parse_tests (lines)
       if obj =~ /#line ([0-9]+).*$/ then
         i = $1.to_i - 1
       end
+      if obj =~ /NOCRASH/ then
+        tests[-42] = "nocrash"
+      elsif obj =~ /FIXPOINT/ then
+        tests[-42] = "fixpoint"
+      elsif obj =~ /NOTIMEOUT/ then
+        tests[-42] = "notimeout"
+      elsif obj =~ /CRAM/ then
+        tests[-42] = "cram"
+      end
       next if obj =~ /^\s*\/\// || obj =~ /^\s*\/\*([^*]|\*+[^*\/])*\*\/$/
       todo << i if obj =~ /TODO|SKIP/
       tests_line[i] = obj
@@ -312,6 +323,9 @@ def parse_tests (lines)
     when /TERM/
       tests[-1] = "term"
     end
+    if tests.empty? then
+      puts "No automatic checks in #{@id} (maybe NOCRASH/FIXPOINT/NOTIMEOUT/CRAM?)"
+    end
     Tests.new(self, tests, tests_line, todo)
   end
 

src/analyses/apron/apronAnalysis.apron.ml

@@ -542,7 +542,7 @@ struct
     |> List.enum
     |> Enum.filter_map (fun (lincons1: Lincons1.t) ->
         (* filter one-vars *)
-        if one_var || Apron.Linexpr0.get_size lincons1.lincons0.linexpr0 >= 2 then
+        if one_var || Lincons1.num_vars lincons1 >= 2 then
           CilOfApron.cil_exp_of_lincons1 lincons1
           |> Option.map e_inv
           |> Option.filter (fun exp -> not (InvariantCil.exp_contains_tmp exp) && InvariantCil.exp_is_in_scope scope exp)

src/analyses/base.ml

@@ -2151,7 +2151,7 @@ struct
      | _ -> ()
     );
     match lval with (* this section ensure global variables contain bottom values of the proper type before setting them  *)
-    | (Var v, offs) when AD.is_definite lval_val && v.vglob ->
+    | (Var v, offs) when v.vglob ->
       (* Optimization: In case of simple integral types, we not need to evaluate the old value.
           v is not an allocated block, as v directly appears as a variable in the program;
           so no explicit check is required here (unlike in set) *)
@@ -2163,14 +2163,14 @@ struct
       in
       begin match current_val with
         | `Bot -> (* current value is VD `Bot *)
-          begin match Addr.to_var_offset (AD.choose lval_val) with
-            | Some (x,offs) ->
+          begin match AD.to_var_offset lval_val with
+            | [(x,offs)] ->
               let t = v.vtype in
               let iv = VD.bot_value t in (* correct bottom value for top level variable *)
-              if M.tracing then M.tracel "set" "init bot value: %a\n" VD.pretty iv;
+              if M.tracing then M.tracel "set" "init bot value (%a): %a\n" d_plaintype t VD.pretty iv;
               let nv = VD.update_offset (Analyses.ask_of_ctx ctx) iv offs rval_val (Some  (Lval lval)) lval t in (* do desired update to value *)
               set_savetop ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local (AD.from_var v) lval_t nv ~lval_raw:lval ~rval_raw:rval (* set top-level variable to updated value *)
-            | None ->
+            | _ ->
               set_savetop ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval_val lval_t rval_val ~lval_raw:lval ~rval_raw:rval
           end
         | _ ->

src/cdomains/apron/apronDomain.apron.ml

@@ -158,6 +158,15 @@ struct
 
   let show = Format.asprintf "%a" print
   let compare x y = String.compare (show x) (show y) (* HACK *)
+
+  let num_vars x =
+    (* Apron.Linexpr0.get_size returns some internal nonsense, so we count ourselves. *)
+    let size = ref 0 in
+    Lincons1.iter (fun coeff var ->
+        if not (Apron.Coeff.is_zero coeff) then
+          incr size
+      ) x;
+    !size
 end
 
 module Lincons1Set =

src/framework/control.ml

@@ -215,6 +215,7 @@ struct
       let is_std = function
         | {vname = ("__tzname" | "__daylight" | "__timezone"); _} (* unix time.h *)
         | {vname = ("tzname" | "daylight" | "timezone"); _} (* unix time.h *)
+        | {vname = "getdate_err"; _} (* unix time.h (only on MacOS?) *)
         | {vname = ("stdin" | "stdout" | "stderr"); _} -> (* standard stdio.h *)
           true
         | _ -> false

src/witness/yamlWitnessType.ml

@@ -105,6 +105,7 @@ struct
     column: int;
     function_: string;
   }
+  [@@deriving ord]
 
   let to_yaml {file_name; file_hash; line; column; function_} =
     `O [
@@ -132,6 +133,7 @@ struct
     type_: string;
     format: string;
   }
+  [@@deriving ord]
 
   let to_yaml {string; type_; format} =
     `O [
@@ -154,6 +156,7 @@ struct
     location: Location.t;
     loop_invariant: Invariant.t;
   }
+  [@@deriving ord]
 
   let entry_type = "loop_invariant"
 
@@ -175,6 +178,7 @@ struct
   type t = {
     flow_insensitive_invariant: Invariant.t;
   }
+  [@@deriving ord]
 
   let entry_type = "flow_insensitive_invariant"
 
@@ -196,6 +200,7 @@ struct
     loop_invariant: Invariant.t;
     precondition: Invariant.t;
   }
+  [@@deriving ord]
 
   let entry_type = "precondition_loop_invariant"
 
@@ -221,6 +226,7 @@ struct
     type_: string;
     file_hash: string;
   }
+  [@@deriving ord]
 
   let to_yaml {uuid; type_; file_hash} =
     `O [
@@ -244,6 +250,7 @@ struct
     type_: string;
     format: string;
   }
+  [@@deriving ord]
 
   let to_yaml {string; type_; format} =
     `O [
@@ -266,6 +273,7 @@ struct
     target: Target.t;
     certification: Certification.t;
   }
+  [@@deriving ord]
 
   let entry_type = "loop_invariant_certificate"
 
@@ -297,6 +305,7 @@ struct
     | PreconditionLoopInvariant of PreconditionLoopInvariant.t
     | LoopInvariantCertificate of LoopInvariantCertificate.t
     | PreconditionLoopInvariantCertificate of PreconditionLoopInvariantCertificate.t
+  [@@deriving ord]
 
   let entry_type = function
     | LoopInvariant _ -> LoopInvariant.entry_type

tests/regression/00-sanity/18-parse-empty-array.c

@@ -1,4 +1,5 @@
 // Test for issue in https://github.com/goblint/cil/issues/19
+// NOCRASH
 static int a[];
 static int a[] = {};
 static int b[0] = {};

tests/regression/00-sanity/29-earlyglobs-insens.c

@@ -1,2 +1,3 @@
 // PARAM: --set ana.ctx_insens[+] base --enable exp.earlyglobs
+// NOCRASH
 int main() {}

tests/regression/00-sanity/33-hoare-over-paths.c

@@ -27,8 +27,8 @@ int main() {
   // NEW explanation:
   // using SensitiveDomain correctly keeps both paths as path-sensitivity demands
 
-  // TODO: manually check final join node in HTML
-  // cannot be automated because concrete execution cannot check
+  // cram test checks internal result
+  // cannot be automated with annotations because concrete execution cannot check
   // if _must_ lockset _may_ contain m on some path
   return 0;
 }