sig
  module Command :
    sig
      type statement =
        BlastCSystemDescr.C_Command.statement =
          Expr of Ast.Expression.expression
        | Return of Ast.Expression.expression
      and command =
        BlastCSystemDescr.C_Command.command =
          Skip
        | Block of statement list
        | Pred of Ast.Predicate.predicate
        | FunctionCall of Ast.Expression.expression
        | Havoc of Ast.Expression.lval
        | HavocAll
        | Phi of Ast.Expression.lval * bool
      and t =
        BlastCSystemDescr.C_Command.t = {
        code : command;
        read : Ast.Expression.lval list;
        written : Ast.Expression.lval list;
      } 
      val print : Format.formatter -> t -> unit
      val to_string : t -> string
    end
  type location = BlastCSystemDescr.C_System_Descr.location
  and edge = BlastCSystemDescr.C_System_Descr.edge
  val skip : Command.t
  val fake_location : location
  val get_source_position : location -> (string * int * int) option
  val print_location : Format.formatter -> location -> unit
  val print_edge : Format.formatter -> edge -> unit
  val location_to_string : location -> string
  val location_coords : location -> int * int
  val edge_to_string : edge -> string
  val edge_to_command : edge -> Command.t
  val get_outgoing_edges : location -> edge list
  val get_ingoing_edges : location -> edge list
  val get_source : edge -> location
  val get_target : edge -> location
  val get_command : edge -> Command.t
  val reads_and_writes_at_edge :
    edge -> Ast.Expression.lval list * Ast.Expression.lval list
  val expression_closure :
    Ast.Expression.expression -> Ast.Expression.expression list
  val iter_global_variables : (Ast.Expression.lval -> unit) -> unit
  val iterate_all_lvals : (Ast.Expression.lval -> unit) -> unit
  val get_type_of_lval : Ast.Expression.lval -> Cil.typ
  val get_type_of_exp : Ast.Expression.expression -> Cil.typ
  val is_array : Ast.Expression.lval -> bool
  val is_ptr : Ast.Expression.lval -> bool
  val is_global : Ast.Expression.lval -> bool
  val can_escape : Ast.Expression.lval -> bool
  val is_a_lock : Ast.Expression.lval -> bool
  val tid : string
  val notTid : string
  val self : string
  exception NoSuchFunctionException of string
  val is_defined : string -> bool
  val lookup_entry_location : string -> location
  val get_location_fname : location -> string
  val list_of_functions : unit -> string list
  val is_loopback : location -> bool
  val isReturn : edge -> bool
  val returnExp : edge -> Ast.Expression.expression
  val isBlock : edge -> bool
  val isPredicate : edge -> bool
  val isFunCall : edge -> bool
  type formals_kind =
    BlastCSystemDescr.C_System_Descr.formals_kind =
      Fixed of string list
    | Variable of string list
  val lookup_locals : string -> string list
  val lookup_formals : string -> formals_kind
  val globals : unit -> string list
  val make_symvar : string -> string -> string
  val get_locations_at_label : string -> location list
  val map_edges : (edge -> 'a) -> 'a list
  val map_edges_fname : (edge -> 'a) -> string -> 'a list
  type callnode =
    BlastCSystemDescr.C_System_Descr.callnode = {
    cnInfo : string;
    cnCallees : (string, callnode) Hashtbl.t;
    cnCallers : (string, callnode) Hashtbl.t;
  } 
  and callgraph = (string, callnode) Hashtbl.t
  val compute_callgraph : unit -> unit
  val get_callgraph : unit -> callgraph
  val get_callers : string -> (string, callnode) Hashtbl.t
  val get_callees : string -> (string, callnode) Hashtbl.t
  val update_callgraph : string -> string -> unit
  val output_callgraph : string -> unit
  val print_callgraph : out_channel -> unit
  val initialize : string list -> unit
  val instrument_with_spec : string -> string -> unit
  val print_system : Format.formatter -> unit -> unit
  val get_cil_files : unit -> Cil.file list
  val get_varinfo : string -> Cil.varinfo
end