Merge branch 'master' into thread/join

Author: sim642

.gitignore

@@ -50,3 +50,5 @@ goblint.bc.js
 
 # Files generated by merge tools after conflicts
 *.orig
+
+sv-comp/goblint.zip

src/analyses/base.ml

@@ -697,7 +697,7 @@ struct
           let a1 = eval_rv a gs st e1 in
           let a2 = eval_rv a gs st e2 in
           let both_arith_type = isArithmeticType (typeOf e1) && isArithmeticType (typeOf e2) in
-          let is_safe = VD.equal a1 a2 || VD.is_safe_cast t1 (typeOf e1) && VD.is_safe_cast t2 (typeOf e2) && not both_arith_type in
+          let is_safe = (VD.equal a1 a2 || VD.is_safe_cast t1 (typeOf e1) && VD.is_safe_cast t2 (typeOf e2)) && not both_arith_type in
           M.tracel "cast" "remove cast on both sides for %a? -> %b\n" d_exp exp is_safe;
           if is_safe then ( (* we can ignore the casts if the values are equal anyway, or if the casts can't change the value *)
             let e1 = if isArithmeticType (typeOf e1) then c1 else e1 in
@@ -1870,7 +1870,7 @@ struct
         let start_addr = eval_tv ctx.ask ctx.global ctx.local start in
         List.filter_map (create_thread (Some (Mem id, NoOffset)) (Some ptc_arg)) (AD.to_var_may start_addr)
       end
-    | `Unknown _ -> begin
+    | `Unknown _ when get_bool "exp.unknown_funs_spawn" -> begin
         let args =
           match LF.get_invalidate_action f.vname with
           | Some fnc -> fnc `Write  args (* why do we only spawn arguments that are written?? *)
@@ -1934,7 +1934,7 @@ struct
   let special ctx (lv:lval option) (f: varinfo) (args: exp list) =
     (*    let heap_var = heap_var !Tracing.current_loc in*)
     let forks = forkfun ctx lv f args in
-    if M.tracing then M.tracel "spawn" "Base.special %s: spawning functions %a\n" f.vname (d_list "," d_varinfo) (List.map BatTuple.Tuple3.second forks);
+    if M.tracing then if not (List.is_empty forks) then M.tracel "spawn" "Base.special %s: spawning functions %a\n" f.vname (d_list "," d_varinfo) (List.map BatTuple.Tuple3.second forks);
     List.iter (BatTuple.Tuple3.uncurry ctx.spawn) forks;
     let cpa,dep as st = ctx.local in
     let gs = ctx.global in

src/domains/setDomain.ml

@@ -614,6 +614,7 @@ struct
   let inter = product_bot B.meet
   let meet = inter
   let subset = leq
+  let map' = map (* HACK: for PathSensitive morphstate *)
   let map f a = map f a |> reduce
   let min_elt a = B.bot ()
   let split x a = failwith "Hoare: unsupported split"

src/framework/constraints.ml

@@ -974,7 +974,7 @@ struct
 
   let exitstate  v = D.singleton (Spec.exitstate  v)
   let startstate v = D.singleton (Spec.startstate v)
-  let morphstate v d = D.map (Spec.morphstate v) d
+  let morphstate v d = D.map' (Spec.morphstate v) d
 
   let call_descr = Spec.call_descr
 

src/util/goblintutil.ml

@@ -119,7 +119,8 @@ let escape (x:string):string =
   Str.global_replace (Str.regexp "\"") """ |>
   Str.global_replace (Str.regexp "'") "'" |>
   Str.global_replace (Str.regexp "\x0b") "" |> (* g2html just cannot handle \v from some kernel benchmarks, even when escaped... *)
-  Str.global_replace (Str.regexp "\001") "" (* g2html just cannot handle \v from some kernel benchmarks, even when escaped... *)
+  Str.global_replace (Str.regexp "\001") "" |> (* g2html just cannot handle \v from some kernel benchmarks, even when escaped... *)
+  Str.global_replace (Str.regexp "\x0c") "" (* g2html just cannot handle \v from some kernel benchmarks, even when escaped... *)
 
 let trim (x:string): string =
   let len = String.length x in

src/witness/witnessConstraints.ml

@@ -85,6 +85,8 @@ struct
   let map (f: key -> key) (s: t): t = match s with
     | `Top -> `Top
     | `Lifted s -> `Lifted (M.fold (fun x v acc -> M.M.add (f x) (R.join v (M.find (f x) acc)) acc) s (M.M.empty))
+  let map' = map (* HACK: for PathSensitive morphstate *)
+  (* TODO: reducing map, like HoareSet *)
 
   module S =
   struct
@@ -296,7 +298,7 @@ struct
 
   let exitstate  v = (Dom.singleton (Spec.exitstate  v) (R.bot ()), Sync.bot ())
   let startstate v = (Dom.singleton (Spec.startstate v) (R.bot ()), Sync.bot ())
-  let morphstate v (d, _) = (Dom.map (Spec.morphstate v) d, Sync.bot())
+  let morphstate v (d, _) = (Dom.map' (Spec.morphstate v) d, Sync.bot ())
 
   let call_descr = Spec.call_descr
 

sv-comp/archive.sh

@@ -0,0 +1,11 @@
+#!/bin/bash
+
+cd ..
+
+rm goblint/sv-comp/goblint.zip
+
+zip goblint/sv-comp/goblint.zip \
+    goblint/goblint \
+    goblint/conf/svcomp21.json \
+    goblint/includes/sv-comp.c \
+    goblint/LICENSE

tests/regression/29-svcomp/21-issue-casting.c

@@ -0,0 +1,12 @@
+// PARAM: --set ana.activated ["'base'","'mallocWrapper'"]
+static long main(void)
+{
+  unsigned int cmd;
+  int __cil_tmp12 ;
+
+  if ((unsigned int )((int )cmd) == (unsigned int )__cil_tmp12) {
+    cmd = 17;
+  }
+
+  return 0;
+}