Merge pull request #1709 from goblint/apron-unassume-no-strengthening

Use naïve unassume for Apron analysis when strengthening disabled

Author: sim642

src/analyses/apron/relationAnalysis.apron.ml

@@ -740,7 +740,12 @@ struct
         in
         ({ f } : Queries.ask) in
       let rel = RD.assert_inv dummyask rel e false (no_overflow ask e_orig) in (* assume *)
-      let rel = RD.keep_vars rel (List.map RV.local vars) in (* restrict *)
+      let rel =
+        if GobConfig.get_bool "ana.apron.strengthening" then
+          RD.keep_vars rel (List.map RV.local vars) (* restrict *)
+        else
+          rel (* naive unassume: will be homogeneous join below *)
+      in
 
       (* TODO: parallel write_global? *)
       let st =

tests/regression/56-witness/48-apron-unassume-no-strengthening.c

@@ -0,0 +1,14 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.apron.domain interval --set ana.activated[+] unassume --set witness.yaml.unassume 48-apron-unassume-no-strengthening.yml --disable ana.apron.strengthening
+#include <goblint.h>
+
+int main() {
+  int i = 0;
+  int j;
+  if (j < 100) {
+    __goblint_check(i == 0); // UNKNOWN (intentional by unassume)
+    __goblint_check(i >= 0);
+    __goblint_check(i < 100);
+    __goblint_check(j < 100);
+  }
+  return 0;
+}

tests/regression/56-witness/48-apron-unassume-no-strengthening.yml

@@ -0,0 +1,34 @@
+- entry_type: invariant_set
+  metadata:
+    format_version: "2.0"
+    uuid: 9b19e72a-376d-4c34-80d4-f46020de0c92
+    creation_time: 2025-03-12T12:53:06Z
+    producer:
+      name: Simmo Saan
+      version: n/a
+    task:
+      input_files:
+      - 48-apron-unassume-no-strengthening.c
+      input_file_hashes:
+        48-apron-unassume-no-strengthening.c: 57377f1e739e562d852b16206d5b1092e2188d3a4fe89bfca405a81bde0e1546
+      data_model: LP64
+      language: C
+  content:
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 48-apron-unassume-no-strengthening.c
+        line: 8
+        column: 5
+        function: main
+      value: i >= 0
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 48-apron-unassume-no-strengthening.c
+        line: 8
+        column: 5
+        function: main
+      value: i < 100
+      format: c_expression

tests/regression/56-witness/dune

@@ -22,6 +22,7 @@
      (run %{update_suite} bh-ex1-poly -q)
      (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)))))
 
 (cram