Hi Tomek,
The purpose I am doing this, is because I would like to ask the solver
even at the point before x is used in the branch condition.
For example, in this code:
int add(int p1, int p2, int p3, int x) {
if(x <= 0){
if(p1 > 8) x = x;
else x = x + 1;
if(p2 > 8) x = x;
else x = x + 2;
assert(x <= 3);
}
return x;
}
In this case, the code has 3 branches condition (p1 > 8), (p2 >8) and
the assertion (x <= 3).
Since KLEE normally do the FALSE condition first, it will execute (p1 <=
8) and it will do the addition (x + 1). At the second branch (p2 > 8),
for example, I need to ask the solver whether x <= 0 by using
solver->evaluate(current constraint, x <= 0, result) . Since the current
constraints are only x <= 0 and p1<=8, the solver would say it is
satisfiable (although it's actually not). Therefore, I would like to add
constraint x + 1 at this point, so the solver aware about this.
Thank you.
On 2015-11-04 16:50, Kuchta, Tomasz wrote:
Hi Felicia,
Why would you like to add assignments to the constraints?
What do you want to achieve?
In your example, if ‘x' is later on present in a branch condition,
e.g. if (x < 5) , the symbolic expression that you quote
will be incorporated in the condition instead of ‘x’. As a result you
should end up with having something like
(Add w32 1 (ReadLSB w32 0 x)) < 5 added to your constraint set (on the
“then” side of the branch).
Kind regards,
Tomek
On 4 Nov 2015, at 08:18, felicia <[email protected]> wrote:
Hi,
I would like to ask on how to collect assignments in the state's
constraints.
Because currently KLEE only collect the constraints at the branch
condition.
I have tried to add the assignment expression in the state
constraints.
For example, x = x + 1 has assignment expression like this (Add w32 1
(ReadLSB w32 0 x)).
Then, I add (Add w32 1 (ReadLSB w32 0 x)) at state constraints.
However, this way always give me an assertion error.Please let me know
if you have any suggestion regarding this.
Thank you.
_______________________________________________
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
