109   ProgramStateRef evalAssume(ProgramStateRef State, SVal Cond,
112   void printState(raw_ostream &Out, ProgramStateRef State, const char *NL,
304                                         ProgramStateRef State) {  in getNullConstraint()  argument
305   ConditionTruthVal Nullness = State->isNull(Val);  in getNullConstraint()
344   ProgramStateRef State = N->getState();  in VisitNode()  local
347   const NullabilityState *TrackedNullab = State->get<NullabilityMap>(Region);  in VisitNode()
379 static bool checkValueAtLValForInvariantViolation(ProgramStateRef State,  in checkValueAtLValForInvariantViolation()  argument
394   auto StoredVal = State->getSVal(*RegionVal).getAs<loc::MemRegionVal>();  in checkValueAtLValForInvariantViolation()
398   if (getNullConstraint(*StoredVal, State) == NullConstraint::IsNull)  in checkValueAtLValForInvariantViolation()
406                                     ProgramStateRef State,  in checkParamsForPreconditionViolation()  argument
412     SVal LV = State->getLValue(ParamDecl, LocCtxt);  in checkParamsForPreconditionViolation()
413     if (checkValueAtLValForInvariantViolation(State, LV,  in checkParamsForPreconditionViolation()
422 checkSelfIvarsForInvariantViolation(ProgramStateRef State,  in checkSelfIvarsForInvariantViolation()  argument
432   SVal SelfVal = State->getSVal(State->getRegion(SelfDecl, LocCtxt));  in checkSelfIvarsForInvariantViolation()
444     SVal LV = State->getLValue(IvarDecl, SelfVal);  in checkSelfIvarsForInvariantViolation()
445     if (checkValueAtLValForInvariantViolation(State, LV, IvarDecl->getType())) {  in checkSelfIvarsForInvariantViolation()
452 static bool checkInvariantViolation(ProgramStateRef State, ExplodedNode *N,  in checkInvariantViolation()  argument
454   if (State->get<InvariantViolated>())  in checkInvariantViolation()
472   if (checkParamsForPreconditionViolation(Params, State, LocCtxt) ||  in checkInvariantViolation()
473       checkSelfIvarsForInvariantViolation(State, LocCtxt)) {  in checkInvariantViolation()
475       C.addTransition(State->set<InvariantViolated>(true), N);  in checkInvariantViolation()
500   ProgramStateRef State = C.getState();  in checkDeadSymbols()  local
501   NullabilityMapTy Nullabilities = State->get<NullabilityMap>();  in checkDeadSymbols()
506       State = State->remove<NullabilityMap>(Reg);  in checkDeadSymbols()
512   PropertyAccessesMapTy PropertyAccesses = State->get<PropertyAccessesMap>();  in checkDeadSymbols()
516       State = State->remove<PropertyAccessesMap>(PropKey);  in checkDeadSymbols()
524   if (checkInvariantViolation(State, C.getPredecessor(), C))  in checkDeadSymbols()
526   C.addTransition(State);  in checkDeadSymbols()
541   ProgramStateRef State = Event.SinkNode->getState();  in checkEvent()  local
543       State->get<NullabilityMap>(Region);  in checkEvent()
575   ProgramStateRef State = C.getState();  in checkBeginFunction()  local
585     const VarRegion *ParamRegion = State->getRegion(Param, LCtx);  in checkBeginFunction()
587         State->getSVal(ParamRegion).getAsRegion();  in checkBeginFunction()
591     State = State->set<NullabilityMap>(ParamPointeeRegion,  in checkBeginFunction()
594   C.addTransition(State);  in checkBeginFunction()
625   ProgramStateRef State = Context.getState();  in checkLocation()  local
627   auto StoredVal = State->getSVal(Region).getAs<loc::MemRegionVal>();  in checkLocation()
637     if (ProgramStateRef NewState = State->assume(*StoredVal, true)) {  in checkLocation()
662   ProgramStateRef State = C.getState();  in checkPreStmt()  local
663   if (State->get<InvariantViolated>())  in checkPreStmt()
692   NullConstraint Nullness = getNullConstraint(*RetSVal, State);  in checkPreStmt()
710     ExplodedNode *N = C.generateErrorNode(State, &Tag);  in checkPreStmt()
728     State = State->set<InvariantViolated>(true);  in checkPreStmt()
729     C.addTransition(State);  in checkPreStmt()
738       State->get<NullabilityMap>(Region);  in checkPreStmt()
746       ExplodedNode *N = C.addTransition(State, C.getPredecessor(), &Tag);  in checkPreStmt()
759     State = State->set<NullabilityMap>(Region,  in checkPreStmt()
762     C.addTransition(State);  in checkPreStmt()
773   ProgramStateRef State = C.getState();  in checkPreCall()  local
774   if (State->get<InvariantViolated>())  in checkPreCall()
777   ProgramStateRef OrigState = State;  in checkPreCall()
796     NullConstraint Nullness = getNullConstraint(*ArgSVal, State);  in checkPreCall()
810       ExplodedNode *N = C.generateErrorNode(State);  in checkPreCall()
830         State->get<NullabilityMap>(Region);  in checkPreCall()
840         ExplodedNode *N = C.addTransition(State);  in checkPreCall()
852         ExplodedNode *N = C.addTransition(State);  in checkPreCall()
862   if (State != OrigState)  in checkPreCall()
863     C.addTransition(State);  in checkPreCall()
881   ProgramStateRef State = C.getState();  in checkPostCall()  local
882   if (State->get<InvariantViolated>())  in checkPostCall()
894     State = State->set<NullabilityMap>(Region, Nullability::Contradicted);  in checkPostCall()
895     C.addTransition(State);  in checkPostCall()
900       State->get<NullabilityMap>(Region);  in checkPostCall()
912     State = State->set<NullabilityMap>(Region, Nullability::Nullable);  in checkPostCall()
913     C.addTransition(State);  in checkPostCall()
918                                           ProgramStateRef State) {  in getReceiverNullability()  argument
929     NullConstraint Nullness = getNullConstraint(*DefOrUnknown, State);  in getReceiverNullability()
939         State->get<NullabilityMap>(SelfRegion);  in getReceiverNullability()
950 ProgramStateRef NullabilityChecker::evalAssume(ProgramStateRef State, SVal Cond,  in evalAssume()  argument
952   PropertyAccessesMapTy PropertyAccesses = State->get<PropertyAccessesMap>();  in evalAssume()
955       ConditionTruthVal IsNonNull = State->isNonNull(PropVal.Value);  in evalAssume()
959         State = State->set<PropertyAccessesMap>(PropKey, Replacement);  in evalAssume()
962         State = State->remove<PropertyAccessesMap>(PropKey);  in evalAssume()
967   return State;  in evalAssume()
982   ProgramStateRef State = C.getState();  in checkPostObjCMessage()  local
983   if (State->get<InvariantViolated>())  in checkPostObjCMessage()
1005       State =  in checkPostObjCMessage()
1006           State->set<NullabilityMap>(ReturnRegion, Nullability::Contradicted);  in checkPostObjCMessage()
1007       C.addTransition(State);  in checkPostObjCMessage()
1015       State =  in checkPostObjCMessage()
1016           State->set<NullabilityMap>(ReturnRegion, Nullability::Contradicted);  in checkPostObjCMessage()
1017       C.addTransition(State);  in checkPostObjCMessage()
1028           State = State->set<NullabilityMap>(ReturnRegion,  in checkPostObjCMessage()
1030           C.addTransition(State);  in checkPostObjCMessage()
1038   Nullability SelfNullability = getReceiverNullability(M, State);  in checkPostObjCMessage()
1041       State->get<NullabilityMap>(ReturnRegion);  in checkPostObjCMessage()
1056       State = State->set<NullabilityMap>(  in checkPostObjCMessage()
1058       C.addTransition(State);  in checkPostObjCMessage()
1090             State->get<PropertyAccessesMap>(Key);  in checkPostObjCMessage()
1102             State = State->set<PropertyAccessesMap>(  in checkPostObjCMessage()
1120     State = State->set<NullabilityMap>(  in checkPostObjCMessage()
1122     C.addTransition(State);  in checkPostObjCMessage()
1139   ProgramStateRef State = C.getState();  in checkPostStmt()  local
1140   if (State->get<InvariantViolated>())  in checkPostStmt()
1157     NullConstraint Nullness = getNullConstraint(*RegionSVal, State);  in checkPostStmt()
1159       State = State->set<NullabilityMap>(Region, Nullability::Contradicted);  in checkPostStmt()
1160       C.addTransition(State);  in checkPostStmt()
1166       State->get<NullabilityMap>(Region);  in checkPostStmt()
1171     State = State->set<NullabilityMap>(Region,  in checkPostStmt()
1173     C.addTransition(State);  in checkPostStmt()
1179     State = State->set<NullabilityMap>(Region, Nullability::Contradicted);  in checkPostStmt()
1180     C.addTransition(State);  in checkPostStmt()
1263   ProgramStateRef State = C.getState();  in checkBind()  local
1264   if (State->get<InvariantViolated>())  in checkBind()
1271   NullConstraint RhsNullness = getNullConstraint(*ValDefOrUnknown, State);  in checkBind()
1295     ExplodedNode *N = C.generateErrorNode(State, &Tag);  in checkBind()
1316     State = State->set<InvariantViolated>(true);  in checkBind()
1317     C.addTransition(State);  in checkBind()
1329       State->get<NullabilityMap>(ValueRegion);  in checkBind()
1338       ExplodedNode *N = C.addTransition(State, C.getPredecessor(), &Tag);  in checkBind()
1353     State = State->set<NullabilityMap>(  in checkBind()
1355     C.addTransition(State);  in checkBind()
1361     State = State->set<NullabilityMap>(  in checkBind()
1363     C.addTransition(State);  in checkBind()
1367 void NullabilityChecker::printState(raw_ostream &Out, ProgramStateRef State,  in printState()  argument
1370   NullabilityMapTy B = State->get<NullabilityMap>();  in printState()
1372   if (State->get<InvariantViolated>())  in printState()
1379   if (!State->get<InvariantViolated>())  in printState()
1382   for (auto [Region, State] : B) {  in printState()
1384     State.print(Out);  in printState()