Hello AK,
You can use klee-replay and gcov, as explained in the KLEE tutorial at
http://klee.llvm.org/TestingCoreutils.html (step 6).
Paul
On 29 Mar 2013, at 12:44, General Email wrote:
> I'm interested in is the value returned as the result from the execution
> process. For example if I have the following small program
> --------------------------------------------------
> int globalVar1=100;
> char* globalVar2="";
> void myFunction(int k) {
> if (k > 0)
> {
> globalVar1 = k;
> globalVar2 = "Message1";
> }
> else
> {
> globalVar2 = "Message2";
> }
> }
>
> int main() {
> int k;
> klee_make_symbolic(&k, sizeof(k), "k");
> get_sign(k);
> }
> --------------------------------------------------
> With klee I got the following two paths, each of which has to satisfy one of
> the following constraints:
> 1)
> array k[4] : w32 -> w8 = symbolic
> (query [(Eq false
> (Slt 0
> (ReadLSB w32 0 k)))]
> false)
>
> 2)
> array k[4] : w32 -> w8 = symbolic
> (query [(Slt 0
> (ReadLSB w32 0 k))]
> false)
>
>
> How can I get the symbolic statements associated with each path. For instance
> I need to know that in the second path, globalVar1 and globalVar2 are changed
> respectively to "some symbolic value" and "Message1".
>
>
> Any suggestions?
> Thanks
> AK
> _______________________________________________
> klee-dev mailing list
> [email protected]
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
