Merge branch 'goblint:master' into master

goblint · Apr 23, 2024 · 49a44c0 · 49a44c0
2 parents bfbfd88 + 98d9af4
commit 49a44c0
Show file tree

Hide file tree

Showing 4 changed files with 37 additions and 1 deletion.
diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
@@ -76,6 +76,7 @@ struct
               VH.find v_ins v
             else
               let v_in = Cilfacade.create_var @@ makeVarinfo false (v.vname ^ "#in") v.vtype in (* temporary local g#in for global g *)
+              v_in.vattr <- v.vattr; (* preserve goblint_relation_track attribute *)
               VH.replace v_ins v v_in;
               v_in
           in
@@ -97,6 +98,7 @@ struct
     let v_ins_inv = VH.create (List.length vs) in
     List.iter (fun v ->
         let v_in = Cilfacade.create_var @@ makeVarinfo false (v.vname ^ "#in") v.vtype in (* temporary local g#in for global g *)
+        v_in.vattr <- v.vattr; (* preserve goblint_relation_track attribute *)
         VH.replace v_ins_inv v_in v;
       ) vs;
     let rel = RD.add_vars st.rel (List.map RV.local (VH.keys v_ins_inv |> List.of_enum)) in (* add temporary g#in-s *)

diff --git a/src/common/domains/printable.ml b/src/common/domains/printable.ml
@@ -605,7 +605,7 @@ struct
       match BatDeque.front q with
       | None -> ()
       | Some (x, xs) -> (BatPrintf.fprintf f "<key>%d</key>\n%a\n" n Base.printXml x; 
-                   loop (n+1) (xs))
+                         loop (n+1) (xs))
     in
     BatPrintf.fprintf f "<value>\n<map>\n";
     loop 0 xs; 

diff --git a/tests/regression/56-witness/45-apron-tracked-global-annot.c b/tests/regression/56-witness/45-apron-tracked-global-annot.c
@@ -0,0 +1,9 @@
+// PARAM: --set ana.activated[+] apron --enable annotation.goblint_relation_track --set ana.activated[+] unassume --set witness.yaml.unassume 45-apron-tracked-global-annot.yml
+#include <goblint.h>
+
+int g __attribute__((__goblint_relation_track__)) = 0;
+
+int main() {
+  __goblint_check(g == 0); // unassume should not crash here
+  return 0;
+}
diff --git a/tests/regression/56-witness/45-apron-tracked-global-annot.yml b/tests/regression/56-witness/45-apron-tracked-global-annot.yml
@@ -0,0 +1,25 @@
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: d834761a-d0d7-4fea-bf42-2ff2b9a19143
+    creation_time: 2024-04-23T10:59:25Z
+    producer:
+      name: Simmo Saan
+      version: n/a
+    task:
+      input_files:
+      - 45-apron-tracked-global-annot.c
+      input_file_hashes:
+        45-apron-tracked-global-annot.c: 9c984e89a790b595d2b37ca8a05e5967a15130592cb2567fac2fae4aff668a4f
+      data_model: LP64
+      language: C
+  location:
+    file_name: 45-apron-tracked-global-annot.c
+    file_hash: 9c984e89a790b595d2b37ca8a05e5967a15130592cb2567fac2fae4aff668a4f
+    line: 7
+    column: 3
+    function: main
+  location_invariant:
+    string: g == 0
+    type: assertion
+    format: C