sig
  val has_requires : Cil_types.spec -> bool
  val mark_invalid_initializers : unit -> unit
  val mark_unreachable : unit -> unit
  val mark_green_and_red : unit -> unit
  val mark_rte : unit -> unit
  val c_labels :
    Cil_types.kernel_function ->
    Value_types.callstack -> Eval_terms.labels_states
end