[klee-dev] Use Kleaver to get test input from KQuery constraints

[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


On 11 Oct 2013, at 04:00, Bowen Zhou <bwzhou at gmail.com> wrote:

> 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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

-------------- next part --------------
A non-text attachment was scrubbed...
Name: winmail.dat
Type: application/ms-tnef
Size: 4189 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20131011/2f8e49a0/attachment.bin>