Add witness invariant test for typedefs

goblint · Mar 1, 2024 · e4231ef · e4231ef
1 parent bb1a2ae
commit e4231ef
Show file tree

Hide file tree

Showing 2 changed files with 178 additions and 0 deletions.
diff --git a/tests/regression/witness/typedef.t/run.t b/tests/regression/witness/typedef.t/run.t
@@ -0,0 +1,163 @@
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' typedef.c
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 6
+    dead: 0
+    total lines: 6
+  [Info][Witness] witness generation summary:
+    total generation entries: 14
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 14
+      column: 2
+      function: main
+    location_invariant:
+      string: x == 42
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 14
+      column: 2
+      function: main
+    location_invariant:
+      string: q == (void *)(& a)
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 14
+      column: 2
+      function: main
+    location_invariant:
+      string: p == (void *)(& x)
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 14
+      column: 2
+      function: main
+    location_invariant:
+      string: a.f == 43
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 14
+      column: 2
+      function: main
+    location_invariant:
+      string: '*((myint *)p) == 42'
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 14
+      column: 2
+      function: main
+    location_invariant:
+      string: ((s *)q)->f == 43
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 13
+      column: 2
+      function: main
+    location_invariant:
+      string: x == 42
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 13
+      column: 2
+      function: main
+    location_invariant:
+      string: p == (void *)(& x)
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 13
+      column: 2
+      function: main
+    location_invariant:
+      string: a.f == 43
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 13
+      column: 2
+      function: main
+    location_invariant:
+      string: '*((myint *)p) == 42'
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 12
+      column: 2
+      function: main
+    location_invariant:
+      string: x == 42
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 12
+      column: 2
+      function: main
+    location_invariant:
+      string: p == (void *)(& x)
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 12
+      column: 2
+      function: main
+    location_invariant:
+      string: '*((myint *)p) == 42'
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 9
+      column: 2
+      function: main
+    location_invariant:
+      string: x == 42
+      type: assertion
+      format: C
diff --git a/tests/regression/witness/typedef.t/typedef.c b/tests/regression/witness/typedef.t/typedef.c
@@ -0,0 +1,15 @@
+typedef int myint;
+
+typedef struct {
+  int f;
+} s;
+
+int main() {
+  myint x = 42;
+  void *p = &x;
+
+  s a;
+  a.f = 43;
+  void *q = &a;
+  return 0;
+}