Home | History | Annotate | Download | only in Checkers

Lines Matching refs:state

45 // GDM Entry for tracking lock state.
51 ProgramStateRef state = C.getState();
63 AcquireLock(C, CE, state->getSVal(CE->getArg(0), LCtx),
68 AcquireLock(C, CE, state->getSVal(CE->getArg(0), LCtx),
73 AcquireLock(C, CE, state->getSVal(CE->getArg(0), LCtx),
78 AcquireLock(C, CE, state->getSVal(CE->getArg(0), LCtx),
84 ReleaseLock(C, CE, state->getSVal(CE->getArg(0), LCtx));
95 ProgramStateRef state = C.getState();
97 SVal X = state->getSVal(CE, C.getLocationContext());
103 if (state->contains<LockSet>(lockR)) {
117 ProgramStateRef lockSucc = state;
119 // Bifurcate the state, and allow a mode where the lock acquisition fails.
123 llvm::tie(lockFail, lockSucc) = state->assume(retVal);
126 llvm::tie(lockSucc, lockFail) = state->assume(retVal);
136 lockSucc = state->assume(retVal, false);
142 lockSucc = state;
157 ProgramStateRef state = C.getState();
158 LockSetTy LS = state->get<LockSet>();
183 state = state->set<LockSet>(LS.getTail());
184 C.addTransition(state);