PostAnalysis (kind2dev@731decdf5fb1.PostAnalysis)

module type PostAnalysis = sig ... end

Signature of modules for post-analysis treatment.

module RunTestGen : PostAnalysis

module RunContractGen : PostAnalysis

module RunInvPrint : PostAnalysis

module RunCertif : PostAnalysis

module RunSliceCertif : PostAnalysis

module RunIVC : PostAnalysis

module RunMCS : PostAnalysis

val run_mcs_post_analysis : 
  'a InputSystem.t ->
  Analysis.param ->
  (bool ->
    bool ->
    bool ->
    Lib.kind_module list ->
    'a InputSystem.t ->
    Analysis.param ->
    TransSys.t ->
    unit) ->
  TransSys.t ->
  unit Res.res

val run : 
  'a InputSystem.t ->
  Scope.t ->
  (bool ->
    bool ->
    bool ->
    Lib.kind_module list ->
    'a InputSystem.t ->
    Analysis.param ->
    TransSys.t ->
    unit) ->
  Analysis.results ->
  unit

Runs the post-analysis things on a system and its results.