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
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 {
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;
}
