Module `PostAnalysis`

module type PostAnalysis = sig ... end: Signature of modules for post-analysis treatment.

module RunTestGen : PostAnalysis

module RunContractGen : PostAnalysis

module RunRustGen : PostAnalysis

module RunInvLog : PostAnalysis

module RunInvPrint : PostAnalysis

module RunCertif : PostAnalysis

module RunIVC : PostAnalysis

module RunMCS : PostAnalysis

val run_mcs_post_analysis : 'a InputSystem.t -> Analysis.param -> (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 -> 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.