Commit 77bb3bea authored by Daniel Liew's avatar Daniel Liew
Browse files

Added a few userful comments.

parent 4d1dc5d4
......@@ -3327,6 +3327,15 @@ void Executor::resolveExact(ExecutionState &state,
it != ie; ++it) {
ref<Expr> inBounds = EqExpr::create(p, it->first->getBaseExpr());
/*
* Assume branches.first is path where inBounds is true
* Assume branches.second is path where inBound is false
* Is this correct with the randomised swapping in fork() ?
*
* Notice that that "unbound" is being reused in the loop.
* Unbound will accumulate a constraint (p does not point
* to a particular MemoryObject) on every iteration.
*/
StatePair branches = fork(*unbound, inBounds, true, KLEE_FORK_INTERNAL);
if (branches.first)
......@@ -3334,9 +3343,18 @@ void Executor::resolveExact(ExecutionState &state,
unbound = branches.second;
if (!unbound) // Fork failure
break;
{
// A state does not exist where inBounds is false.
// No need to search for more states where p could
// point to other MemoryObjects.
break;
}
}
// If we've finished looping through all memory objects
// and a state exists where p does not point to any of those
// objects then the pointer can point to an invalid point in
// memory.
if (unbound) {
terminateStateOnError(*unbound,
"memory error: invalid pointer: " + name,
......
......@@ -196,6 +196,7 @@ cl_int clEnqueueNDRangeKernel(cl_command_queue command_queue,
cl_uint num_events_in_wait_list,
const cl_event *event_wait_list,
cl_event *event) {
// Why 64? Usually have work_dim <= 3
size_t num_groups[64], ids[64], local_ids[64], global_ids[64], workgroup_count,
work_item_count;
cl_uint i, last_id;
......@@ -230,6 +231,11 @@ cl_int clEnqueueNDRangeKernel(cl_command_queue command_queue,
return CL_INVALID_WORK_GROUP_SIZE;
num_groups[i] = global_work_size[i] / local_work_size[i];
} else {
/* NULL was passed so runtime is being asked to choose
* our own division of work items into work groups.
* We choose to simply only have 1 work group and have
* all work items in the same work group.
*/
num_groups[i] = 1;
}
}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment