Goblint_lib.WitnessUtilUtilities for witness generation and witness invariants.
module NH : sig ... endmodule NS : sig ... endval find_main_entry : ((MyCFG.node * 'a) * 'b) list -> MyCFG.node * 'aval find_loop_heads : (module MyCFG.FileCfg) -> unit NH.tmodule Invariant (FileCfg : MyCFG.FileCfg) : sig ... endmodule YamlInvariant (FileCfg : MyCFG.FileCfg) : sig ... endmodule YamlInvariantValidate (FileCfg : MyCFG.FileCfg) : sig ... endmodule InvariantParser : sig ... end