Driver (soteria-c.Soteria_c

module Call_trace = Soteria.Terminal.Call_trace

module SState = State

module Wpst_interp : sig ... end

exception Tool_error

val tool_error : string -> 'a

val with_tool_errors_caught : 
  unit ->
  (unit -> Error.Exit_code.t) ->
  Error.Exit_code.t

val default_wpst_fuel : Soteria.Symex.Fuel_gauge.t

val as_nonempty_list : 'a list -> 'a list option

val impl_name : string

val set_cerb_conf : unit -> unit

val io : Cerb_backend.Pipeline.io_helpers

module Frontend : sig ... end

val parse_ail_raw_default : 
  includes:string list ->
  string ->
  (Cerb_frontend.GenTypes.genTypeCategory Cerb_frontend.AilSyntax.ail_program,
    [> `ParsingError of string ] * Cerb_location.t Call_trace.t)
    Stdlib.result

val parse_and_link_ail : 
  includes:string list ->
  string list ->
  (Ail_tys.linked_program,
    [> `LinkError of string | `ParsingError of string ]
    * Cerb_location.t Call_trace.t)
    Stdlib.result

val parse_compilation_item : 
  Compilation_database.cmd ->
  (Cerb_frontend.GenTypes.genTypeCategory Cerb_frontend.AilSyntax.ail_program,
    [> `ParsingError of string ] * Cerb_location.t Call_trace.t)
    Stdlib.result

val is_main : Cerb_frontend.Cabs.function_definition -> bool

val pp_err_and_call_trace : 
  Stdlib.Format.formatter ->
  ([< `DivisionByZero
   | `DoubleFree
   | `FailedAssert
   | `Gave_up of string
   | `InvalidFree
   | `InvalidFunctionPtr
   | `LinkError of string
   | `Memory_leak
   | `NullDereference
   | `OutOfBounds
   | `Overflow
   | `ParsingError of string
   | `UBPointerArithmetic
   | `UBPointerComparison
   | `UninitializedMemoryAccess
   | `UseAfterFree ]
   * Cerb_location.t Call_trace.element list) ->
  unit

val resolve_function : 
  Ail_tys.linked_program ->
  string ->
  (Cerb_frontend.Symbol.sym
   * (Cerb_location.t
      * int
      * Cerb_frontend.Annot.attributes
      * Cerb_frontend.AilSyntax.ail_identifier list
      * Cerb_frontend.GenTypes.genTypeCategory
          Cerb_frontend.AilSyntax.statement),
    [> `ParsingError of string ] * 'a Call_trace.t)
    Soteria.Soteria_std.Result.t

val with_function_context : Ail_tys.linked_program -> (unit -> 'a) -> 'a

val exec_function : 
  includes:string list ->
  fuel:Soteria.Symex.Fuel_gauge.t ->
  string list ->
  string ->
  ((Aggregate_val.t * Wpst_interp.InterpM.StateM.st,
     (Error.with_trace * Wpst_interp.InterpM.StateM.st)
       Soteria.Symex.Or_gave_up.t,
     SState.syn list)
     Soteria.Symex.Compo_res.t
   * Soteria.Bv_values.Bv_solver.Z3_solver.Value.sbool
       Soteria.Bv_values.Bv_solver.Z3_solver.Value.t
       list)
    list

val temp_file : string lazy_t

val generate_errors : string -> (Error.t * Cerb_location.t Call_trace.t) list

Entry points

val initialise : 
  ?soteria_config:Soteria.Config.t ->
  Config.mode ->
  Config.t ->
  (unit -> 'a) ->
  'a

val print_states : 
  (('a Typed.t Aggregate_val.agv * SState.t option,
     (([< `DivisionByZero
       | `DoubleFree
       | `FailedAssert
       | `Gave_up of string
       | `InvalidFree
       | `InvalidFunctionPtr
       | `LinkError of string
       | `Memory_leak
       | `NullDereference
       | `OutOfBounds
       | `Overflow
       | `ParsingError of string
       | `UBPointerArithmetic
       | `UBPointerComparison
       | `UninitializedMemoryAccess
       | `UseAfterFree ]
       * Cerb_location.t Call_trace.element list)
      * SState.t option)
       Soteria.Symex.Or_gave_up.t,
     SState.syn list)
     Soteria.Symex.Compo_res.t
   * 'b)
    list ->
  unit

val exec_and_print : 
  Soteria.Config.t ->
  Config.t ->
  (Soteria__Symex__Fuel_gauge.t, string) Stdlib.result ->
  string list ->
  string list ->
  string ->
  Error.Exit_code.t

val dump_report : Yojson.Safe.t list -> unit

val dump_summaries : 
  (Cerb_frontend.Symbol.sym * 'a Summary.t list) list ->
  unit

val analyse_summaries : 
  (Ail_tys.sym * 'a Summary.t list) list ->
  (Ail_tys.sym * Summary.analysed Summary.t list) list

val generate_summaries : 
  functions_to_analyse:string list option ->
  Ail_tys.linked_program ->
  Error.Exit_code.t

val lsp : Config.t -> unit -> Error.Exit_code.t

val show_ail : 
  Soteria.Config.t ->
  Config.t ->
  string list ->
  string list ->
  Error.Exit_code.t

val generate_all_summaries : 
  Soteria.Config.t ->
  Config.t ->
  string list ->
  string list ->
  string list ->
  Error.Exit_code.t

val linked_prog_of_db : string -> Ail_tys.linked_program

val capture_db : 
  Soteria.Config.t ->
  Config.t ->
  string ->
  string list ->
  Error.Exit_code.t