Lu,

bindLocal just sets the value of the destination stack local (register) of the 
'target' instruction to 'value' in the current state. Each instruction with a 
return value is statically mapped to a stack location on startup.

-David

On Jul 21, 2011, at 12:24 PM, Lu Huizhi wrote:

> Hello,
> 
> I'm studying the source code of KLEE and have a question now.
> 
> I don't quite understand the purpose of bindLocal function. Could you please 
> give me some help about it? Thanks very much!
> 
> void Executor::bindLocal(KInstruction *target, ExecutionState &state, 
>                          ref<Expr> value) 
> 
> Thanks
> -- 
> Lu Huizhi
> [email protected]
> 
> _______________________________________________
> klee-dev mailing list
> [email protected]
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev

_______________________________________________
klee-dev mailing list
[email protected]
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev

Reply via email to