A Formal Automated Approach for Reverse Engineering Programs with Pointers