Re: [klee-dev] Possibly incorrect models generated

2018-11-10 Thread 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  Hi,
>
>
> On Sat, 10 Nov 2018 07:07:13 +
> Alberto Barbaro  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
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Re: [klee-dev] Possibly incorrect models generated

2018-11-10 Thread Frank Busse 
Hi,


On Sat, 10 Nov 2018 07:07:13 +
Alberto Barbaro  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
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[klee-dev] Possibly incorrect models generated

2018-11-09 Thread Alberto Barbaro 
Hi all,
I'm generating the .smt2 file for the following simple c program:

#include 

int main() {
int a;
int another;

klee_make_symbolic(, sizeof(a), "a");
klee_make_symbolic(, sizeof(another), "another");

if ( a == 77 ) {
a += 6;
another = 5;
} else {
a = 9;
if ( another == 12 ) {
a += 7;
} else {
a += 10;
}
}

return 0;
}

I can compile it using clang -I ../../include -emit-llvm -c -g simple.c and
obtain the .smt2 running klee -write-smt2s simple.bc. At this point I would
like to see the model for the 3 test case and I have the following results:

klee@a8a6399e6799:~/klee_src/examples/simple$ ktest-tool --write-ints
klee-last/test01.ktest
ktest file : 'klee-last/test01.ktest'
args   : ['simple.bc']
num objects: 2
object0: name: b'a'
object0: size: 4
object0: data: 77
object1: name: b'another'
object1: size: 4
object1: data: 0


klee@a8a6399e6799:~/klee_src/examples/simple$ ktest-tool --write-ints
klee-last/test02.ktest
ktest file : 'klee-last/test02.ktest'
args   : ['simple.bc']
num objects: 2
object0: name: b'a'
object0: size: 4
object0: data: 0
object1: name: b'another'
object1: size: 4
object1: data: 0

klee@a8a6399e6799:~/klee_src/examples/simple$ ktest-tool --write-ints
klee-last/test03.ktest
ktest file : 'klee-last/test03.ktest'
args   : ['simple.bc']
num objects: 2
object0: name: b'a'
object0: size: 4
object0: data: 0
object1: name: b'another'
object1: size: 4
object1: data: 12

I feel I'm missing something because, for instance, I cannot see the case
where a = 0 and another = 12.

Can you help me to understand if the models are correct and why?

Thanks
Alberto
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev