Module Goblint_lib.AutoSoundConfig

Automatically turning on analyses required to ensure soundness based on a given specification (e.g., SV-COMP specification) or programming idioms (e.g., longjmp) in the analyzed code, but only when it is possible to do so automatically. This does not fully exempt from the need for manual configuration.

val enableSpecAnalyses : SvcompSpec.t -> string list -> unit
val enableOptions : string list -> unit
val enableAnalysesForMemSafetySpecification : unit -> unit
val enableAnalysesForTerminationSpecification : unit -> unit
val enableAnalysesForSpecification : unit -> unit
val longjmpAnalyses : string list
val activateLongjmpAnalysesWhenRequired : unit -> unit