Force thread arguments to be added, as they will escape, but have not yet -- is there a better way?

Author: vesalvojdani

src/analyses/region.ml

@@ -187,7 +187,8 @@ struct
     let fd = Cilfacade.find_varinfo_fundec f in
     match args, fd.sformals with
     | [exp], [param] -> 
-      let reg = Reg.assign (Analyses.ask_of_ctx ctx) (var param) exp (ctx.global (), RegMap.bot ()) in
+      (* The parameter may not have escaped here (for the first thread). *)
+      let reg = Reg.assign ~thread_arg:true (Analyses.ask_of_ctx ctx) (var param) exp (ctx.global (), RegMap.bot ()) in
       [`Lifted (snd reg)] 
     | _ -> [`Lifted (RegMap.bot ())]
   let threadspawn ctx lval f args fctx = ctx.local

src/cdomains/regionDomain.ml

@@ -195,7 +195,7 @@ struct
       let p = RegPart.add s p in
       p, closure p m
 
-  let assign (ask: Queries.ask) (lval: lval) (rval: exp) (st: t): t =
+  let assign ?(thread_arg=false) (ask: Queries.ask) (lval: lval) (rval: exp) (st: t): t =
     (*    let _ = printf "%a = %a\n" (printLval plainCilPrinter) lval (printExp plainCilPrinter) rval in *)
     let t = Cilfacade.typeOf rval in
     if isPointerType t then begin (* TODO: this currently allows function pointers, e.g. in iowarrior, but should it? *)
@@ -209,7 +209,7 @@ struct
                 | `Right () -> `Right ()
               )
             in
-            match BaseUtil.is_global ask (fst x), deref_x, BaseUtil.is_global ask (fst y) with
+            match BaseUtil.is_global ask (fst x), deref_x, BaseUtil.is_global ask (fst y) || thread_arg with
             | false, false, true  ->
               p, RegMap.add x (append_offs_y (RegPart.closure p (RS.single_vf y))) m
             | false, false, false ->