Parameter Make.D

type state

An abstract domain is a lattice representing abstract states state.

type transition = G.transition

The syntax for transiton between program points.

type loop_id

An identifier for the loop id. Can be unit if unused; it can be used as a widening ID in the symbolic expression domain (Lemerre, POPL'23; Lesbre & Lemerre, PLDI'24).

val copy : state -> state

Create an independant copy of the state, not sharing any mutable data

val join : state -> state -> state

Standard join operation, over-approximating union.

val fixpoint_step : loop_id:loop_id -> state -> state -> state * bool

fixpoint_step ~loop_id previous next detects whether fixpoint computation is over (then it returns true and the final abstract state), or it tries to extrapolates (widen) from the evolution from previous to next (returning false and an widened state).

val transfer : transition -> state -> state option

Standard transfer function. The transition returns None if the state is bottom

val pp : Stdlib.Format.formatter -> state -> unit

Pretty printer used for debugging.

val enter_loop : state -> state * loop_id

Enter loop, providing a new identifier for the loop.

val leave_loop : state -> state

Leave loop; useful e.g. for induction variable analysis, that introduces variable counting the number of loop iterations.