[klee-dev] Stopping Klee when reaching a particular location

[Urmas Repinski]

Hi Vu, Loi.

This question, if i am not mistaken, was already previously in the list couple of months ago.
This is practically the answer that were posted:

Firstly, 
If you want that some branches are not processed by KLEE, then it is probably worth to investigate klee_assume function.
klee_assume(false) will stop processing branch, where this function is reached, and execution will switch to other branches.

Klee assume is equivalent to the 
void klee_assume(int constraint) {
  if (!constraint) klee_silent_exit(0);
}If you want to avoid the 

klee_assume call (provably false) 
KLEE: NOTE: now ignoring this error at this location

message, you can try to use 
klee_silent_exit(0);

function then.

Secondly,
You want to completely stop klee processing, when some branches should be reached, this will cause undetermined generated data.

Thirdly,
I see no reason why not to use C return instead of klee_assume and klee_silent_exit(0); , as i see results should be the same, you can experiment using this different syntax to check if i am right or not.

Urmas Repinski.



Date: Sat, 4 Jan 2014 20:06:01 +0800
From: loi.luuthe at gmail.com
To: nguyenthanhvuh at gmail.com; klee-dev at imperial.ac.uk
Subject: Re: [klee-dev] Stopping Klee when reaching a particular location

Why dont u just return the program at that location?
On 4 Jan 2014 19:58, "ThanhVu (Vu) Nguyen" <nguyenthanhvuh at gmail.com> wrote:

Hi, is there a trick to force KLEE to complete stop when reaching a

particular location ?  I've tried putting klee_assert(0);  at the

location I want but that just reports a KLEE: ERROR: ASSERTION FAIL: 0

and then keeps going.  I want KLEE to stop as soon as it reports that

error.



--

Vu



_______________________________________________

klee-dev mailing list

klee-dev at imperial.ac.uk

https://mailman.ic.ac.uk/mailman/listinfo/klee-dev



_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


 		 	   		  
-------------- next part --------------
HTML attachment scrubbed and removed