module Make:functor (
Domain
:
Abstract_domain.Internal
) ->
functor (
Convert
:
Conversion
with type internal_value := Domain.value and type internal_location := Domain.location
) ->
Abstract_domain.Internal
with type state = Domain.state and type value = Convert.extended_value and type location = Convert.extended_location and type origin = Domain.origin
Parameters: |
|
include Abstract_domain.S_with_Structure
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.