Re: [klee-dev] concretized symbolic size

2021-02-16 Thread Michael
Thx Daniel. Got that (the three states); my question is why does your State 3 need to exist at all? This doesn not seem like an error to me. Guo,Shengjian writes: Hi, To my understanding, KLEE will maintain three states in handling a symbolic-size memory allocation: State 1 -- tries to

Re: [klee-dev] Store only test cases with counter-examples

2021-02-16 Thread Frank Busse
Hi Anton, On Wed, 10 Feb 2021 10:39:09 +0300 Anton Trunov wrote: > I’m looking for a CLI option that would allow me to store only test > cases resulting in errors. The `--only-output-states-covering-new` > option reduces the number of tests written to my hard drive > significantly, however I’d

Re: [klee-dev] Use of -sym-stdin/stdout

2021-02-16 Thread Cristian Cadar
On 09/02/2021 14:09, Eduardo R B Marques wrote: 2) you should only use —sym-sdout if you need to symbolically analyze the contents of stdout, otherwise don't set it Yes, that’s right, I do want to “analyze the contents of stdout”. But how can it be done? As I mentioned, the ktest files do