Fix spurious overflow in pointer subtraction

src/analyses/base.ml

@@ -345,7 +345,10 @@ struct
       (* Pointer subtracted by a value (e-i) is very similar *)
       (* Cast n to the (signed) ptrdiff_ikind, then add the its negated value. *)
       | MinusPI ->
-        let n = ID.neg (ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) n) in (* TODO: proper castkind *)
+        let n = (* only speculative during ID.neg *)
+          let@ () = GobRef.wrap AnalysisState.executing_speculative_computations true in
+          ID.neg (ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) n) (* TODO: proper castkind *)
+        in
         Address (ad_concat_map (addToAddr n) p)
       | Mod -> Int (ID.top_of (Cilfacade.ptrdiff_ikind ())) (* we assume that address is actually casted to int first*)
       | _ -> Address AD.top_ptr

tests/regression/39-signed-overflows/16-ptr-minus-speculating.c

@@ -0,0 +1,8 @@
+// PARAM: --enable ana.int.interval
+
+int main() {
+  void *p;
+  long long i;
+  void *q = p - i; // NOWARN (signed integer overflow in unary -)
+  return 0;
+}