Re: [klee-dev] Unexpected Output!

2014-01-27 Thread General Email
, metadata !1, null} !14 = metadata !{i32 19, i32 0, metadata !1, null} Thanks On Friday, January 24, 2014 11:43 AM, General Email general_mail2...@yahoo.com wrote: Thanks Dan, I moved the klee_assume statement to the end of the conditional statement and ran klee with the emit-all-errors option

[klee-dev] How to show (get) the negative values returned in klee's .pc files?

2013-05-01 Thread General Email
Hi, I need to understand how to use klee_assume and klee_assert. I tried to implement the following assumptions (in the function listed below) which assumed that if a symbolic variable x satisfies the condition !(0(x+5)) and that if another variable y is set to x+7, I want to check whether y is

Re: [klee-dev] How to show (get) the negative values returned in klee's .pc files?

2013-05-01 Thread General Email
and klee_assert work. Again thank you so much for your help. From: Daniel Liew daniel.l...@imperial.ac.uk To: General Email general_mail2...@yahoo.com Cc: klee-dev klee-dev@imperial.ac.uk Sent: Wednesday, May 1, 2013 1:01 PM Subject: Re: [klee-dev] How to show (get

[klee-dev] How to get the content of a symbolic variable?

2013-04-08 Thread General Email
Hi, How to get the content of a symbolic variable? When I tried to run the code listed below, I got the following output from klee KLEE: WARNING ONCE: calling external: printf(182324664, 182337984, (Add w32 7 (ReadLSB w32 0 inVar))) KLEE: ERROR: /home/try1.c:53: failed external call: printf

[klee-dev] KLEE: ERROR: failed external call: itos

2013-03-26 Thread General Email
Hi, I'm trying to explore how to use klee. When I run klee on a small program I got the following warning messages: KLEE: WARNING: undefined reference to function: itos KLEE: WARNING: undefined reference to function: printf KLEE: WARNING: undefined reference to function: strcat Also I got the