I am working on a Formal verification project. The project handles C programs, and as part of the process the C file is compiled to llvm (using llvm-14). Then we extract some logic formulas from the llvm code, but that is besides the point.
Say we have a variable x in the main function of the C code. As we go over the code in llvm, I wanted to know if there is a way (maybe some llvm function that should expect the Function pointer) to figure out which are all the llvm variables that refers to x. As llvm is SSA, I figure that if x changes a lot we would have a lot of different variables referencing it, and I wish to find them by order if possible.
Any help would be appreciated
I could not find anything useful in the LLVM manual