WResult (p.goblint.2.0.0.doc.goblint.lib.Goblint

val init : GoblintCil.Cil.file -> unit

val determine_result : 
  Spec.D.t LHT.t ->
  [> `Bot | `Lifted1 of Spec.G.t ] GHT.t ->
  ((MyCFG.node * Spec.C.t) * 'a) list ->
  (module Svcomp.Task) ->
  (module Goblint_lib__Witness.WitnessTaskResult)

val write : 
  Spec.D.t LHT.t ->
  [> `Bot | `Lifted1 of Spec.G.t ] GHT.t ->
  ((MyCFG.node * Spec.C.t) * 'a) list ->
  unit