Add location ranges to output

goblint.opam

@@ -55,8 +55,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 pin-depends: [
-  # the published goblint-cil 1.8.2 is currently up-to-date, so no pin needed
-  # [ "goblint-cil.1.8.1" "git+https://github.com/goblint/cil.git#c16dddf74f6053a8b3fac07ca2feff18d4d56964" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#a3c91aa6e8f946fec9a9a13361b051a73b12a65c" ]
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   [ "ppx_deriving_yojson.3.6.1" "git+https://github.com/ocaml-ppx/ppx_deriving_yojson.git#e030f13a3450e9cf7d2c43fa04e709ef608486cd" ]
   [ "zarith.1.12-gob0" "git+https://github.com/goblint/Zarith.git#goblint-release-1.12" ]

goblint.opam.locked

@@ -78,6 +78,10 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 pin-depends: [
+  [
+    "goblint-cil.1.8.2"
+    "git+https://github.com/goblint/cil.git#a3c91aa6e8f946fec9a9a13361b051a73b12a65c"
+  ]
   [
     "apron.v0.9.13"
     "git+https://github.com/antoinemine/apron.git#c852ebcc89e5cf4a5a3318e7c13c73e1756abb11"

goblint.opam.template

@@ -1,8 +1,7 @@
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 pin-depends: [
-  # the published goblint-cil 1.8.2 is currently up-to-date, so no pin needed
-  # [ "goblint-cil.1.8.1" "git+https://github.com/goblint/cil.git#c16dddf74f6053a8b3fac07ca2feff18d4d56964" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#a3c91aa6e8f946fec9a9a13361b051a73b12a65c" ]
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   [ "ppx_deriving_yojson.3.6.1" "git+https://github.com/ocaml-ppx/ppx_deriving_yojson.git#e030f13a3450e9cf7d2c43fa04e709ef608486cd" ]
   [ "zarith.1.12-gob0" "git+https://github.com/goblint/Zarith.git#goblint-release-1.12" ]

scripts/update_suite.rb

@@ -392,7 +392,7 @@ def to_s
         vars = $1
         evals = $2
       end
-      next unless l =~ /(.*)\(.*?\:(\d+)(?:\:\d+)?\)/
+      next unless l =~ /(.*)\(.*?\:(\d+)(?:\:\d+)?(?:-(?:\d+)(?:\:\d+)?)?\)/
       obj,i = $1,$2.to_i
 
       ranking = ["other", "warn", "race", "norace", "deadlock", "nodeadlock", "success", "fail", "unknown", "term", "noterm"]

src/analyses/arinc.ml

@@ -99,7 +99,7 @@ struct
   (* function for creating a new intermediate node (will generate a new sid every time!) *)
   let mkDummyNode ?loc line =
     let loc = { (loc |? !Tracing.current_loc) with line = line } in
-    MyCFG.Statement { (mkStmtOneInstr @@ Set (var dummyFunDec.svar, zero, loc)) with sid = new_sid () }
+    MyCFG.Statement { (mkStmtOneInstr @@ Set (var dummyFunDec.svar, zero, loc, locUnknown)) with sid = new_sid () }
   (* table from sum type to negative line number for new intermediate node (-1 to -4 have special meanings) *)
   type tmpNodeUse = Branch of stmt | Combine of lval
   module NodeTbl = ArincUtil.SymTbl (struct type k = tmpNodeUse type v = MyCFG.node let getNew xs = mkDummyNode @@ -5 - (List.length (List.of_enum xs)) end)
@@ -217,7 +217,7 @@ struct
             (* let success = return_code_is_success i = tv in (* both must be true or false *) *)
             (* ignore(printf "if %s: %a = %B (line %i)\n" (if success then "success" else "error") d_plainexp exp tv (!Tracing.current_loc).line); *)
             (match env.node with
-             | MyCFG.Statement({ skind = If(e, bt, bf, loc); _ } as stmt) ->
+             | MyCFG.Statement({ skind = If(e, bt, bf, loc, eloc); _ } as stmt) ->
                (* 1. write out edges to predecessors, 2. set predecessors to current node, 3. write edge to the first node of the taken branch and set it as predecessor *)
                (* the then-block always has some stmts, but the else-block might be empty! in this case we use the successors of the if instead. *)
                let then_node = NodeTbl.get @@ Branch (List.hd bt.bstmts) in

src/analyses/mallocWrapperAnalysis.ml

@@ -76,8 +76,11 @@ struct
     | Q.HeapVar ->
       let node = match ctx.local with
         | `Lifted vinfo -> vinfo
-        | _ -> ctx.node in
-      `Lifted (get_heap_var node)
+        | _ -> ctx.node
+      in
+      let var = get_heap_var node in
+      var.vdecl <- UpdateCil.getLoc node; (* TODO: does this do anything bad for incremental? *)
+      `Lifted var
     | Q.IsHeapVar v ->
       NodeVarinfoMap.mem_varinfo v
     | Q.IsMultiple v ->

src/analyses/termination.ml

@@ -19,15 +19,15 @@ class loopCounterVisitor (fd : fundec) = object(self)
   inherit nopCilVisitor
   method! vstmt s =
     let action s = match s.skind with
-      | Loop (b, loc, _, _) ->
+      | Loop (b, loc, eloc, _, _) ->
         (* insert loop counter variable *)
         let name = "term"^show_location_id loc in
         let typ = intType in (* TODO the type should be the same as the one of the original loop counter *)
         let v = Goblintutil.create_var (makeLocalVar fd name ~init:(SingleInit zero) typ) in
         (* make an init stmt since the init above is apparently ignored *)
-        let init_stmt = mkStmtOneInstr @@ Set (var v, zero, loc) in
+        let init_stmt = mkStmtOneInstr @@ Set (var v, zero, loc, eloc) in
         (* increment it every iteration *)
-        let inc_stmt = mkStmtOneInstr @@ Set (var v, increm (Lval (var v)) 1, loc) in
+        let inc_stmt = mkStmtOneInstr @@ Set (var v, increm (Lval (var v)) 1, loc, eloc) in
         b.bstmts <- inc_stmt :: b.bstmts;
         let nb = mkBlock [init_stmt; mkStmt s.skind] in
         s.skind <- Block nb;
@@ -41,7 +41,7 @@ class loopBreaksVisitor (fd : fundec) = object(self)
   inherit nopCilVisitor
   method! vstmt s =
     (match s.skind with
-     | Loop (b, loc, Some continue, Some break) -> Hashtbl.add loopBreaks break.sid loc
+     | Loop (b, loc, eloc, Some continue, Some break) -> Hashtbl.add loopBreaks break.sid loc (* TODO: use eloc? *)
      | Loop _ -> failwith "Termination.preprocess: every loop should have a break and continue stmt after prepareCFG"
      | _ -> ());
     DoChildren
@@ -71,7 +71,7 @@ class loopVarsVisitor (fd : fundec) = object
       | _ -> ()
     in
     (match s.skind with
-     | If (e, tb, fb, loc) -> Option.map_default (add_exit_cond e) () (exits tb ||? exits fb)
+     | If (e, tb, fb, loc, eloc) -> Option.map_default (add_exit_cond e) () (exits tb ||? exits fb)
      | _ -> ());
     DoChildren
 end
@@ -97,39 +97,40 @@ let f_check  = Lval (var (emptyFunction "__goblint_check").svar)
 class loopInstrVisitor (fd : fundec) = object(self)
   inherit nopCilVisitor
   method! vstmt s =
+    (* TODO: use Loop eloc? *)
     (match s.skind with
-     | Loop (_, loc, _, _) ->
+     | Loop (_, loc, eloc, _, _) ->
        cur_loop' := !cur_loop;
        cur_loop := Some loc
      | _ -> ());
     let action s =
       (* first, restore old cur_loop *)
       (match s.skind with
-       | Loop (_, loc, _, _) ->
+       | Loop (_, loc, eloc, _, _) ->
          cur_loop := !cur_loop';
        | _ -> ());
       let in_loop () = Option.is_some !cur_loop && Hashtbl.mem loopVars (Option.get !cur_loop) in
       match s.skind with
-      | Loop (b, loc, Some continue, Some break) when Hashtbl.mem loopVars loc ->
+      | Loop (b, loc, eloc, Some continue, Some break) when Hashtbl.mem loopVars loc ->
         (* find loop var for current loop *)
         let x = Hashtbl.find loopVars loc in
         (* insert loop counter and diff to loop var *)
         let t = var @@ makeVar fd loc "t" in
         let d1 = var @@ makeVar fd loc "d1" in
         let d2 = var @@ makeVar fd loc "d2" in
         (* make init stmts *)
-        let t_init = mkStmtOneInstr @@ Set (t, zero, loc) in
-        let d1_init = mkStmtOneInstr @@ Set (d1, Lval x, loc) in
-        let d2_init = mkStmtOneInstr @@ Set (d2, Lval x, loc) in
+        let t_init = mkStmtOneInstr @@ Set (t, zero, loc, eloc) in
+        let d1_init = mkStmtOneInstr @@ Set (d1, Lval x, loc, eloc) in
+        let d2_init = mkStmtOneInstr @@ Set (d2, Lval x, loc, eloc) in
         (* increment/decrement in every iteration *)
-        let t_inc = mkStmtOneInstr @@ Set (t, increm (Lval t) 1, loc) in
-        let d1_inc = mkStmtOneInstr @@ Set (d1, increm (Lval d1) (-1), loc) in
-        let d2_inc = mkStmtOneInstr @@ Set (d2, increm (Lval d2)   1 , loc) in
+        let t_inc = mkStmtOneInstr @@ Set (t, increm (Lval t) 1, loc, eloc) in
+        let d1_inc = mkStmtOneInstr @@ Set (d1, increm (Lval d1) (-1), loc, eloc) in
+        let d2_inc = mkStmtOneInstr @@ Set (d2, increm (Lval d2)   1 , loc, eloc) in
         let typ = intType in
         let e1 = BinOp (Eq, Lval t, BinOp (MinusA, Lval x, Lval d1, typ), typ) in
         let e2 = BinOp (Eq, Lval t, BinOp (MinusA, Lval d2, Lval x, typ), typ) in
-        let inv1 = mkStmtOneInstr @@ Call (None, f_commit, [e1], loc) in
-        let inv2 = mkStmtOneInstr @@ Call (None, f_commit, [e2], loc) in
+        let inv1 = mkStmtOneInstr @@ Call (None, f_commit, [e1], loc, eloc) in
+        let inv2 = mkStmtOneInstr @@ Call (None, f_commit, [e2], loc, eloc) in
         (match b.bstmts with
          | cont :: cond :: ss ->
            (* changing succs/preds directly doesn't work -> need to replace whole stmts  *)
@@ -138,18 +139,18 @@ class loopInstrVisitor (fd : fundec) = object(self)
            s.skind <- Block nb;
          | _ -> ());
         s
-      | Loop (b, loc, Some continue, Some break) ->
+      | Loop (b, loc, eloc, Some continue, Some break) ->
         print_endline @@ "WARN: Could not determine loop variable for loop at " ^ CilType.Location.show loc;
         s
       | _ when Hashtbl.mem loopBreaks s.sid -> (* after a loop, we check that t is bounded/positive (no overflow happened) *)
         let loc = Hashtbl.find loopBreaks s.sid in
         let t = var @@ makeVar fd loc "t" in
         let e3 = BinOp (Ge, Lval t, zero, intType) in
-        let inv3 = mkStmtOneInstr @@ Call (None, f_check, [e3], loc) in
+        let inv3 = mkStmtOneInstr @@ Call (None, f_check, [e3], loc, locUnknown) in
         let nb = mkBlock [mkStmt s.skind; inv3] in
         s.skind <- Block nb;
         s
-      | Instr [Set (lval, e, loc)] when in_loop () ->
+      | Instr [Set (lval, e, loc, eloc)] when in_loop () ->
         (* find loop var for current loop *)
         let cur_loop = Option.get !cur_loop in
         let x = Hashtbl.find loopVars cur_loop in
@@ -161,17 +162,17 @@ class loopInstrVisitor (fd : fundec) = object(self)
           (match stripCastsDeep e with
            | BinOp (op, Lval x', e2, typ) when (op = PlusA || op = MinusA) && x' = x && isArithmeticType typ -> (* TODO x = 1 + x, MinusA! *)
              (* increase diff by same expr *)
-             let d1_inc = mkStmtOneInstr @@ Set (var d1, BinOp (PlusA, Lval (var d1), e2, typ), loc) in
-             let d2_inc = mkStmtOneInstr @@ Set (var d2, BinOp (PlusA, Lval (var d2), e2, typ), loc) in
+             let d1_inc = mkStmtOneInstr @@ Set (var d1, BinOp (PlusA, Lval (var d1), e2, typ), loc, eloc) in
+             let d2_inc = mkStmtOneInstr @@ Set (var d2, BinOp (PlusA, Lval (var d2), e2, typ), loc, eloc) in
              let nb = mkBlock [d1_inc; d2_inc; mkStmt s.skind] in
              s.skind <- Block nb;
              s
            | _ ->
              (* otherwise diff is e - counter *)
              let t = makeVar fd cur_loop "t" in
              let te = Cilfacade.typeOf e in
-             let dt1 = mkStmtOneInstr @@ Set (var d1, BinOp (MinusA, Lval x, Lval (var t), te), loc) in
-             let dt2 = mkStmtOneInstr @@ Set (var d2, BinOp (MinusA, Lval x, Lval (var t), te), loc) in
+             let dt1 = mkStmtOneInstr @@ Set (var d1, BinOp (MinusA, Lval x, Lval (var t), te), loc, eloc) in
+             let dt2 = mkStmtOneInstr @@ Set (var d2, BinOp (MinusA, Lval x, Lval (var t), te), loc, eloc) in
              let nb = mkBlock [mkStmt s.skind; dt1; dt2] in
              s.skind <- Block nb;
              s

src/analyses/threadId.ml

@@ -90,11 +90,11 @@ struct
     | _ -> Queries.Result.top x
 
   let threadenter ctx lval f args =
-    [(create_tid ctx.local ctx.node f, TD.bot ())]
+    [(create_tid ctx.local ctx.prev_node f, TD.bot ())]
 
   let threadspawn ctx lval f args fctx =
     let (current, td) = ctx.local in
-    (current, Thread.threadspawn td ctx.node f)
+    (current, Thread.threadspawn td ctx.prev_node f)
 
   type marshal = Thread.marshal
   let init m =

src/framework/cfgTools.ml

@@ -288,8 +288,8 @@ let createCFG (file: file) =
 
           | Instr instrs -> (* non-empty Instr *)
             let edge_of_instr = function
-              | Set (lval,exp,loc) -> loc, Assign (lval, exp)
-              | Call (lval,func,args,loc) -> loc, Proc (lval,func,args)
+              | Set (lval,exp,loc,eloc) -> eloc, Assign (lval, exp) (* TODO: eloc loc fallback if unknown here and If *)
+              | Call (lval,func,args,loc,eloc) -> eloc, Proc (lval,func,args)
               | Asm (attr,tmpl,out,inp,regs,loc) -> loc, ASM (tmpl,out,inp)
               | VarDecl (v, loc) -> loc, VDecl(v)
             in
@@ -301,7 +301,7 @@ let createCFG (file: file) =
               | _ -> failwith "MyCFG.createCFG: >1 non-empty Instr succ"
             end
 
-          | If (exp, _, _, loc) ->
+          | If (exp, _, _, loc, eloc) ->
             (* Cannot use true and false blocks from If constructor, because blocks don't have succs (stmts do).
                Cannot use first stmt in block either, because block may be empty (e.g. missing branch). *)
             (* Hence we rely on implementation detail of the If case in CIL's succpred_stmt.
@@ -313,10 +313,10 @@ let createCFG (file: file) =
               | [same_stmt] -> (same_stmt, same_stmt)
               | _ -> failwith "MyCFG.createCFG: invalid number of If succs"
             in
-            addEdge (Statement stmt) (loc, Test (exp, true )) (Statement true_stmt);
-            addEdge (Statement stmt) (loc, Test (exp, false)) (Statement false_stmt)
+            addEdge (Statement stmt) (eloc, Test (exp, true )) (Statement true_stmt);
+            addEdge (Statement stmt) (eloc, Test (exp, false)) (Statement false_stmt)
 
-          | Loop (_, loc, Some cont, Some brk) -> (* TODO: use loc for something? *)
+          | Loop (_, loc, eloc, Some cont, Some brk) -> (* TODO: use loc for something? *)
             (* CIL already converts Loop logic to Gotos and If. *)
             (* CIL eliminates the constant true If corresponding to constant true Loop.
                Then there is no Goto to after the loop and the CFG is unconnected (to Function node).
@@ -336,7 +336,7 @@ let createCFG (file: file) =
                 ()
             end
 
-          | Loop (_, _, _, _) ->
+          | Loop (_, _, _, _, _) ->
             (* CIL's xform_switch_stmt (via prepareCFG) always adds both continue and break statements to all Loops. *)
             failwith "MyCFG.createCFG: unprepared Loop"
 
@@ -532,7 +532,7 @@ struct
       | _ -> ["label=\"" ^ String.escaped (Node.show_cfg n) ^ "\""]
     in
     let shape = match n with
-      | Statement {skind=If (_,_,_,_); _}  -> ["shape=diamond"]
+      | Statement {skind=If (_,_,_,_,_); _}  -> ["shape=diamond"]
       | Statement _     -> [] (* use default shape *)
       | Function _
       | FunctionEntry _ -> ["shape=box"]
@@ -697,7 +697,7 @@ let getGlobalInits (file: file) : edges  =
   iterGlobals file f;
   let initfun = emptyFunction "__goblint_dummy_init" in
   (* order is not important since only compile-time constants can be assigned *)
-  ({line = 0; file="initfun"; byte= 0; column = 0}, Entry initfun) :: (BatHashtbl.keys inits |> BatList.of_enum)
+  ({line = 0; file="initfun"; byte= 0; column = 0; endLine = -1; endByte = -1; endColumn = -1;}, Entry initfun) :: (BatHashtbl.keys inits |> BatList.of_enum)
 
 
 let numGlobals file =

src/incremental/compareAST.ml

@@ -172,17 +172,17 @@ and eq_lval (a: lval) (b: lval) = match a, b with
     (host1, off1), (host2, off2) -> eq_lhost host1 host2 && eq_offset off1 off2
 
 let eq_instr (a: instr) (b: instr) = match a, b with
-  | Set (lv1, exp1, _l1), Set (lv2, exp2, _l2) -> eq_lval lv1 lv2 && eq_exp exp1 exp2
-  | Call (Some lv1, f1, args1, _l1), Call (Some lv2, f2, args2, _l2) -> eq_lval lv1 lv2 && eq_exp f1 f2 && eq_list eq_exp args1 args2
-  | Call (None, f1, args1, _l1), Call (None, f2, args2, _l2) -> eq_exp f1 f2 && eq_list eq_exp args1 args2
+  | Set (lv1, exp1, _l1, _el1), Set (lv2, exp2, _l2, _el2) -> eq_lval lv1 lv2 && eq_exp exp1 exp2
+  | Call (Some lv1, f1, args1, _l1, _el1), Call (Some lv2, f2, args2, _l2, _el2) -> eq_lval lv1 lv2 && eq_exp f1 f2 && eq_list eq_exp args1 args2
+  | Call (None, f1, args1, _l1, _el1), Call (None, f2, args2, _l2, _el2) -> eq_exp f1 f2 && eq_list eq_exp args1 args2
   | Asm (attr1, tmp1, ci1, dj1, rk1, l1), Asm (attr2, tmp2, ci2, dj2, rk2, l2) -> eq_list String.equal tmp1 tmp2 && eq_list(fun (x1,y1,z1) (x2,y2,z2)-> x1 = x2 && y1 = y2 && eq_lval z1 z2) ci1 ci2 && eq_list(fun (x1,y1,z1) (x2,y2,z2)-> x1 = x2 && y1 = y2 && eq_exp z1 z2) dj1 dj2 && eq_list String.equal rk1 rk2(* ignore attributes and locations *)
   | VarDecl (v1, _l1), VarDecl (v2, _l2) -> eq_varinfo v1 v2
   | _, _ -> false
 
 let eq_label (a: label) (b: label) = match a, b with
     Label (lb1, _l1, s1), Label (lb2, _l2, s2) -> lb1 = lb2 && s1 = s2
-  |   Case (exp1, _l1), Case (exp2, _l2) -> exp1 = exp2
-  | Default _l1, Default l2 -> true
+  |   Case (exp1, _l1, _el1), Case (exp2, _l2, el_2) -> exp1 = exp2
+  | Default (_l1, _el1), Default (_l2, _el2) -> true
   | _, _ -> false
 
 (* This is needed for checking whether a goto does go to the same semantic location/statement*)
@@ -205,9 +205,9 @@ let rec eq_stmtkind ?(cfg_comp = false) ((a, af): stmtkind * fundec) ((b, bf): s
   | Goto (st1, _l1), Goto (st2, _l2) -> eq_stmt_with_location (!st1, af) (!st2, bf)
   | Break _, Break _ -> if cfg_comp then failwith "CompareCFG: Invalid stmtkind in CFG" else true
   | Continue _, Continue _ -> if cfg_comp then failwith "CompareCFG: Invalid stmtkind in CFG" else true
-  | If (exp1, then1, else1, _l1), If (exp2, then2, else2, _l2) -> eq_exp exp1 exp2 && eq_block' then1 then2 && eq_block' else1 else2
-  | Switch (exp1, block1, stmts1, _l1), Switch (exp2, block2, stmts2, _l2) -> if cfg_comp then failwith "CompareCFG: Invalid stmtkind in CFG" else eq_exp exp1 exp2 && eq_block' block1 block2 && eq_list (fun a b -> eq_stmt (a,af) (b,bf)) stmts1 stmts2
-  | Loop (block1, _l1, _con1, _br1), Loop (block2, _l2, _con2, _br2) -> eq_block' block1 block2
+  | If (exp1, then1, else1, _l1, _el1), If (exp2, then2, else2, _l2, _el2) -> eq_exp exp1 exp2 && eq_block' then1 then2 && eq_block' else1 else2
+  | Switch (exp1, block1, stmts1, _l1, _el1), Switch (exp2, block2, stmts2, _l2, _el2) -> if cfg_comp then failwith "CompareCFG: Invalid stmtkind in CFG" else eq_exp exp1 exp2 && eq_block' block1 block2 && eq_list (fun a b -> eq_stmt (a,af) (b,bf)) stmts1 stmts2
+  | Loop (block1, _l1, _el1, _con1, _br1), Loop (block2, _l2, _el2, _con2, _br2) -> eq_block' block1 block2
   | Block block1, Block block2 -> eq_block' block1 block2
   | TryFinally (tryBlock1, finallyBlock1, _l1), TryFinally (tryBlock2, finallyBlock2, _l2) -> eq_block' tryBlock1 tryBlock2 && eq_block' finallyBlock1 finallyBlock2
   | TryExcept (tryBlock1, exn1, exceptBlock1, _l1), TryExcept (tryBlock2, exn2, exceptBlock2, _l2) -> eq_block' tryBlock1 tryBlock2 && eq_block' exceptBlock1 exceptBlock2