In this paper a method is proposed for carrying out analysis of imperative programs. We achieve this by writing down the language
semantics as a declarative program (a constraint logic program, in the approach shown here). We propose an effective style
of writing operational semantics suitable for analysis which we call one-state small-step semantics. Through controlled partial evaluation we are able to generate residual programs where the relationship between
imperative statements and predicates is straightforward. Then we use a static analyser for constraint logic programs on the
residual program. The analysis results are interpreted through program points associating predicates in the partially evaluated
interpreter to statements in its corresponding imperative program. We used an analyser that allows us to determine linear
equality, inequality and disequality relations among the variables of a program without user-provided inductive assertions
or human interaction. The proposed method intends to serve as a framework for the analysis of programs in any imperative language.
The tools required are a partial evaluator and a static analyser for the declarative language.
Keywords Partial Evaluation - Constraint Logic Programming - Operational Semantics - Imperative Program Analysis