Lines Matching full:env
143 const Formula &getFormula(const ValueDecl &D, const Environment &Env) {
144 return cast<BoolValue>(Env.getValue(D))->formula();
198 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
203 EXPECT_EQ(Env.getStorageLocation(*FooDecl), nullptr);
221 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
226 const StorageLocation *FooLoc = Env.getStorageLocation(*FooDecl);
229 const Value *FooVal = Env.getValue(*FooLoc);
246 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
251 const StorageLocation *FooLoc = Env.getStorageLocation(*FooDecl);
254 const Value *FooVal = Env.getValue(*FooLoc);
273 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
277 auto *FooValue = dyn_cast_or_null<PointerValue>(Env.getValue(*FooDecl));
309 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
328 cast<RecordStorageLocation>(Env.getStorageLocation(*FooDecl));
332 EXPECT_EQ(Env.getValue(UnmodeledXLoc), nullptr);
336 EXPECT_THAT(Env.getValue(*ZabDecl), NotNull());
357 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
376 cast<RecordStorageLocation>(Env.getStorageLocation(*FooDecl));
377 EXPECT_TRUE(isa<IntegerValue>(getFieldValue(FooLoc, *BarDecl, Env)));
400 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
419 cast<RecordStorageLocation>(Env.getStorageLocation(*FooDecl));
420 EXPECT_TRUE(isa<IntegerValue>(getFieldValue(FooLoc, *BarDecl, Env)));
437 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
442 ASSERT_THAT(Env.getValue(*ArrayDecl), IsNull());
464 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
483 cast<RecordStorageLocation>(Env.getStorageLocation(*FooDecl));
484 EXPECT_TRUE(isa<IntegerValue>(getFieldValue(FooLoc, *BarDecl, Env)));
504 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
509 const StorageLocation *FooLoc = Env.getStorageLocation(*FooDecl);
546 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
594 *cast<RecordStorageLocation>(Env.getStorageLocation(*FooDecl));
601 EXPECT_EQ(Env.getValue(*cast<RecordStorageLocation>(
607 *cast<PointerValue>(getFieldValue(&BarLoc, *FooPtrDecl, Env));
610 EXPECT_EQ(Env.getValue(*cast<RecordStorageLocation>(
615 EXPECT_TRUE(isa<PointerValue>(getFieldValue(&BarLoc, *BazPtrDecl, Env)));
635 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
640 const StorageLocation *FooLoc = Env.getStorageLocation(*FooDecl);
643 const PointerValue *FooVal = cast<PointerValue>(Env.getValue(*FooLoc));
682 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
742 *cast<ScalarStorageLocation>(Env.getStorageLocation(*FooDecl));
743 const auto &FooVal = *cast<PointerValue>(Env.getValue(FooLoc));
748 *cast<PointerValue>(getFieldValue(&FooPointeeLoc, *BarDecl, Env));
753 getFieldValue(&BarPointeeLoc, *FooPtrDecl, Env));
756 EXPECT_EQ(Env.getValue(*FooPtrPointeeLoc.getChild(*BarDecl)), nullptr);
759 isa<PointerValue>(getFieldValue(&BarPointeeLoc, *BazPtrDecl, Env)));
777 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
780 auto *ThisLoc = Env.getThisPointeeStorageLocation();
798 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
806 const StorageLocation *FooLoc = Env.getStorageLocation(*FooDecl);
809 const StorageLocation *BarLoc = Env.getStorageLocation(*BarDecl);
812 const Value *FooVal = Env.getValue(*FooLoc);
815 const Value *BarVal = Env.getValue(*BarLoc);
888 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
893 const Value *FooVal = Env.getValue(*FooDecl);
899 EXPECT_EQ(Env.getValue(*BarDecl), FooVal);
941 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
946 const Value *FooVal = Env.getValue(*FooDecl);
952 EXPECT_EQ(Env.getValue(*BarDecl), FooVal);
970 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
975 const Value *FooVal = Env.getValue(*FooDecl);
984 EXPECT_EQ(Env.getValue(*BarDecl), FooVal);
985 EXPECT_EQ(Env.getValue(*BazDecl), FooVal);
1004 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
1009 const Value *FooVal = Env.getValue(*FooDecl);
1015 const auto *BarVal = cast<PointerValue>(Env.getValue(*BarDecl));
1016 EXPECT_EQ(Env.getValue(BarVal->getPointeeLoc()), FooVal);
1021 EXPECT_EQ(Env.getValue(*BazDecl), FooVal);
1088 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
1093 const StorageLocation *FooLoc = Env.getStorageLocation(*FooDecl);
1096 const Value *FooVal = Env.getValue(*FooLoc);
1102 const StorageLocation *BarLoc = Env.getStorageLocation(*BarDecl);
1105 const Value *BarVal = Env.getValue(*BarLoc);
1126 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
1145 cast<RecordStorageLocation>(Env.getStorageLocation(*FooDecl));
1146 EXPECT_TRUE(isa<IntegerValue>(getFieldValue(FooLoc, *BarDecl, Env)));
1164 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
1169 const StorageLocation *FooLoc = Env.getStorageLocation(*FooDecl);
1188 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
1193 const StorageLocation *FooLoc = Env.getStorageLocation(*FooDecl);
1196 const PointerValue *FooVal = cast<PointerValue>(Env.getValue(*FooLoc));
1218 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
1237 cast<RecordStorageLocation>(Env.getStorageLocation(*FooDecl));
1239 cast<IntegerValue>(getFieldValue(FooLoc, *BarDecl, Env));
1244 EXPECT_EQ(Env.getValue(*BazDecl), BarVal);
1313 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
1368 isa<RecordStorageLocation>(Env.getStorageLocation(*FooDecl)));
1376 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
1399 *cast<RecordStorageLocation>(Env.getStorageLocation(*FooDecl));
1400 EXPECT_NE(Env.getValue(*FooLoc.getChild(*BarDecl)), nullptr);
1458 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
1477 cast<RecordStorageLocation>(Env.getStorageLocation(*FooDecl));
1479 cast<IntegerValue>(getFieldValue(FooLoc, *BarDecl, Env));
1484 EXPECT_EQ(Env.getValue(*BazDecl), BarVal);
1550 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
1551 EXPECT_EQ(getFieldValue(Env.getThisPointeeStorageLocation(), "Val",
1552 ASTCtx, Env),
1580 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
1583 EXPECT_NE(getFieldValue(Env.getThisPointeeStorageLocation(), "BaseVal",
1584 ASTCtx, Env),
1586 EXPECT_EQ(getFieldValue(Env.getThisPointeeStorageLocation(), "Val",
1587 ASTCtx, Env),
1635 const Environment &Env =
1637 auto &SLoc = getLocForDecl<RecordStorageLocation>(ASTCtx, Env, "s");
1683 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
1684 auto &SLoc = getLocForDecl<RecordStorageLocation>(ASTCtx, Env, "s");
1725 const Environment &Env =
1729 auto &MDLoc = getLocForDecl<RecordStorageLocation>(ASTCtx, Env, "MD");
1765 const Environment &Env =
1770 auto &MD = getLocForDecl<RecordStorageLocation>(ASTCtx, Env, "MD");
1772 getFieldValue(&MD, *findValueDecl(ASTCtx, "base1"), Env)),
1775 getFieldValue(&MD, *findValueDecl(ASTCtx, "intermediate"), Env)),
1778 getFieldValue(&MD, *findValueDecl(ASTCtx, "base2"), Env)),
1781 getFieldValue(&MD, *findValueDecl(ASTCtx, "most_derived"), Env)),
1802 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
1821 cast<RecordStorageLocation>(Env.getStorageLocation(*FooDecl));
1823 cast<IntegerValue>(getFieldValue(FooLoc, *BarDecl, Env));
1828 EXPECT_EQ(Env.getValue(*BazDecl), BarReferentVal);
1855 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
1857 const auto *ThisLoc = Env.getThisPointeeStorageLocation();
1867 const Value *BarVal = Env.getValue(*BarLoc);
1872 EXPECT_EQ(Env.getValue(*FooDecl), BarVal);
1894 cast<IntegerValue>(getFieldValue(QuxLoc, *BazDecl, Env));
1898 EXPECT_EQ(Env.getValue(*QuuxDecl), BazVal);
1926 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
1928 const auto *ThisLoc = Env.getThisPointeeStorageLocation();
1937 const Value *BarVal = Env.getValue(*BarLoc);
1942 EXPECT_EQ(Env.getValue(*FooDecl), BarVal);
1964 cast<IntegerValue>(getFieldValue(QuxLoc, *BazDecl, Env));
1968 EXPECT_EQ(Env.getValue(*QuuxDecl), BazVal);
1992 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
1994 const auto *ThisLoc = Env.getThisPointeeStorageLocation();
2004 const Value *FooVal = Env.getValue(*FooLoc);
2014 const Value *BarVal = Env.getValue(*BarLoc);
2037 const Environment &Env = getEnvironmentAtAnnotation(Results, "p1");
2039 const auto *ThisLoc = Env.getThisPointeeStorageLocation();
2049 const Value *BarVal = Env.getValue(*BarLoc);
2054 EXPECT_EQ(Env.getValue(*FooDecl), BarVal);
2075 const Environment &Env = getEnvironmentAtAnnotation(Results, "p2");
2077 const auto *ThisLoc = Env.getThisPointeeStorageLocation();
2087 const Value *BarVal = Env.getValue(*BarLoc);
2092 EXPECT_EQ(Env.getValue(*FooDecl), BarVal);
2110 const Environment &Env = getEnvironmentAtAnnotation(Results, "p3");
2112 EXPECT_THAT(Env.getThisPointeeStorageLocation(), IsNull());
2133 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
2135 const auto *ThisLoc = Env.getThisPointeeStorageLocation();
2141 const auto *FooVal = cast<IntegerValue>(Env.getValue(*FooDecl));
2145 EXPECT_EQ(Env.getValue(*QuxDecl), FooVal);
2166 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
2168 const auto *ThisLoc = Env.getThisPointeeStorageLocation();
2174 const auto *FooVal = cast<IntegerValue>(Env.getValue(*FooDecl));
2178 EXPECT_EQ(Env.getValue(*QuxDecl), FooVal);
2199 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
2201 const auto *ThisLoc = Env.getThisPointeeStorageLocation();
2207 const auto *FooLoc = Env.getStorageLocation(*FooDecl);
2212 const auto *QuxLoc = Env.getStorageLocation(*QuxDecl);
2234 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
2243 cast<RecordStorageLocation>(Env.getStorageLocation(*FooDecl));
2244 EXPECT_TRUE(isa<IntegerValue>(getFieldValue(FooLoc, *BarDecl, Env)));
2267 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
2276 cast<RecordStorageLocation>(Env.getStorageLocation(*FooDecl));
2277 EXPECT_TRUE(isa<IntegerValue>(getFieldValue(FooLoc, *BarDecl, Env)));
2387 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
2391 getLocForDecl<RecordStorageLocation>(ASTCtx, Env, "Foo");
2393 getLocForDecl<RecordStorageLocation>(ASTCtx, Env, "Bar");
2396 cast<IntegerValue>(getFieldValue(&FooLoc, *BazDecl, Env));
2398 cast<IntegerValue>(getFieldValue(&BarLoc, *BazDecl, Env));
2600 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
2601 const auto &FooVal = getValueForDecl<BoolValue>(ASTCtx, Env, "Foo");
2642 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
2645 *Env.getThisPointeeStorageLocation(), "F", ASTCtx);
2646 auto *AVal = cast<PointerValue>(getFieldValue(&FLoc, "a", ASTCtx, Env));
2647 EXPECT_EQ(AVal, &getValueForDecl<PointerValue>(ASTCtx, Env, "null"));
2648 EXPECT_EQ(getFieldValue(&FLoc, "b", ASTCtx, Env), nullptr);
2677 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
2680 *Env.getThisPointeeStorageLocation(), "F", ASTCtx);
2681 auto *AVal = cast<PointerValue>(getFieldValue(&FLoc, "a", ASTCtx, Env));
2682 EXPECT_EQ(AVal, &getValueForDecl<PointerValue>(ASTCtx, Env, "null"));
2683 EXPECT_EQ(getFieldValue(&FLoc, "b", ASTCtx, Env), nullptr);
2707 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
2710 *Env.getThisPointeeStorageLocation(), "F", ASTCtx);
2711 auto *AVal = cast<PointerValue>(getFieldValue(&FLoc, "a", ASTCtx, Env));
2713 &getValueForDecl<PointerValue>(ASTCtx, Env, "NullIntPtr"));
2714 auto *BVal = cast<PointerValue>(getFieldValue(&FLoc, "b", ASTCtx, Env));
2716 &getValueForDecl<PointerValue>(ASTCtx, Env, "NullBoolPtr"));
2749 const Environment &Env =
2753 cast<RecordStorageLocation>(Env.getStorageLocation(*FooDecl));
2755 cast<RecordStorageLocation>(Env.getStorageLocation(*BarDecl));
2758 EXPECT_TRUE(recordsEqual(*FooLoc, *BarLoc, Env));
2762 cast<IntegerValue>(getFieldValue(FooLoc, *BazDecl, Env));
2764 cast<IntegerValue>(getFieldValue(BarLoc, *BazDecl, Env));
2770 const Environment &Env =
2774 cast<RecordStorageLocation>(Env.getStorageLocation(*FooDecl));
2776 cast<RecordStorageLocation>(Env.getStorageLocation(*BarDecl));
2778 EXPECT_FALSE(recordsEqual(*FooLoc, *BarLoc, Env));
2781 cast<IntegerValue>(getFieldValue(FooLoc, *BazDecl, Env));
2783 cast<IntegerValue>(getFieldValue(BarLoc, *BazDecl, Env));
2809 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
2821 cast<RecordStorageLocation>(Env.getStorageLocation(*FooDecl));
2823 cast<RecordStorageLocation>(Env.getStorageLocation(*BarDecl));
2824 EXPECT_TRUE(recordsEqual(*FooLoc, *BarLoc, Env));
2827 cast<IntegerValue>(getFieldValue(FooLoc, *BazDecl, Env));
2829 cast<IntegerValue>(getFieldValue(BarLoc, *BazDecl, Env));
2852 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
2864 cast<RecordStorageLocation>(Env.getStorageLocation(*FooDecl));
2866 cast<RecordStorageLocation>(Env.getStorageLocation(*BarDecl));
2867 EXPECT_TRUE(recordsEqual(*FooLoc, *BarLoc, Env));
2870 cast<IntegerValue>(getFieldValue(FooLoc, *BazDecl, Env));
2872 cast<IntegerValue>(getFieldValue(BarLoc, *BazDecl, Env));
2893 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
2898 getLocForDecl<RecordStorageLocation>(ASTCtx, Env, "Foo");
2900 getLocForDecl<RecordStorageLocation>(ASTCtx, Env, "Bar");
2903 cast<IntegerValue>(getFieldValue(&FooLoc, *BazDecl, Env));
2905 cast<IntegerValue>(getFieldValue(&BarLoc, *BazDecl, Env));
3012 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
3024 *cast<RecordStorageLocation>(Env.getStorageLocation(*FooDecl));
3025 const auto *BarVal = cast<IntegerValue>(Env.getValue(*BarDecl));
3026 EXPECT_EQ(BarVal, getFieldValue(&FooLoc, *BazDecl, Env));
3055 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
3059 // `Env.getResultObjectLocation()` should return the same location for
3082 RecordStorageLocation &Loc = Env.getResultObjectLocation(*TOE);
3083 EXPECT_EQ(&Loc, &Env.getResultObjectLocation(*Comma));
3084 EXPECT_EQ(&Loc, &Env.getResultObjectLocation(*EWC));
3085 EXPECT_EQ(&Loc, &Env.getResultObjectLocation(*BTE));
3110 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
3119 Env.getResultObjectLocation(*DefaultArg);
3142 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
3153 RecordStorageLocation &Loc = Env.getResultObjectLocation(*DefaultInit);
3155 EXPECT_EQ(&Loc, Env.getThisPointeeStorageLocation()->getChild(*SField));
3182 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
3188 EXPECT_NE(&Env.getResultObjectLocation(*CallExpr), nullptr);
3213 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
3222 &Env.getResultObjectLocation(*Construct),
3223 &getFieldLoc(getLocForDecl<RecordStorageLocation>(ASTCtx, Env, "O"),
3249 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
3258 &Env.getResultObjectLocation(*Construct),
3259 &getFieldLoc(getLocForDecl<RecordStorageLocation>(ASTCtx, Env, "O"),
3304 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
3311 &Env.getResultObjectLocation(*Spaceship),
3312 &getLocForDecl<RecordStorageLocation>(ASTCtx, Env, "ordering"));
3337 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
3344 EXPECT_EQ(&Env.getResultObjectLocation(*StdInitList),
3345 &getLocForDecl<RecordStorageLocation>(ASTCtx, Env, "list"));
3365 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
3370 EXPECT_EQ(&Env.getResultObjectLocation(*Construct),
3371 &getLocForDecl<RecordStorageLocation>(ASTCtx, Env, "s"));
3391 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
3396 EXPECT_EQ(&Env.getResultObjectLocation(*BuiltinBitCast),
3397 &getLocForDecl<RecordStorageLocation>(ASTCtx, Env, "s"));
3417 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
3422 EXPECT_EQ(&Env.getResultObjectLocation(*Atomic),
3423 &getLocForDecl<RecordStorageLocation>(ASTCtx, Env, "s"));
3449 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
3462 auto &ALoc = getLocForDecl<StorageLocation>(ASTCtx, Env, "a");
3463 EXPECT_EQ(&Env.getResultObjectLocation(*ConstructExpr0), &ALoc);
3464 EXPECT_EQ(&Env.getResultObjectLocation(*ConstructExpr1), &ALoc);
3556 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
3564 const auto *FooVal = Env.getValue(*FooDecl);
3565 const auto *BarVal = Env.getValue(*BarDecl);
3583 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
3585 const auto &FooVal = getValueForDecl<IntegerValue>(ASTCtx, Env, "Foo");
3586 const auto &BarVal = getValueForDecl<IntegerValue>(ASTCtx, Env, "Bar");
3602 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
3604 const auto &FooVal = getValueForDecl(ASTCtx, Env, "Foo");
3605 const auto &BarVal = getValueForDecl(ASTCtx, Env, "Bar");
3623 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
3625 const auto &FooVal = getValueForDecl<BoolValue>(ASTCtx, Env, "Foo");
3626 const auto &BarVal = getValueForDecl<BoolValue>(ASTCtx, Env, "Bar");
3673 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
3690 const auto *FooXVal = cast<PointerValue>(Env.getValue(*FooXDecl));
3691 const auto *FooYVal = cast<PointerValue>(Env.getValue(*FooYDecl));
3692 const auto *BarVal = cast<PointerValue>(Env.getValue(*BarDecl));
3693 const auto *BazVal = cast<PointerValue>(Env.getValue(*BazDecl));
3694 const auto *NullVal = cast<PointerValue>(Env.getValue(*NullDecl));
3703 EXPECT_THAT(Env.getValue(FooPointeeLoc), IsNull());
3707 EXPECT_THAT(Env.getValue(BarPointeeLoc), IsNull());
3711 EXPECT_EQ(BazVal, &Env.fork().getOrCreateNullPointerValue(
3716 EXPECT_THAT(Env.getValue(NullPointeeLoc), IsNull());
3734 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
3739 ASSERT_THAT(Env.getValue(*MemberPointerDecl), IsNull());
3757 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
3762 ASSERT_THAT(Env.getValue(*MemberPointerDecl), IsNull());
3779 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
3784 ASSERT_THAT(Env.getValue(*MemberPointerDecl), IsNull());
3801 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
3810 cast<ScalarStorageLocation>(Env.getStorageLocation(*FooDecl));
3811 const auto *BarVal = cast<PointerValue>(Env.getValue(*BarDecl));
3828 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
3836 const auto *FooVal = cast<PointerValue>(Env.getValue(*FooDecl));
3837 const auto *BarVal = cast<PointerValue>(Env.getValue(*BarDecl));
3906 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
3908 EXPECT_EQ(&getLocForDecl(ASTCtx, Env, "IRef"),
3909 &getLocForDecl(ASTCtx, Env, "I"));
3952 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
3955 &getLocForDecl<RecordStorageLocation>(ASTCtx, Env, "Foo"), "i",
3956 ASTCtx, Env));
3958 &getLocForDecl<RecordStorageLocation>(ASTCtx, Env, "Bar"), "i",
3959 ASTCtx, Env));
3961 &getLocForDecl<RecordStorageLocation>(ASTCtx, Env, "Baz"), "i",
3962 ASTCtx, Env));
4066 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
4092 const auto *FooArgVal = cast<IntegerValue>(Env.getValue(*FooArgDecl));
4093 const auto *BarArgVal = cast<IntegerValue>(Env.getValue(*BarArgDecl));
4094 const auto *QuxArgVal = cast<IntegerValue>(Env.getValue(*QuxArgDecl));
4097 *cast<RecordStorageLocation>(Env.getStorageLocation(*QuuxDecl));
4101 EXPECT_EQ(getFieldValue(&QuuxLoc, *BarDecl, Env), BarArgVal);
4102 EXPECT_EQ(getFieldValue(&BazLoc, *FooDecl, Env), FooArgVal);
4103 EXPECT_EQ(getFieldValue(&QuuxLoc, *QuxDecl, Env), QuxArgVal);
4108 getLocForDecl<RecordStorageLocation>(ASTCtx, Env, "OtherB");
4131 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
4135 auto &ILoc = getLocForDecl<StorageLocation>(ASTCtx, Env, "i");
4136 auto &SLoc = getLocForDecl<RecordStorageLocation>(ASTCtx, Env, "s");
4158 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
4163 auto &SLoc = getLocForDecl<RecordStorageLocation>(ASTCtx, Env, "s");
4165 auto &IValue = getValueForDecl<IntegerValue>(ASTCtx, Env, "i");
4167 *cast<IntegerValue>(getFieldValue(&SLoc, *I1FieldDecl, Env));
4170 *cast<IntegerValue>(getFieldValue(&SLoc, *I2FieldDecl, Env));
4212 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
4230 Env.getStorageLocation(*BazDecl));
4234 cast<IntegerValue>(getFieldValue(BazLoc, *FooDecl, Env));
4238 const auto *BarLoc = Env.getStorageLocation(*BarDecl);
4241 EXPECT_EQ(Env.getValue(*BarLoc), FooVal);
4258 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
4264 dyn_cast_or_null<BoolValue>(Env.getValue(*FooDecl));
4271 dyn_cast_or_null<BoolValue>(Env.getValue(*BarDecl));
4274 EXPECT_EQ(FooVal, &Env.getBoolLiteralValue(true));
4275 EXPECT_EQ(BarVal, &Env.getBoolLiteralValue(false));
4292 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
4298 dyn_cast_or_null<BoolValue>(Env.getValue(*FooDecl));
4305 dyn_cast_or_null<BoolValue>(Env.getValue(*BarDecl));
4312 dyn_cast_or_null<BoolValue>(Env.getValue(*QuxDecl));
4319 dyn_cast_or_null<BoolValue>(Env.getValue(*BazDecl));
4321 auto &A = Env.arena();
4340 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
4346 dyn_cast_or_null<BoolValue>(Env.getValue(*FooDecl));
4353 dyn_cast_or_null<BoolValue>(Env.getValue(*BarDecl));
4360 dyn_cast_or_null<BoolValue>(Env.getValue(*QuxDecl));
4367 dyn_cast_or_null<BoolValue>(Env.getValue(*BazDecl));
4369 auto &A = Env.arena();
4388 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
4393 const auto *AVal = dyn_cast_or_null<BoolValue>(Env.getValue(*ADecl));
4399 const auto *BVal = dyn_cast_or_null<BoolValue>(Env.getValue(*BDecl));
4405 const auto *CVal = dyn_cast_or_null<BoolValue>(Env.getValue(*CDecl));
4411 const auto *DVal = dyn_cast_or_null<BoolValue>(Env.getValue(*DDecl));
4418 dyn_cast_or_null<BoolValue>(Env.getValue(*FooDecl));
4420 auto &A = Env.arena();
4443 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
4449 dyn_cast_or_null<BoolValue>(Env.getValue(*FooDecl));
4456 dyn_cast_or_null<BoolValue>(Env.getValue(*BarDecl));
4458 auto &A = Env.arena();
4475 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
4483 EXPECT_EQ(Env.getValue(*FooDecl), Env.getValue(*BarDecl));
4502 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
4510 EXPECT_EQ(Env.getValue(*FooDecl), Env.getValue(*BarDecl));
4531 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
4542 EXPECT_EQ(Env.getValue(*FooDecl), Env.getValue(*BarDecl));
4563 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
4573 EXPECT_EQ(Env.getValue(*FooDecl), Env.getValue(*BarDecl));
4594 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
4603 EXPECT_NE(Env.getValue(*FooDecl), Env.getValue(*BarDecl));
4619 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
4624 const StorageLocation *FooLoc = Env.getStorageLocation(*FooDecl);
4627 const Value *FooVal = Env.getValue(*FooLoc);
4645 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
4653 const StorageLocation *FooLoc = Env.getStorageLocation(*FooDecl);
4656 const StorageLocation *BarLoc = Env.getStorageLocation(*BarDecl);
4659 const Value *FooVal = Env.getValue(*FooLoc);
4662 const Value *BarVal = Env.getValue(*BarLoc);
4684 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
4692 const Value *BarVal = cast<IntegerValue>(Env.getValue(*BarDecl));
4693 const Value *BazVal = cast<IntegerValue>(Env.getValue(*BazDecl));
4715 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
4723 const Value *BarVal = cast<IntegerValue>(Env.getValue(*BarDecl));
4724 const Value *BazVal = cast<IntegerValue>(Env.getValue(*BazDecl));
4746 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
4754 const Value *BarVal = cast<IntegerValue>(Env.getValue(*BarDecl));
4755 const Value *BazVal = cast<IntegerValue>(Env.getValue(*BazDecl));
4780 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
4794 const auto *BarVal = cast<IntegerValue>(Env.getValue(*BarDecl));
4797 *cast<RecordStorageLocation>(Env.getStorageLocation(*A2Decl));
4798 EXPECT_EQ(getFieldValue(&A2Loc, *FooDecl, Env), BarVal);
4901 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
4905 EXPECT_NE(&getValueForDecl<PointerValue>(ASTCtx, Env, "p1"),
4906 &getValueForDecl<PointerValue>(ASTCtx, Env, "p2"));
4908 EXPECT_EQ(&getValueForDecl<BoolValue>(ASTCtx, Env, "p1_eq_p1"),
4909 &Env.getBoolLiteralValue(true));
4910 EXPECT_EQ(&getValueForDecl<BoolValue>(ASTCtx, Env, "p1_eq_p2"),
4911 &Env.getBoolLiteralValue(true));
4913 getValueForDecl<BoolValue>(ASTCtx, Env, "p1_eq_p_other")));
4916 getValueForDecl<BoolValue>(ASTCtx, Env, "p1_eq_null")));
4918 getValueForDecl<BoolValue>(ASTCtx, Env, "p1_eq_nullptr")));
4919 EXPECT_EQ(&getValueForDecl<BoolValue>(ASTCtx, Env, "null_eq_nullptr"),
4920 &Env.getBoolLiteralValue(true));
4922 &getValueForDecl<BoolValue>(ASTCtx, Env, "nullptr_eq_nullptr"),
4923 &Env.getBoolLiteralValue(true));
4925 EXPECT_EQ(&getValueForDecl<BoolValue>(ASTCtx, Env, "p1_ne_p1"),
4926 &Env.getBoolLiteralValue(false));
4947 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
4954 getValueForDecl<BoolValue>(ASTCtx, Env, "i1_eq_i2")));
4969 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
4972 getValueForDecl<BoolValue>(ASTCtx, Env, "equal").formula();
4973 EXPECT_TRUE(Env.proves(Equal));
5005 const Environment &Env = getEnvironmentAtAnnotation(Results, "p0");
5008 auto &BVal = getFormula(*BDecl, Env);
5010 EXPECT_TRUE(Env.proves(Env.arena().makeNot(BVal)));
5014 const Environment &Env = getEnvironmentAtAnnotation(Results, "p1");
5015 auto &CVal = getFormula(*CDecl, Env);
5016 EXPECT_TRUE(Env.proves(CVal));
5020 const Environment &Env = getEnvironmentAtAnnotation(Results, "p2");
5021 auto &CVal = getFormula(*CDecl, Env);
5022 EXPECT_TRUE(Env.proves(CVal));
5048 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
5053 auto &BarVal = getFormula(*BarDecl, Env);
5054 EXPECT_TRUE(Env.proves(Env.arena().makeNot(BarVal)));
5078 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
5085 auto &BarVal = getFormula(*BarDecl, Env);
5086 auto &ErrVal = getFormula(*ErrDecl, Env);
5087 EXPECT_TRUE(Env.proves(BarVal));
5091 EXPECT_FALSE(Env.proves(Env.arena().makeNot(ErrVal)));
5115 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
5120 auto &BarVal = getFormula(*BarDecl, Env);
5121 EXPECT_TRUE(Env.proves(Env.arena().makeNot(BarVal)));
5254 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
5255 auto &BVal = getValueForDecl<BoolValue>(ASTCtx, Env, "b");
5256 EXPECT_TRUE(Env.proves(Env.arena().makeNot(BVal.formula())));
5320 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
5337 const StorageLocation *FooRefLoc = Env.getStorageLocation(*FooRefDecl);
5340 const StorageLocation *BarRefLoc = Env.getStorageLocation(*BarRefDecl);
5343 const Value *QuxVal = Env.getValue(*QuxDecl);
5347 Env.getStorageLocation(*BoundFooRefDecl);
5351 Env.getStorageLocation(*BoundBarRefDecl);
5354 EXPECT_EQ(Env.getValue(*BoundFooRefDecl), QuxVal);
5379 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
5396 const StorageLocation *FooRefLoc = Env.getStorageLocation(*FooRefDecl);
5399 const StorageLocation *BarRefLoc = Env.getStorageLocation(*BarRefDecl);
5402 const Value *QuxVal = Env.getValue(*QuxDecl);
5406 Env.getStorageLocation(*BoundFooRefDecl);
5410 Env.getStorageLocation(*BoundBarRefDecl);
5413 EXPECT_EQ(Env.getValue(*BoundFooRefDecl), QuxVal);
5439 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
5456 const StorageLocation *FooRefLoc = Env.getStorageLocation(*FooRefDecl);
5459 const StorageLocation *BarRefLoc = Env.getStorageLocation(*BarRefDecl);
5462 const Value *QuxVal = Env.getValue(*QuxDecl);
5466 Env.getStorageLocation(*BoundFooDecl);
5470 Env.getStorageLocation(*BoundBarDecl);
5473 EXPECT_EQ(Env.getValue(*BoundFooDecl), QuxVal);
5652 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
5660 const StorageLocation *BarLoc = Env.getStorageLocation(*BarDecl);
5663 const StorageLocation *BazLoc = Env.getStorageLocation(*BazDecl);
5680 Environment Env = getEnvironmentAtAnnotation(Results, "p").fork();
5682 auto &B1 = getValueForDecl<BoolValue>(ASTCtx, Env, "B1");
5683 auto &B2 = getValueForDecl<BoolValue>(ASTCtx, Env, "B2");
5684 auto &JoinSame = getValueForDecl<BoolValue>(ASTCtx, Env, "JoinSame");
5686 getValueForDecl<BoolValue>(ASTCtx, Env, "JoinDifferent");
5691 Env.arena().makeEquals(JoinDifferent.formula(), B1.formula());
5692 EXPECT_TRUE(Env.allows(JoinDifferentEqB1));
5693 EXPECT_FALSE(Env.proves(JoinDifferentEqB1));
5696 Env.arena().makeEquals(JoinDifferent.formula(), B2.formula());
5697 EXPECT_TRUE(Env.allows(JoinDifferentEqB2));
5698 EXPECT_FALSE(Env.proves(JoinDifferentEqB1));
5714 Environment Env = getEnvironmentAtAnnotation(Results, "p").fork();
5716 StorageLocation &I1 = getLocForDecl(ASTCtx, Env, "I1");
5717 StorageLocation &I2 = getLocForDecl(ASTCtx, Env, "I2");
5718 StorageLocation &JoinSame = getLocForDecl(ASTCtx, Env, "JoinSame");
5720 getLocForDecl(ASTCtx, Env, "JoinDifferent");
5744 Environment Env = getEnvironmentAtAnnotation(Results, "p").fork();
5747 getValueForDecl<BoolValue>(ASTCtx, Env, "JoinTrueTrue");
5755 getValueForDecl<BoolValue>(ASTCtx, Env, "JoinTrueFalse");
5946 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
5951 auto &FooVal = getFormula(*FooDecl, Env);
5952 EXPECT_FALSE(Env.proves(FooVal));
5953 EXPECT_FALSE(Env.proves(Env.arena().makeNot(FooVal)));
5970 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
5975 auto *SLoc = Env.getStorageLocation(*SDecl);
5978 ASSERT_THAT(Env.getReturnStorageLocation(), Eq(SLoc));
5997 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
6002 auto *SLoc = Env.getStorageLocation(*SDecl);
6005 auto *Loc = Env.getReturnStorageLocation();
6035 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
6049 StorageLocation *S1Loc = Env.getStorageLocation(*S1);
6050 StorageLocation *S2Loc = Env.getStorageLocation(*S2);
6052 EXPECT_THAT(Env.getStorageLocation(*ReturnS1), Eq(S1Loc));
6053 EXPECT_THAT(Env.getStorageLocation(*ReturnS2), Eq(S2Loc));
6058 EXPECT_THAT(Env.getStorageLocation(*ReturnDontKnow), Ne(S1Loc));
6059 EXPECT_THAT(Env.getStorageLocation(*ReturnDontKnow), Ne(S2Loc));
6080 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
6085 auto &FooVal = getFormula(*FooDecl, Env);
6086 EXPECT_FALSE(Env.proves(FooVal));
6087 EXPECT_FALSE(Env.proves(Env.arena().makeNot(FooVal)));
6108 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
6113 auto &FooVal = getFormula(*FooDecl, Env);
6114 EXPECT_TRUE(Env.proves(FooVal));
6135 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
6140 auto &FooVal = getFormula(*FooDecl, Env);
6141 EXPECT_TRUE(Env.proves(Env.arena().makeNot(FooVal)));
6164 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
6165 auto &A = Env.arena();
6173 auto &FooVal = getFormula(*FooDecl, Env);
6174 EXPECT_TRUE(Env.proves(FooVal));
6175 EXPECT_FALSE(Env.proves(A.makeNot(FooVal)));
6177 auto &BarVal = getFormula(*BarDecl, Env);
6178 EXPECT_FALSE(Env.proves(BarVal));
6179 EXPECT_TRUE(Env.proves(A.makeNot(BarVal)));
6201 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
6206 auto &FooVal = getFormula(*FooDecl, Env);
6207 EXPECT_FALSE(Env.proves(FooVal));
6208 EXPECT_FALSE(Env.proves(Env.arena().makeNot(FooVal)));
6230 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
6235 auto &FooVal = getFormula(*FooDecl, Env);
6236 EXPECT_TRUE(Env.proves(FooVal));
6259 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
6264 auto &FooVal = getFormula(*FooDecl, Env);
6265 EXPECT_FALSE(Env.proves(FooVal));
6266 EXPECT_FALSE(Env.proves(Env.arena().makeNot(FooVal)));
6289 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
6294 auto &FooVal = getFormula(*FooDecl, Env);
6295 EXPECT_TRUE(Env.proves(FooVal));
6331 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
6336 auto &FooVal = getFormula(*FooDecl, Env);
6338 EXPECT_FALSE(Env.proves(FooVal));
6339 EXPECT_FALSE(Env.proves(Env.arena().makeNot(FooVal)));
6363 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
6371 auto &FooVal = getFormula(*FooDecl, Env);
6372 EXPECT_TRUE(Env.proves(FooVal));
6373 EXPECT_FALSE(Env.proves(Env.arena().makeNot(FooVal)));
6375 auto &BarVal = getFormula(*BarDecl, Env);
6376 EXPECT_FALSE(Env.proves(BarVal));
6377 EXPECT_TRUE(Env.proves(Env.arena().makeNot(BarVal)));
6405 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
6413 auto &BarVal = getFormula(*BarDecl, Env);
6414 EXPECT_FALSE(Env.proves(BarVal));
6415 EXPECT_TRUE(Env.proves(Env.arena().makeNot(BarVal)));
6417 auto &BazVal = getFormula(*BazDecl, Env);
6418 EXPECT_TRUE(Env.proves(BazVal));
6419 EXPECT_FALSE(Env.proves(Env.arena().makeNot(BazVal)));
6457 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
6462 auto &FooVal = getFormula(*FooDecl, Env);
6463 EXPECT_TRUE(Env.proves(FooVal));
6482 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
6487 auto &FooVal = getFormula(*FooDecl, Env);
6488 EXPECT_TRUE(Env.proves(Env.arena().makeNot(FooVal)));
6510 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
6515 auto &BazVal = getFormula(*BazDecl, Env);
6516 EXPECT_TRUE(Env.proves(BazVal));
6558 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
6561 getLocForDecl<RecordStorageLocation>(ASTCtx, Env, "FalseS");
6563 getLocForDecl<RecordStorageLocation>(ASTCtx, Env, "TrueS");
6565 EXPECT_EQ(getFieldValue(&FalseSLoc, "B", ASTCtx, Env),
6566 &Env.getBoolLiteralValue(false));
6567 EXPECT_EQ(getFieldValue(&TrueSLoc, "B", ASTCtx, Env),
6568 &Env.getBoolLiteralValue(true));
6594 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
6596 auto &MySLoc = getLocForDecl<RecordStorageLocation>(ASTCtx, Env, "MyS");
6599 cast<PointerValue>(getFieldValue(&MySLoc, "self", ASTCtx, Env));
6623 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
6628 auto &FooVal = getFormula(*FooDecl, Env);
6629 EXPECT_TRUE(Env.proves(FooVal));
6655 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
6660 auto &FooVal = getFormula(*FooDecl, Env);
6661 EXPECT_TRUE(Env.proves(FooVal));
6687 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
6692 auto &FooVal = getFormula(*FooDecl, Env);
6693 EXPECT_TRUE(Env.proves(FooVal));
6721 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
6726 auto &FooVal = getFormula(*FooDecl, Env);
6727 EXPECT_TRUE(Env.proves(FooVal));
6756 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
6761 auto &FooVal = getFormula(*FooDecl, Env);
6762 EXPECT_TRUE(Env.proves(FooVal));
6790 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
6795 auto &FooVal = getFormula(*FooDecl, Env);
6796 EXPECT_TRUE(Env.proves(FooVal));
6821 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
6826 auto &FooVal = getFormula(*FooDecl, Env);
6827 EXPECT_TRUE(Env.proves(FooVal));
6852 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
6857 auto &FooVal = getFormula(*FooDecl, Env);
6858 EXPECT_TRUE(Env.proves(FooVal));
6883 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
6888 auto &FooVal = getFormula(*FooDecl, Env);
6889 EXPECT_TRUE(Env.proves(FooVal));
6922 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
6923 auto &SelfVal = *cast<PointerValue>(Env.getValue(*SelfDecl));
6924 EXPECT_EQ(Env.getStorageLocation(*MyObjDecl), &SelfVal.getPointeeLoc());
6967 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
6968 auto &B = getValueForDecl<BoolValue>(ASTCtx, Env, "b").formula();
6969 EXPECT_TRUE(Env.proves(B));
7010 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
7011 auto &A = Env.arena();
7014 EXPECT_FALSE(Env.proves(A.makeLiteral(false)));
7016 auto &B1 = getValueForDecl<BoolValue>(ASTCtx, Env, "b1").formula();
7017 EXPECT_TRUE(Env.proves(A.makeNot(B1)));
7020 getValueForDecl<BoolValue>(ASTCtx, Env, "NoreturnOnRhsOfAnd").formula();
7021 EXPECT_TRUE(Env.proves(A.makeNot(NoreturnOnRhsOfAnd)));
7023 auto &B2 = getValueForDecl<BoolValue>(ASTCtx, Env, "b2").formula();
7024 EXPECT_TRUE(Env.proves(B2));
7027 getValueForDecl<BoolValue>(ASTCtx, Env, "NoreturnOnRhsOfOr")
7029 EXPECT_TRUE(Env.proves(NoreturnOnRhsOfOr));
7032 ASTCtx, Env, "NoreturnOnLhsMakesAndUnreachable").formula();
7033 EXPECT_TRUE(Env.proves(NoreturnOnLhsMakesAndUnreachable));
7036 ASTCtx, Env, "NoreturnOnLhsMakesOrUnreachable").formula();
7037 EXPECT_TRUE(Env.proves(NoreturnOnLhsMakesOrUnreachable));
7052 const Environment &Env =
7055 auto &P = getValueForDecl<PointerValue>(ASTCtx, Env, "p");
7057 EXPECT_THAT(Env.getValue(P.getPointeeLoc()), NotNull());
7083 const Environment &Env =
7089 auto &P = getValueForDecl<PointerValue>(ASTCtx, Env, "p");
7096 EXPECT_THAT(Env.getValue(InnerFieldLoc), NotNull());
7123 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
7126 getValueForDecl<PointerValue>(ASTCtx, Env, "non_member_p1");
7128 getValueForDecl<PointerValue>(ASTCtx, Env, "non_member_p2");
7132 getValueForDecl<PointerValue>(ASTCtx, Env, "member_p1");
7134 getValueForDecl<PointerValue>(ASTCtx, Env, "member_p2");
7158 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
7168 EXPECT_THAT(Env.getValue(*ImplicitCast), IsNull());
7200 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
7218 auto *Ptr1 = cast<PointerValue>(Env.getValue(*Call1->getCallee()));
7219 auto *Ptr2 = cast<PointerValue>(Env.getValue(*Call2->getCallee()));
7243 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
7249 auto *S = cast<RecordStorageLocation>(Env.getStorageLocation(*SDecl));
7253 auto *B = cast<BoolValue>(getFieldValue(&AnonStruct, *BDecl, Env));
7254 ASSERT_TRUE(Env.proves(B->formula()));
7274 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
7280 cast<RecordStorageLocation>(Env.getThisPointeeStorageLocation());
7284 auto *B = cast<BoolValue>(getFieldValue(&AnonStruct, *BDecl, Env));
7285 ASSERT_TRUE(Env.proves(B->formula()));
7306 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
7313 cast<RecordStorageLocation>(Env.getThisPointeeStorageLocation());
7318 Env.getStorageLocation(*GlobalIDecl));
7356 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
7361 const StorageLocation *FooLoc = Env.getStorageLocation(*FooDecl);
7364 const Value *FooVal = Env.getValue(*FooLoc);
7370 const StorageLocation *BarLoc = Env.getStorageLocation(*BarDecl);
7389 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
7394 const StorageLocation *FooLoc = Env.getStorageLocation(*FooDecl);
7397 const Value *FooVal = Env.getValue(*FooLoc);
7403 const StorageLocation *BarLoc = Env.getStorageLocation(*BarDecl);
7422 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
7427 const StorageLocation *FooLoc = Env.getStorageLocation(*FooDecl);
7430 const Value *FooVal = Env.getValue(*FooLoc);
7436 const StorageLocation *BarLoc = Env.getStorageLocation(*BarDecl);
7455 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
7460 const StorageLocation *FooLoc = Env.getStorageLocation(*FooDecl);
7463 const Value *FooVal = Env.getValue(*FooLoc);
7471 const StorageLocation *BarLoc = Env.getStorageLocation(*BarDecl);
7490 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
7495 const StorageLocation *FooLoc = Env.getStorageLocation(*FooDecl);
7498 const Value *FooVal = Env.getValue(*FooLoc);
7506 const StorageLocation *BarLoc = Env.getStorageLocation(*BarDecl);
7529 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
7532 Env.getThisPointeeStorageLocation();
7541 const Value *FooVal = Env.getValue(*FooLoc);
7568 const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
7569 auto &A = Env.arena();
7570 auto &VarA = getValueForDecl<BoolValue>(ASTCtx, Env, "a").formula();
7571 auto &VarB = getValueForDecl<BoolValue>(ASTCtx, Env, "b").formula();
7573 EXPECT_FALSE(Env.allows(A.makeAnd(VarA, A.makeNot(VarB))));