Obtain symbolic values of some variables backward from some path-sensitive callback

classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

Obtain symbolic values of some variables backward from some path-sensitive callback

Renato Golin via cfe-dev
I need to find loop at first and then to find all definitions of variables in loop control expression, and definitions of some related variables used in rhs of previous definitions.
For example program: 

foo2(int start, int end){
  for (int i=start; i<end; i++){
   …//memory copy loop
  }
}

foo1(int b)
 if(…){
   c = 5;
 }
else c = 10;
 a = b + c;
 foo2(a, b)
}

I need to find loop at first and then (backward) definitions:
a) start = foo2 param (a)
b) a = b + c
c) b = …
d1) c = 5
d2) c = 10

 I.e. is it exist a pointer to previous node(s) of current node of ExplodedGraph?
Also is it possible to find with Clang SA checkers' API input data that allow to reach some basic block?

I want to find constraints on input data that allow to reach particular definitions of variables. Yes, it is over all paths, but not using simple meet operator. So it seemed for me that ExplodedGraph is the best choice.


_______________________________________________
cfe-dev mailing list
[hidden email]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Obtain symbolic values of some variables backward from some path-sensitive callback

Renato Golin via cfe-dev


I need to find loop at first and then to find all definitions of variables in loop control expression, and definitions of some related variables used in rhs of previous definitions.
For example program: 

foo2(int start, int end){
  for (int i=start; i<end; i++){
   …//memory copy loop
  }
}

foo1(int b)
 if(…){
   c = 5;
 }
else c = 10;
 a = b + c;
 foo2(a, b)
}

I need to find loop at first and then (backward) definitions:
a) start = foo2 param (a)
b) a = b + c
c) b = …
d1) c = 5
d2) c = 10

 I.e. is it exist a pointer to previous node(s) of current node of ExplodedGraph?
Also is it possible to find with Clang SA checkers' API input data that allow to reach some basic block?

I want to find constraints on input data that allow to reach particular definitions of variables. Yes, it is over all paths, but not using simple meet operator. So it seemed for me that ExplodedGraph is the best choice.






_______________________________________________
cfe-dev mailing list
[hidden email]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev