Fix the bug in subsumption related to Global vars

[rasoolmaghareh]

@xuanlinhha I have checked this branch with the programs in the klee-examples\basic folder. There are a few issues:

1- In addition_safe6.c, the number of subsumptions is zero (can you please check the subsumptions manually). 2- pointer_struct5.c, pointer_struct6.c and regexp_mark.c crash. 3- recursion2.c takes a very long time (possibly the same issue as addition_safe6.c.

Can you please check these issues? Thanks.

[rasoolmaghareh]

Summary of our online meeting:

•If a global variable is updated, TxTreeNode should contain a copy of its value. •This way when generating an interpolant, we have the intermediate value of the global var.

Example:

int a = 5;
main() {
  if (b > 0)
      a = a + 2;
  else
      skip;
  …
  if (a >= 7){
      …
  } else {
     …
  }
}

Here, the node after b>0 should contain the updated value a = 7. While the node after b<=0 should read the original value a = 5.

After the false branch of the first if statment, a=5, then a>=7 is false and a=5 would be stored as interpolant.

At the true branch, a=7, then a<7 is false and a=7 is retrieved from the parent node and stored as interpolant.

[xuanlinhha]

I made a commit to get global value from parent node if it exists, otherwise, get the current one

[xuanlinhha]

1- In addition_safe6.c & 3- recursion2.c => Fixed 2- pointer_struct5.c, pointer_struct6.c and regexp_mark.c crash. => I see the global is a pointer to a structure, so I need to see more

[xuanlinhha]

I decided to skip checking global variable if it is a pointer

[rasoolmaghareh]

Noted. I have checked and this branch passes the make check in the klee folder and make in the klee-examples\basic folder.