Ignore synthetic locations in yaml witnesses

goblint.opam

@@ -68,7 +68,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: [
-  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#cc89da947d200575574de20867b56dbbbb2083bb" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#9118601602d34edf53f73b35996abf2296c2d900" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   # quoter workaround reverted for release, so no pin needed

goblint.opam.locked

@@ -124,7 +124,7 @@ version: "dev"
 pin-depends: [
   [
     "goblint-cil.1.8.2"
-    "git+https://github.com/goblint/cil.git#cc89da947d200575574de20867b56dbbbb2083bb"
+    "git+https://github.com/goblint/cil.git#9118601602d34edf53f73b35996abf2296c2d900"
   ]
   [
     "apron.v0.9.13"

goblint.opam.template

@@ -1,7 +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: [
-  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#cc89da947d200575574de20867b56dbbbb2083bb" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#9118601602d34edf53f73b35996abf2296c2d900" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   # quoter workaround reverted for release, so no pin needed

src/framework/cfgTools.ml

@@ -676,7 +676,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; endLine = -1; endByte = -1; endColumn = -1;}, Entry initfun) :: (BatHashtbl.keys inits |> BatList.of_enum)
+  ({line = 0; file="initfun"; byte= 0; column = 0; endLine = -1; endByte = -1; endColumn = -1; synthetic = true}, Entry initfun) :: (BatHashtbl.keys inits |> BatList.of_enum)
 
 
 let numGlobals file =

src/framework/control.ml

@@ -135,6 +135,7 @@ struct
           endLine = e;
           endColumn = -1; (* not shown *)
           endByte = 0; (* wrong, but not shown *)
+          synthetic = false;
         }
         in
         (doc, Some loc)

src/util/cilType.ml

@@ -79,7 +79,7 @@ struct
     | `Assoc l ->
       begin match List.assoc_opt "file" l, List.assoc_opt "line" l, List.assoc_opt "column" l, List.assoc_opt "byte" l with
         | Some (`String file), Some (`Int line), Some (`Int column), Some (`Int byte) ->
-          let loc = {file; line; column; byte; endLine = -1; endColumn = -1; endByte = -1} in
+          let loc = {file; line; column; byte; endLine = -1; endColumn = -1; endByte = -1; synthetic = false} in
           begin match List.assoc_opt "endLine" l, List.assoc_opt "endColumn" l, List.assoc_opt "endByte" l with
             | Some (`Int endLine), Some (`Int endColumn), Some (`Int endByte) ->
               Result.Ok {loc with endLine; endColumn; endByte}

src/witness/yamlWitness.ml

@@ -131,8 +131,9 @@ struct
     let nh = join_contexts lh in
 
     let yaml_entries = NH.fold (fun n local acc ->
+        let loc = Node.location n in
         match n with
-        | Statement _ when WitnessInvariant.is_invariant_node n ->
+        | Statement _ when not loc.synthetic && WitnessInvariant.is_invariant_node n ->
           let context: Invariant.context = {
             scope=Node.find_fundec n;
             i = -1;
@@ -143,7 +144,6 @@ struct
           in
           begin match Spec.D.invariant context local with
             | Some inv ->
-              let loc = Node.location n in
               let invs = WitnessUtil.InvariantExp.process_exp inv in
               List.fold_left (fun acc inv ->
                   let location_function = (Node.find_fundec n).svar.vname in
@@ -206,9 +206,11 @@ struct
     let file_loc_lvars: LvarS.t LocM.t FileH.t = FileH.create 100 in
     LHT.iter (fun ((n, _) as lvar) _ ->
         let loc = Node.location n in
-        FileH.modify_def LocM.empty loc.file (
-          LocM.modify_def LvarS.empty loc (LvarS.add lvar)
-        ) file_loc_lvars
+        if not loc.synthetic then (
+          FileH.modify_def LocM.empty loc.file (
+            LocM.modify_def LvarS.empty loc (LvarS.add lvar)
+          ) file_loc_lvars
+        )
       ) lh;
 
     let global_vars = List.filter_map (function
@@ -266,6 +268,7 @@ struct
           endLine = -1;
           endColumn = -1;
           endByte = -1;
+          synthetic = false;
         }
         in