Use Kleaver to get test input from KQuery constraints

[Bowen Zhou]

Hello,

I tried to use Kleaver to solve a .pc file generated by Klee with option
'-write-pcs'. The command I used is 'kleaver input.pc'. Kleaver always
gives 'Query 0: INVALID' as its output.

How can I get Kleaver to output a test input that satisfy the
constraints in the input .pc file? Is it possible?

Cheers,
Bowen

[Kuchta, Tomasz]

Hi Bowen,

The way to do that is the following:
- at the beginning of the file you will find a list of arrays
- from the list, you choose the name of the array that you are interested in
- .pc file probably ends with "false)"
- the way to get the value of the selected array is to modify "false)" into "false [] [array_name])"
(where you put the name of the selected array in square brackets); so you have two pairs of
square brackets - the first pair is empty and in the second one you put the name of the array.

Hope that helps,
Best regards,
Tomek

Post by Bowen Zhou
Hello,
I tried to use Kleaver to solve a .pc file generated by Klee with option '-write-pcs'. The command I used is 'kleaver input.pc'. Kleaver always gives 'Query 0: INVALID' as its output.
How can I get Kleaver to output a test input that satisfy the constraints in the input .pc file? Is it possible?
Cheers,
Bowen
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev