Processing predicates including pointer information
US8595707B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Dec 30, 2009 |
| Grant date | Nov 26, 2013 |
| Priority date | — |
| Expiry date | Dec 24, 2031 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F11/3608
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
A system is described for processing predicates in the course of analyzing a program, based on a general-purpose theory of pointers. The system converts location expressions in the predicates into logical formulae that are interpretable by a theorem prover module, producing converted predicates. This conversion associates the location expressions with location objects. More specifically, the conversion represents variables as explicitly-specified location objects, and location terms (such as a field-type access terms and dereference-type terms) as constructor-specified location objects. The theory of pointers is also expressed by a set of axioms which constrain the operation of the theorem prover module.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.