Stubs (soteria-c.Soteria_c_lib.Driver.Wpst

module SM : sig ... end

val error : 
  'a ->
  ('b, 'a * Cerb_location.t Soteria.Terminal.Call_trace.t, 'c)
    Soteria.Symex.Compo_res.t
    SM.t

val not_impl : string -> 'a SM.t

val of_opt_not_impl : msg:string -> 'a option -> 'a SM.t

type 'err fun_exec =
  args:Aggregate_val.t list ->
  (Aggregate_val.t, Error.with_trace, SState.syn list) SM.Result.t

val failed_alloc_case : 
  unit ->
  (unit ->
    ([> Soteria__Bv_values__Typed.T.sptr ] Soteria__Bv_values__Typed.t
       Aggregate_val.agv,
      'a,
      'b)
      SM.Result.t)
    list

val malloc : 
  args:Aggregate_val.t list ->
  ([> Soteria__Bv_values__Typed.T.sptr ] Typed.t Aggregate_val.agv,
    Error.with_trace,
    SState.syn list)
    Soteria.Symex.Compo_res.t
    SM.t

val calloc : 
  args:Aggregate_val.t list ->
  ([> Soteria__Bv_values__Typed.T.sptr ] Typed.t Aggregate_val.agv,
    Error.with_trace,
    SState.syn list)
    Soteria.Symex.Compo_res.t
    SM.t

val free : 
  args:Aggregate_val.t list ->
  ([> Soteria__Bv_values__Typed.T.zero ] Soteria__Bv_values__Typed.t
     Aggregate_val.agv,
    Error.with_trace,
    SState.syn list)
    Soteria.Symex.Compo_res.t
    SM.t

val memcpy : 
  args:Aggregate_val.t list ->
  ('a Typed.t Aggregate_val.agv, Error.with_trace, SState.syn list)
    Soteria.Symex.Compo_res.t
    SM.t

val assert_ : 
  args:Aggregate_val.t list ->
  ([> Soteria__Bv_values__Typed.T.zero ] Soteria__Bv_values__Typed.t
     Aggregate_val.agv,
    [> `FailedAssert ] * Cerb_location.t Soteria.Terminal.Call_trace.t,
    'a)
    Soteria.Symex.Compo_res.t
    SM.t

val assert_fail : 
  args:'a ->
  ('b, [> `FailedAssert ] * Cerb_location.t Soteria.Terminal.Call_trace.t, 'c)
    Soteria.Symex.Compo_res.t
    SM.t

val assume_ : 
  args:Aggregate_val.t list ->
  ([> Soteria__Bv_values__Typed.T.zero ] Soteria__Bv_values__Typed.t
     Aggregate_val.agv,
    'a,
    'b)
    Soteria.Symex.Compo_res.t
    SM.t

val nondet : 
  Soteria_c_lib.Layout.CF.Ctype.ctype_ ->
  args:'a ->
  (Soteria_c_lib.Layout.Agv.t, 'b, 'c) Soteria.Symex.Compo_res.t SM.t

val strcmp : 
  args:'a Typed.t Aggregate_val.agv list ->
  ([> Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t
     Aggregate_val.agv,
    Error.with_trace,
    SState.syn list)
    Soteria.Symex.Compo_res.t
    SM.t

val memset : 
  args:'a Typed.t Aggregate_val.agv list ->
  ([> Soteria__Bv_values__Typed.T.zero ] Soteria__Bv_values__Typed.t
     Aggregate_val.agv,
    Error.with_trace,
    SState.syn list)
    Soteria.Symex.Compo_res.t
    SM.t

val havoc : 
  return_ty:Soteria_c_lib.Layout.CF.Ctype.ctype option ->
  args:Soteria_c_lib.Aggregate_val.T.cval Typed.t Aggregate_val.agv list ->
  (Soteria_c_lib.Layout.Agv.t, 'a, 'b) Soteria.Symex.Compo_res.t SM.t

val vanish_fn : args:'a -> 'b SM.t

module Arg_filter : sig ... end

val with_cbmc_support : 
  ((args:Aggregate_val.t list ->
   (Aggregate_val.t, Error.with_trace, SState.syn list) SM.Result.t)
   * Arg_filter.t) ->
  ((args:Aggregate_val.t list ->
   (Aggregate_val.t, Error.with_trace, SState.syn list) SM.Result.t)
   * Arg_filter.t)
    option

val with_testcomp_support : 
  ((args:Aggregate_val.t list ->
   (Aggregate_val.t, Error.with_trace, SState.syn list) SM.Result.t)
   * Arg_filter.t) ->
  ((args:Aggregate_val.t list ->
   (Aggregate_val.t, Error.with_trace, SState.syn list) SM.Result.t)
   * Arg_filter.t)
    option

val find_stub : 
  Cerb_frontend.Symbol.sym ->
  ('err fun_exec * Arg_filter.t) option