1. A method comprising: receiving, from a program analysis engine, at least one predicate that is identified during analysis of a program, said at least one predicate having a location expression associated therewith that includes pointer information; converting, using at least one translation rule, the location expression of said at least one predicate to a logical formula that is interpretable by a theorem prover module, wherein: the converting thereby forms at least one converted predicate, the logical formula identifies a location object that is associated with an address object and a value object, and the address object corresponds to an address of the location object and dereferences to obtain the value object of the location object; and passing said at least one converted predicate, including the location object, the address object, and the value object, to the theorem prover module for processing, wherein at least the converting is performed by a processing device.
8. The method of claim 1 , wherein the location object is associated with either a normal location object or an abnormal location object, the abnormal location object representing a invalid location.