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-***@public.gmane.org
To: nguyenthanhvuh-***@public.gmane.org; klee-dev-AQ/***@public.gmane.org
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-***@public.gmane.org> 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-AQ/***@public.gmane.org
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev