Fix unsound query in path-sensitivity functor

src/analyses/mCP.ml

@@ -468,6 +468,7 @@ struct
         ; assign = (fun ?name _ -> failwith "Cannot \"assign\" in query context.")
         }
       in
+      (* meet results so that precision from all analyses is combined *)
       Queries.Result.meet a @@ S.query ctx' q
     in
     match q with

src/framework/constraints.ml

@@ -1034,7 +1034,8 @@ struct
     fold' ctx Spec.sync identity (fun (a,b) (a',b') -> D.add a' a, b'@b) (D.empty (), [])
 
   let query ctx q =
-    fold' ctx Spec.query identity (fun x f -> Queries.Result.meet x (f q)) `Top
+    (* join results so that they are sound for all paths *)
+    fold' ctx Spec.query identity (fun x f -> Queries.Result.join x (f q)) `Bot
 
   let enter ctx l f a =
     let g xs ys = (List.map (fun (x,y) -> D.singleton x, D.singleton y) ys) @ xs in

src/witness/witnessConstraints.ml

@@ -403,7 +403,8 @@ struct
         ) (fst ctx.local);
       `Bot
     | _ ->
-      fold' ctx Spec.query identity (fun x _ f -> Queries.Result.meet x (f q)) `Top
+      (* join results so that they are sound for all paths *)
+      fold' ctx Spec.query identity (fun x _ f -> Queries.Result.join x (f q)) `Bot
 
   let should_inline f =
     (* (* inline __VERIFIER_error because Control requires the corresponding FunctionEntry node *)

tests/regression/01-cpa/46-funptr_path.c

@@ -0,0 +1,30 @@
+extern int __VERIFIER_nondet_int();
+
+#include <assert.h>
+#include <pthread.h>
+
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+
+void fun1() {
+  assert(0); // FAIL
+}
+
+void fun2() {
+  assert(0); // FAIL
+}
+
+int main() {
+  int x = __VERIFIER_nondet_int();
+
+  void (*fp)();
+
+  if (x) {
+    pthread_mutex_lock(&mutex);
+    fp = fun1;
+  }
+  else {
+    fp = fun2;
+  }
+
+  fp();
+}