[klee-dev] Possibly incorrect models generated

[Alberto Barbaro]

Hi,
Thanks for you reply. So in the file I can only see information about the
conditions encountered? If the assignment are not tracked how is it
possible to understand which value can a variable assume at the end of the
path? For example I don't how I could verify if another, for instance, can
be 9 (or any other  value) athe end of ktest3.

Thanks


On Sat, Nov 10, 2018, 20:29 Frank Busse <f.busse17 at imperial.ac.uk wrote:

> Hi,
>
>
> On Sat, 10 Nov 2018 07:07:13 +0000
> Alberto Barbaro <barbaro.alberto at gmail.com> wrote:
>
> > I feel I'm missing something because, for instance, I cannot see the
> > case where a = 0 and another = 12.
>
> That's the 2nd if statement:
>
> | if ( a == 77 ) {           // a=77, another=?[0]       = ktest 1
> | } else {                   // (a!=77)
> |   if ( another == 12 ) {   // a!=77[0], another=12     = ktest 3
> |   } else {                 // a!=77[0], another!=12[0] = ktest 2
>
> Seems fine to me (values generated by solver in brackets).
>
>
> Kind regards,
>
> Frank
>
-------------- next part --------------
HTML attachment scrubbed and removed