Example of heap usage

Author: michael-schwarz

tests/regression/19-ghost-witness/11-empire-detect-bounds-malloc.c

@@ -0,0 +1,44 @@
+// CRAM
+// Like 05, but x is a global pointer to a dynamically allocated integer.
+#include<pthread.h>
+#include<stdlib.h>
+#include<goblint.h>
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int *x;
+
+
+void fun() {
+    int y = *x;
+    while (y> 0) {
+        y--;
+    }
+
+    (*x)++;
+}
+
+int main(void) {
+    int z;
+    int top;
+
+    x = malloc(sizeof(int));
+
+    if(top) { *x = 10000; }
+
+    pthread_t thread;
+    pthread_create(&thread, NULL, (void*)fun, NULL);
+
+    while(z != 0) {
+        z--;
+    }
+
+    (*x)++;
+
+    pthread_join(thread, NULL);
+
+    top = 8;
+    top = 3;
+
+    return 0;
+}

tests/regression/19-ghost-witness/11-empire-detect-bounds-malloc.t

@@ -0,0 +1,22 @@
+Run witness validation with `phaseGhost` on the empire example, but with `x`
+as a global pointer to a dynamically allocated integer.
+
+  $ goblint --disable warn.race --disable warn.integer --enable warn.deterministic --enable ana.sv-comp.functions --set witness.yaml.validate 11-empire-detect-bounds-malloc.yml --set ana.activated[+] phaseGhost --set ana.activated[+] phaseGhostSplit --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --set lib.activated[+] sv-comp --set ana.base.privatization protection-atomic-ghost --enable ana.int.interval --set colors never 11-empire-detect-bounds-malloc.c
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 17
+    dead: 0
+    total lines: 17
+  [Info][Witness] phaseGhost: global ghost_a is only accessed by unique thread [main, fun@11-empire-detect-bounds-malloc.c:30:5-30:51] and is only ever increased by one
+  [Info][Witness] phaseGhost: global ghost_b is only accessed by unique thread [main] and is only ever increased by one
+  [Info][Witness] witness validation summary:
+    confirmed: 3
+    unconfirmed: 0
+    refuted: 0
+    error: 0
+    unchecked: 0
+    unsupported: 0
+    disabled: 0
+    total validation entries: 3
+  [Success][Witness] invariant confirmed: (ghost_b == 0 && *x >= 1) || (ghost_b == 1 && *x >= 2) (11-empire-detect-bounds-malloc.c:19:1)
+  [Success][Witness] invariant confirmed: ghost_a == 1 && *x >= 2 (11-empire-detect-bounds-malloc.c:40:5)
+  [Success][Witness] invariant confirmed: ghost_b == 1 && *x >= 2 (11-empire-detect-bounds-malloc.c:40:5)

tests/regression/19-ghost-witness/11-empire-detect-bounds-malloc.yml

@@ -0,0 +1,91 @@
+- entry_type: ghost_instrumentation
+  metadata:
+    format_version: "2.1-goblint"
+    uuid: 00000000-0000-0000-0000-000000000033
+    creation_time: 2026-04-21T00:00:00Z
+    producer:
+      name: Test
+      version: "0.0"
+    task:
+      input_files:
+      - 11-empire-detect-bounds-malloc.c
+      input_file_hashes:
+        11-empire-detect-bounds-malloc.c: "0000000000000000000000000000000000000000000000000000000000000000"
+      data_model: LP64
+      language: C
+  content:
+    ghost_variables:
+    - name: ghost_a
+      scope: global
+      type: int
+      initial:
+        value: "0"
+        format: c_expression
+    - name: ghost_b
+      scope: global
+      type: int
+      initial:
+        value: "0"
+        format: c_expression
+    ghost_updates:
+    - location:
+        file_name: 11-empire-detect-bounds-malloc.c
+        line: 18
+        column: 5
+        function: fun
+      updates:
+      - variable: ghost_a
+        value: "ghost_a + 1"
+        format: c_expression
+    - location:
+        file_name: 11-empire-detect-bounds-malloc.c
+        line: 36
+        column: 5
+        function: main
+      updates:
+      - variable: ghost_b
+        value: "ghost_b + 1"
+        format: c_expression
+- entry_type: invariant_set
+  metadata:
+    format_version: "2.0"
+    uuid: 00000000-0000-0000-0000-000000000034
+    creation_time: 2026-04-21T00:00:00Z
+    producer:
+      name: Test
+      version: "0.0"
+    task:
+      input_files:
+      - 11-empire-detect-bounds-malloc.c
+      input_file_hashes:
+        11-empire-detect-bounds-malloc.c: "0000000000000000000000000000000000000000000000000000000000000000"
+      data_model: LP64
+      language: C
+  content:
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 11-empire-detect-bounds-malloc.c
+        line: 19
+        column: 1
+        function: fun
+      value: (ghost_b == 0 && *x >= 1) || (ghost_b == 1 && *x >= 2)
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 11-empire-detect-bounds-malloc.c
+        line: 40
+        column: 5
+        function: main
+      value: ghost_a == 1 && *x >= 2
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 11-empire-detect-bounds-malloc.c
+        line: 40
+        column: 5
+        function: main
+      value: ghost_b == 1 && *x >= 2
+      format: c_expression