Add test 56-witness/76-apron-unassume-extra-trivial

Author: sim642

tests/regression/56-witness/76-apron-unassume-extra-trivial.c

@@ -0,0 +1,11 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.apron.domain polyhedra --set ana.activated[+] unassume --set witness.yaml.unassume 76-apron-unassume-extra-trivial.yml
+#include <assert.h>
+// Using polyhedra instead of octagon, because the former has no narrowing and really needs the witness.
+int main() {
+  int i = 0;
+  while (i < 100) { // TODO: location invariant before loop doesn't work anymore
+    i++;
+  }
+  assert(i == 100);
+  return 0;
+}

tests/regression/56-witness/76-apron-unassume-extra-trivial.yml

@@ -0,0 +1,46 @@
+- entry_type: invariant_set
+  metadata:
+    format_version: "2.0"
+    uuid: 0a72f7b3-7826-4f68-bc7b-25425e95946e
+    creation_time: 2022-07-26T09:11:03Z
+    producer:
+      name: Goblint
+      version: heads/yaml-witness-unassume-0-g48503c690-dirty
+      command_line: '''./goblint'' ''--enable'' ''dbg.debug'' ''--enable'' ''dbg.regression''
+        ''--html'' ''--set'' ''ana.activated[+]'' ''apron'' ''--enable'' ''witness.yaml.enabled''
+        ''76-apron-unassume-extra-trivial.c'''
+    task:
+      input_files:
+      - 76-apron-unassume-extra-trivial.c
+      input_file_hashes:
+        76-apron-unassume-extra-trivial.c: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
+      data_model: LP64
+      language: C
+  content:
+  - invariant:
+      type: loop_invariant
+      location:
+        file_name: 76-apron-unassume-extra-trivial.c
+        line: 6
+        column: 3
+        function: main
+      value: 100LL - (long long )i >= 0LL
+      format: c_expression
+  - invariant:
+      type: loop_invariant
+      location:
+        file_name: 76-apron-unassume-extra-trivial.c
+        line: 6
+        column: 3
+        function: main
+      value: (long long )i >= 0LL
+      format: c_expression
+  - invariant:
+      type: loop_invariant
+      location:
+        file_name: 76-apron-unassume-extra-trivial.c
+        line: 6
+        column: 3
+        function: main
+      value: '1'
+      format: c_expression

tests/regression/56-witness/dune

@@ -23,7 +23,8 @@
      (run %{update_suite} apron-unassume-precheck -q)
      (run %{update_suite} apron-tracked-global-annot -q)
      (run %{update_suite} apron-unassume-no-strengthening -q)
-     (run %{update_suite} apron-unassume-set-tokens -q)))))
+     (run %{update_suite} apron-unassume-set-tokens -q)
+     (run %{update_suite} apron-unassume-extra-trivial -q)))))
 
 (cram
  (deps (glob_files *.c) (glob_files ??-*.yml) (glob_files strip-ghost-alloc.sh)))