================
@@ -6177,6 +6212,102 @@ TEST(TransferTest, ConditionalOperatorLocation) {
});
}
+TEST(TransferTest, ConditionalOperatorValuesTested) {
+ // Even though the LHS and the RHS of the conditional operator have different
+ // StorageLocations, we get constraints from the condition that the values
+ // must be equal to B1 for JoinDifferentIsB1, or B2 for JoinDifferentIsB2.
+ std::string Code = R"(
+ void target(bool B1, bool B2) {
+ bool JoinDifferentIsB1 = (B1 == B2) ? B2 : B1;
+ bool JoinDifferentIsB2 = (B1 == B2) ? B1 : B2;
+ // [[p]]
+ }
+ )";
+ runDataflow(
+ Code,
+ [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
+ ASTContext &ASTCtx) {
+ Environment Env = getEnvironmentAtAnnotation(Results, "p").fork();
+
+ auto &B1 = getValueForDecl<BoolValue>(ASTCtx, Env, "B1");
+ auto &B2 = getValueForDecl<BoolValue>(ASTCtx, Env, "B2");
+ auto &JoinDifferentIsB1 =
+ getValueForDecl<BoolValue>(ASTCtx, Env, "JoinDifferentIsB1");
+ auto &JoinDifferentIsB2 =
+ getValueForDecl<BoolValue>(ASTCtx, Env, "JoinDifferentIsB2");
+
+ const Formula &JoinDifferentIsB1EqB1 =
+ Env.arena().makeEquals(JoinDifferentIsB1.formula(), B1.formula());
+ EXPECT_TRUE(Env.allows(JoinDifferentIsB1EqB1));
+ EXPECT_TRUE(Env.proves(JoinDifferentIsB1EqB1));
----------------
ymand wrote:
why both? If "proves" is true, then "allows" is definitely true.
https://github.com/llvm/llvm-project/pull/168994
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
