sig
  val is_integral_const : Cil_types.constant -> bool
  val possible_value_of_integral_const :
    Cil_types.constant -> Integer.t option
  val possible_value_of_integral_expr : Cil_types.exp -> Integer.t option
  val value_of_integral_const : Cil_types.constant -> Integer.t
  val value_of_integral_expr : Cil_types.exp -> Integer.t
  val is_null_expr : Cil_types.exp -> bool
  val is_non_null_expr : Cil_types.exp -> bool
  val is_integral_logic_const : Cil_types.logic_constant -> bool
  val possible_value_of_integral_logic_const :
    Cil_types.logic_constant -> Integer.t option
  val value_of_integral_logic_const : Cil_types.logic_constant -> Integer.t
  val possible_value_of_integral_term : Cil_types.term -> Integer.t option
  val term_lvals_of_term : Cil_types.term -> Cil_types.term_lval list
  val precondition : goal:bool -> Cil_types.funspec -> Cil_types.predicate
  val behavior_assumes : Cil_types.funbehavior -> Cil_types.predicate
  val behavior_precondition :
    goal:bool -> Cil_types.funbehavior -> Cil_types.predicate
  val behavior_postcondition :
    goal:bool ->
    Cil_types.funbehavior ->
    Cil_types.termination_kind -> Cil_types.predicate
  val disjoint_behaviors :
    Cil_types.funspec -> string list -> Cil_types.predicate
  val complete_behaviors :
    Cil_types.funspec -> string list -> Cil_types.predicate
  val merge_assigns_from_complete_bhvs :
    ?warn:bool ->
    ?unguarded:bool ->
    Cil_types.funbehavior list -> string list list -> Cil_types.assigns
  val merge_assigns_from_spec :
    ?warn:bool -> Cil_types.funspec -> Cil_types.assigns
  val merge_assigns :
    ?warn:bool -> Cil_types.funbehavior list -> Cil_types.assigns
  val variable_term :
    Cil_types.location -> Cil_types.logic_var -> Cil_types.term
  val constant_term : Cil_types.location -> Integer.t -> Cil_types.term
  val is_null_term : Cil_types.term -> bool
  val is_loop_statement : Cil_types.stmt -> bool
  val get_sid : Cil_types.kinstr -> int
  val mkassign :
    Cil_types.lval -> Cil_types.exp -> Cil_types.location -> Cil_types.instr
  val mkassign_statement :
    Cil_types.lval -> Cil_types.exp -> Cil_types.location -> Cil_types.stmt
  val is_block_local : Cil_types.varinfo -> Cil_types.block -> bool
  val block_of_local :
    Cil_types.fundec -> Cil_types.varinfo -> Cil_types.block
  val array_type :
    ?length:Cil_types.exp ->
    ?attr:Cil_types.attributes -> Cil_types.typ -> Cil_types.typ
  val direct_array_size : Cil_types.typ -> Integer.t
  val array_size : Cil_types.typ -> Integer.t
  val direct_element_type : Cil_types.typ -> Cil_types.typ
  val element_type : Cil_types.typ -> Cil_types.typ
  val direct_pointed_type : Cil_types.typ -> Cil_types.typ
  val pointed_type : Cil_types.typ -> Cil_types.typ
  val is_function_type : Cil_types.varinfo -> bool
  module Function :
    sig
      val formal_args :
        Cil_types.varinfo ->
        (string * Cil_types.typ * Cil_types.attributes) list
      val is_formal : Cil_types.varinfo -> Cil_types.fundec -> bool
      val is_local : Cil_types.varinfo -> Cil_types.fundec -> bool
      val is_formal_or_local : Cil_types.varinfo -> Cil_types.fundec -> bool
      val is_formal_of_prototype :
        Cil_types.varinfo -> Cil_types.varinfo -> bool
      val is_definition : Cil_types.cil_function -> bool
      val get_vi : Cil_types.cil_function -> Cil_types.varinfo
      val get_name : Cil_types.cil_function -> string
      val get_id : Cil_types.cil_function -> int
    end
  val can_be_cea_function : string -> bool
  val is_cea_function : string -> bool
  val is_cea_domain_function : string -> bool
  val is_cea_dump_function : string -> bool
  val is_cea_dump_file_function : string -> bool
  val is_frama_c_builtin : string -> bool
end