Home | History | Annotate | Download | only in Checkers

Lines Matching full:state

45 // GDM Entry for tracking lock state.
59 const ProgramState *state = C.getState();
61 const FunctionDecl *FD = state->getSVal(Callee).getAsFunctionDecl();
78 AcquireLock(C, CE, state->getSVal(CE->getArg(0)), false, PthreadSemantics);
82 AcquireLock(C, CE, state->getSVal(CE->getArg(0)), false, XNUSemantics);
86 AcquireLock(C, CE, state->getSVal(CE->getArg(0)), true, PthreadSemantics);
90 AcquireLock(C, CE, state->getSVal(CE->getArg(0)), true, XNUSemantics);
95 ReleaseLock(C, CE, state->getSVal(CE->getArg(0)));
106 const ProgramState *state = C.getState();
108 SVal X = state->getSVal(CE);
114 if (state->contains<LockSet>(lockR)) {
128 const ProgramState *lockSucc = state;
130 // Bifurcate the state, and allow a mode where the lock acquisition fails.
134 llvm::tie(lockFail, lockSucc) = state->assume(retVal);
137 llvm::tie(lockSucc, lockFail) = state->assume(retVal);
148 lockSucc = state->assume(retVal, false);
154 lockSucc = state;
169 const ProgramState *state = C.getState();
170 llvm::ImmutableList<const MemRegion*> LS = state->get<LockSet>();
195 state = state->set<LockSet>(LS.getTail());
196 C.addTransition(state);