Hi, Kirill.
First of all, it is not clear what type of inputs should be generated.
In the example below all integers will be generated, starting from 0 ...
including 500.
klee_assert function will trigger __assert_fail klee function, this possibly
will terminate input generation process, possibly not, i am not very sure.
Anyway it is possible that you want something more meaningful, if input 500
should be generated, or input 500 should not be generated.
In this case better to use klee_assume function:
void klee_assume(int constraint) {
if (!constraint) klee_silent_exit(0);
}
{int a;
klee_make_symbolic(&a, sizeof(a), "a");
int i =0 ;
int n =1;
for (i =0; i < a;i++){
n++;
}
klee_assume(n==500); or klee_assume(n!=500);
Will generate a=500 or all a-s, except 500.
Urmas Repinski.
Date: Tue, 25 Mar 2014 09:33:26 +0000
From: [email protected]
To: [email protected]
Subject: [klee-dev] KLEE relationship between loop length and counter.
Hello Everyone,(Sorry for the previous email, it has been sent by mistake
before I finished it!)
Could you please let me know if what I am doing cannot be achieved with KLEE
and if it can, how can I do it?
1. Please consider my usage example below. The problem that I am observing is
that KLEE does not sees relationship between loop length and the counter "n".
In my experiments (with different search strategies) KLEE always encountered
assertion by a blind search, and usually after generating 500 test cases.
{int a;
klee_make_symbolic(&a, sizeof(a), "a");
int i =0 ;
int n =1;
for (i =0; i < a;i++){
n++;
}
if (n == 500)
klee_assert(0);
return 0;
}
Is this is something that is fundamentally impossible in KLEE, or can be
achieved by rewriting my example?
Thank you very much!
_______________________________________________
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
