In which circumstances we cannot use symbolic execution?

70 views Asked by At

In which circumstances one cannot use symbolic execution for assertion checking? To illustrate, take the following example:

int a = A, b = B, c = C; \\symbolic

int x = 0, y = 0, z = 0;
if (a){
  x = -2
}
if (b < 5){
  if (!a && c) {y = 1;}
  z = 2;
}
assert (x + y + z != 3)

Here, we can employ a symbolic execution and find out that ¬A ^ (B < 5) ^ C violates our assertion. Now, suppose we change the first condition as follows:

if (a){
  x = x - 10;
  b = b + 5a;
}

With this change, we don't know the new value of x and b. So, can we still use a symbolic execution for assertion checking?

In general, are there any circumstances that we cannot use symbolic execution? i.e., situations where we have to analyze all possible runs of a program.

0

There are 0 answers