Module type Abstract_domain.Internal

module type Internal = sig .. end

Full implementation of domains. Automatically built by Domain_builder.Complete from an S_with_Structure domain.

include Abstract_domain.S

module Store: Abstract_domain.Store  with type state := state

val post_analysis : t Eval.or_bottom -> unit

This function is called after the analysis. The argument is the state computed at the return statement of the main function. The function can also access all states stored in the Store module during the analysis. If the analysis aborted, this function is not called.