Give diagnostic in default mode when a root function has call with false precondition and unknown path cond

checker/src/body_visitor.rs

@@ -1614,15 +1614,15 @@ impl<'analysis, 'compilation, 'tcx> BodyVisitor<'analysis, 'compilation, 'tcx> {
             if cond_as_bool.unwrap_or(false)
                 || self.current_environment.entry_condition.implies(cond_val)
             {
-                return (Some(true), None);
+                return (Some(true), entry_cond_as_bool);
             }
             if !cond_as_bool.unwrap_or(true)
                 || self
                     .current_environment
                     .entry_condition
                     .implies_not(cond_val)
             {
-                return (Some(false), None);
+                return (Some(false), entry_cond_as_bool);
             }
             // The abstract domains are unable to decide if the entry condition is always true.
             // (If it could decide that the condition is always false, we wouldn't be here.)

checker/src/call_visitor.rs

@@ -2651,10 +2651,14 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx>
             let warn;
             if !refined_precondition_as_bool.unwrap_or(true) {
                 // The precondition is definitely false.
-                if entry_cond_as_bool.unwrap_or(false)
-                    && self.block_visitor.bv.function_being_analyzed_is_root()
-                {
-                    // We always get to this call and we are at the analysis root
+                if !entry_cond_as_bool.unwrap_or(true) {
+                    // The call is unreachable, so the precondition does not matter
+                    continue;
+                }
+                if self.block_visitor.bv.function_being_analyzed_is_root() {
+                    // This diagnostic says that the precondition is false and since
+                    // we know for certain that it will be false, should this call be reached,
+                    // it seems appropriate to issue an error message rather than a warning.
                     self.issue_diagnostic_for_call(precondition, &refined_condition, false);
                     return;
                 } else {

checker/tests/run-pass/false_precon.rs

@@ -0,0 +1,29 @@
+// Copyright (c) Facebook, Inc. and its affiliates.
+//
+// This source code is licensed under the MIT license found in the
+// LICENSE file in the root directory of this source tree.
+//
+
+// MIRAI_FLAGS --diag=default
+
+// A test that calls a function with a false precondition unconditionally from an analysis root
+
+#![cfg_attr(mirai, allow(incomplete_features), feature(generic_const_exprs))]
+
+use mirai_annotations::*;
+
+struct SecretTaintKind<const MASK: TagPropagationSet> {}
+const MASK: TagPropagationSet = TAG_PROPAGATION_ALL;
+type SecretTaint = SecretTaintKind<MASK>;
+
+fn foo(v: &Vec<i32>) {
+    // This precondition should never be true.
+    precondition!(does_not_have_tag!(&v[0], SecretTaint) && has_tag!(&v[0], SecretTaint));
+    //~ related location
+}
+
+pub fn main() {
+    let v = vec![1, 2, 3];
+    add_tag!(&v, SecretTaint);
+    foo(&v); //~ unsatisfied precondition
+}