M (soteria-c.Soteria_c

Parameters

module State : State_intf.S

Signature

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:Agv.t list ->
  (Agv.t, Error.with_trace, State.syn list) SM.Result.t

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

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

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

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

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

val assert_ : 
  args:Agv.t list ->
  ([> Soteria__Bv_values__Typed.T.zero ] Soteria__Bv_values__Typed.t Agv.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:Agv.t list ->
  ([> Soteria__Bv_values__Typed.T.zero ] Soteria__Bv_values__Typed.t Agv.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 Agv.agv list ->
  ([> Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t Agv.agv,
    Error.with_trace,
    State.syn list)
    Soteria.Symex.Compo_res.t
    SM.t

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

val havoc : 
  return_ty:Soteria_c_lib.Layout.CF.Ctype.ctype option ->
  args:Agv.T.cval Typed.t Agv.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

HACK: Some internal functions such as __builtin___memcpy_chk are not needed in our tool, since we perform all checks. For this function, we return the real implementation (here, memcpy), with a filter saying that the last argument should be elided. See: https://gcc.gnu.org/onlinedocs/gcc-4.3.0/gcc/Object-Size-Checking.html

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

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

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