sig   exception Not_well_formed of Cil_types.location * string   val add_logic_function : Cil_types.logic_info -> unit   val instantiate :     (string * Cil_types.logic_type) list ->     Cil_types.logic_type -> Cil_types.logic_type   val is_instance_of :     string list -> Cil_types.logic_type -> Cil_types.logic_type -> bool   val unroll_type :     ?unroll_typedef:bool -> Cil_types.logic_type -> Cil_types.logic_type   val isLogicType : (Cil_types.typ -> bool) -> Cil_types.logic_type -> bool   val isLogicArrayType : Cil_types.logic_type -> bool   val isLogicCharType : Cil_types.logic_type -> bool   val isLogicVoidType : Cil_types.logic_type -> bool   val isLogicPointerType : Cil_types.logic_type -> bool   val isLogicVoidPointerType : Cil_types.logic_type -> bool   val logicCType : Cil_types.logic_type -> Cil_types.typ   val array_to_ptr : Cil_types.logic_type -> Cil_types.logic_type   val typ_to_logic_type : Cil_types.typ -> Cil_types.logic_type   val predicate_of_identified_predicate :     Cil_types.identified_predicate -> Cil_types.predicate   val translate_old_label :     Cil_types.stmt -> Cil_types.predicate -> Cil_types.predicate   val is_C_array : Cil_types.term -> bool   val mk_logic_StartOf : Cil_types.term -> Cil_types.term   val mk_logic_AddrOf :     ?loc:Cil_types.location ->     Cil_types.term_lval -> Cil_types.logic_type -> Cil_types.term   val isLogicPointer : Cil_types.term -> bool   val mk_logic_pointer_or_StartOf : Cil_types.term -> Cil_types.term   val mk_cast :     ?loc:Cil_types.location ->     ?force:bool -> Cil_types.typ -> Cil_types.term -> Cil_types.term   val array_with_range : Cil_types.exp -> Cil_types.term -> Cil_types.term   val remove_logic_coerce : Cil_types.term -> Cil_types.term   val numeric_coerce :     Cil_types.logic_type -> Cil_types.term -> Cil_types.term   val pointer_comparable :     ?loc:Cil_types.location ->     Cil_types.term -> Cil_types.term -> Cil_types.predicate   val points_to_valid_string :     ?loc:Cil_types.location -> Cil_types.term -> Cil_types.predicate   val expr_to_term : cast:bool -> Cil_types.exp -> Cil_types.term   val expr_to_term_coerce : cast:bool -> Cil_types.exp -> Cil_types.term   val lval_to_term_lval : cast:bool -> Cil_types.lval -> Cil_types.term_lval   val host_to_term_host :     cast:bool -> Cil_types.lhost -> Cil_types.term_lhost   val offset_to_term_offset :     cast:bool -> Cil_types.offset -> Cil_types.term_offset   val constant_to_lconstant : Cil_types.constant -> Cil_types.logic_constant   val lconstant_to_constant : Cil_types.logic_constant -> Cil_types.constant   val string_to_float_lconstant : string -> Cil_types.logic_constant   val remove_term_offset :     Cil_types.term_offset -> Cil_types.term_offset * Cil_types.term_offset   val lval_contains_result : Cil_types.term_lhost -> bool   val loffset_contains_result : Cil_types.term_offset -> bool   val contains_result : Cil_types.term -> bool   val get_pred_body : Cil_types.logic_info -> Cil_types.predicate   val is_result : Cil_types.term -> bool   val lhost_c_type : Cil_types.term_lhost -> Cil_types.typ   val is_trivially_true : Cil_types.predicate -> bool   val is_trivially_false : Cil_types.predicate -> bool   val is_same_list : ('-> '-> bool) -> 'a list -> 'a list -> bool   val is_same_logic_label :     Cil_types.logic_label -> Cil_types.logic_label -> bool   val is_same_pconstant :     Logic_ptree.constant -> Logic_ptree.constant -> bool   val is_same_type : Cil_types.logic_type -> Cil_types.logic_type -> bool   val is_same_var : Cil_types.logic_var -> Cil_types.logic_var -> bool   val is_same_logic_signature :     Cil_types.logic_info -> Cil_types.logic_info -> bool   val is_same_logic_profile :     Cil_types.logic_info -> Cil_types.logic_info -> bool   val is_same_builtin_profile :     Cil_types.builtin_logic_info -> Cil_types.builtin_logic_info -> bool   val is_same_logic_ctor_info :     Cil_types.logic_ctor_info -> Cil_types.logic_ctor_info -> bool   val is_same_constant : Cil_types.constant -> Cil_types.constant -> bool   val is_same_term : Cil_types.term -> Cil_types.term -> bool   val is_same_logic_info :     Cil_types.logic_info -> Cil_types.logic_info -> bool   val is_same_logic_body :     Cil_types.logic_body -> Cil_types.logic_body -> bool   val is_same_indcase :     string * Cil_types.logic_label list * string list * Cil_types.predicate ->     string * Cil_types.logic_label list * string list * Cil_types.predicate ->     bool   val is_same_tlval : Cil_types.term_lval -> Cil_types.term_lval -> bool   val is_same_lhost : Cil_types.term_lhost -> Cil_types.term_lhost -> bool   val is_same_offset : Cil_types.term_offset -> Cil_types.term_offset -> bool   val is_same_predicate_node :     Cil_types.predicate_node -> Cil_types.predicate_node -> bool   val is_same_predicate : Cil_types.predicate -> Cil_types.predicate -> bool   val is_same_identified_predicate :     Cil_types.identified_predicate -> Cil_types.identified_predicate -> bool   val is_same_identified_term :     Cil_types.identified_term -> Cil_types.identified_term -> bool   val is_same_deps :     Cil_types.identified_term Cil_types.deps ->     Cil_types.identified_term Cil_types.deps -> bool   val is_same_allocation :     Cil_types.identified_term Cil_types.allocation ->     Cil_types.identified_term Cil_types.allocation -> bool   val is_same_assigns :     Cil_types.identified_term Cil_types.assigns ->     Cil_types.identified_term Cil_types.assigns -> bool   val is_same_variant :     Cil_types.term Cil_types.variant ->     Cil_types.term Cil_types.variant -> bool   val is_same_post_cond :     Cil_types.termination_kind * Cil_types.identified_predicate ->     Cil_types.termination_kind * Cil_types.identified_predicate -> bool   val is_same_behavior :     Cil_types.funbehavior -> Cil_types.funbehavior -> bool   val is_same_spec : Cil_types.funspec -> Cil_types.funspec -> bool   val is_same_logic_type_def :     Cil_types.logic_type_def -> Cil_types.logic_type_def -> bool   val is_same_logic_type_info :     Cil_types.logic_type_info -> Cil_types.logic_type_info -> bool   val is_same_loop_pragma :     Cil_types.term Cil_types.loop_pragma ->     Cil_types.term Cil_types.loop_pragma -> bool   val is_same_slice_pragma :     Cil_types.term Cil_types.slice_pragma ->     Cil_types.term Cil_types.slice_pragma -> bool   val is_same_impact_pragma :     Cil_types.term Cil_types.impact_pragma ->     Cil_types.term Cil_types.impact_pragma -> bool   val is_same_pragma :     Cil_types.term Cil_types.pragma ->     Cil_types.term Cil_types.pragma -> bool   val is_same_code_annotation :     Cil_types.code_annotation -> Cil_types.code_annotation -> bool   val is_same_global_annotation :     Cil_types.global_annotation -> Cil_types.global_annotation -> bool   val is_same_axiomatic :     Cil_types.global_annotation list ->     Cil_types.global_annotation list -> bool   val is_same_model_info :     Cil_types.model_info -> Cil_types.model_info -> bool   val is_same_lexpr : Logic_ptree.lexpr -> Logic_ptree.lexpr -> bool   val hash_term : Cil_types.term -> int   val compare_term : Cil_types.term -> Cil_types.term -> int   val get_behavior_names : Cil_types.spec -> string list   val concat_assigns :     Cil_types.identified_term Cil_types.assigns ->     Cil_types.identified_term Cil_types.assigns ->     Cil_types.identified_term Cil_types.assigns   val merge_assigns :     Cil_types.identified_term Cil_types.assigns ->     Cil_types.identified_term Cil_types.assigns ->     Cil_types.identified_term Cil_types.assigns   val concat_allocation :     Cil_types.identified_term Cil_types.allocation ->     Cil_types.identified_term Cil_types.allocation ->     Cil_types.identified_term Cil_types.allocation   val merge_allocation :     Cil_types.identified_term Cil_types.allocation ->     Cil_types.identified_term Cil_types.allocation ->     Cil_types.identified_term Cil_types.allocation   val merge_behaviors :     silent:bool ->     Cil_types.funbehavior list ->     Cil_types.funbehavior list -> Cil_types.funbehavior list   val merge_funspec :     ?silent_about_merging_behav:bool ->     Cil_types.funspec -> Cil_types.funspec -> unit   val clear_funspec : Cil_types.funspec -> unit   val is_assert : Cil_types.code_annotation -> bool   val is_contract : Cil_types.code_annotation -> bool   val is_stmt_invariant : Cil_types.code_annotation -> bool   val is_loop_invariant : Cil_types.code_annotation -> bool   val is_invariant : Cil_types.code_annotation -> bool   val is_variant : Cil_types.code_annotation -> bool   val is_assigns : Cil_types.code_annotation -> bool   val is_pragma : Cil_types.code_annotation -> bool   val is_loop_pragma : Cil_types.code_annotation -> bool   val is_slice_pragma : Cil_types.code_annotation -> bool   val is_impact_pragma : Cil_types.code_annotation -> bool   val is_loop_annot : Cil_types.code_annotation -> bool   val is_trivial_annotation : Cil_types.code_annotation -> bool   val is_property_pragma : Cil_types.term Cil_types.pragma -> bool   val extract_loop_pragma :     Cil_types.code_annotation list ->     Cil_types.term Cil_types.loop_pragma list   val extract_contract :     Cil_types.code_annotation list -> (string list * Cil_types.funspec) list   val constFoldTermToInt :     ?machdep:bool -> Cil_types.term -> Integer.t option   class simplify_const_lval :     (Cil_types.varinfo -> Cil_types.init option) -> Cil.cilVisitor   val complete_types : Cil_types.file -> unit   val register_extension : string -> unit   val is_extension : string -> bool   val kw_c_mode : bool Pervasives.ref   val enter_kw_c_mode : unit -> unit   val exit_kw_c_mode : unit -> unit   val is_kw_c_mode : unit -> bool   val rt_type_mode : bool Pervasives.ref   val enter_rt_type_mode : unit -> unit   val exit_rt_type_mode : unit -> unit   val is_rt_type_mode : unit -> bool end