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 <[email protected] wrote: > Hi, > > > On Sat, 10 Nov 2018 07:07:13 +0000 > Alberto Barbaro <[email protected]> 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 >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
