This module defines the actual PDS reachability analysis.
module type Analysis = sig ... endmodule Make
(Basis : Pds_reachability_basis.Basis)
(Dph :
Pds_reachability_types_stack.Dynamic_pop_handler
with module Stack_element = Basis.Stack_element
and module State = Basis.State)
(Work_collection_template_impl :
Pds_reachability_work_collection.Work_collection_template) :
Analysis
with module State = Basis.State
and module Stack_element = Basis.Stack_element
and module Targeted_dynamic_pop_action = Dph.Targeted_dynamic_pop_action
and module Untargeted_dynamic_pop_action =
Dph.Untargeted_dynamic_pop_action
and module Stack_action = Dph.Stack_action
and module Terminus = Dph.Terminus