Support reordered pointer operands in local_bitvector_analysis

regression/goto-instrument/local_bitvector_simplify/main.c

@@ -0,0 +1,20 @@
+// Test case for issue #2689
+// This test verifies that goto-instrument can analyze binaries
+// generated by goto-analyzer --simplify without assertion failures
+// in local_bitvector_analysis.cpp
+
+int array[10];
+
+int main()
+{
+  int *p = array;
+  // Pointer arithmetic that may be simplified in various ways
+  int *q = p + 1 + 2;     // This could be simplified to p + 3
+  int *r = p + 1 + 2 + 3; // Multiple additions
+
+  // Access through computed pointer
+  *q = 42;
+  *r = 43;
+
+  return 0;
+}

regression/goto-instrument/local_bitvector_simplify/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--show-local-bitvector-analysis
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

src/analyses/local_bitvector_analysis.cpp

@@ -173,10 +173,27 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get_rec(
 
     if(plus_expr.operands().size() >= 3)
     {
-      DATA_INVARIANT(
-        plus_expr.op0().type().id() == ID_pointer,
-        "pointer in pointer-typed sum must be op0");
-      return get_rec(plus_expr.op0(), loc_info_src) | flagst::mk_uses_offset();
+      // In pointer arithmetic with 3+ operands, typically the pointer is op0,
+      // but simplification may reorder operands. Search for the pointer
+      // operand.
+      if(plus_expr.op0().type().id() == ID_pointer)
+      {
+        return get_rec(plus_expr.op0(), loc_info_src) |
+               flagst::mk_uses_offset();
+      }
+      else
+      {
+        // Search for pointer operand in remaining operands
+        for(const auto &op : plus_expr.operands())
+        {
+          if(op.type().id() == ID_pointer)
+          {
+            return get_rec(op, loc_info_src) | flagst::mk_uses_offset();
+          }
+        }
+        // No pointer operand found
+        return flagst::mk_unknown();
+      }
     }
     else if(plus_expr.operands().size() == 2)
     {