Wpst_interp (soteria-c.Soteria_c_lib.Driver.Wpst

module InterpM : sig ... end

module Stubs : sig ... end

exception Unsupported of string * Cerb_location.t

val type_of : 
  Cerb_frontend.GenTypes.genTypeCategory Cerb_frontend.AilSyntax.expression ->
  Cerb_frontend.Ctype.ctype

val unwrap_ctype : 
  Soteria_c_lib__Interp.Ctype.ctype ->
  Soteria_c_lib__Interp.Ctype.ctype_

val pointer_inner : 
  Soteria_c_lib__Interp.Ctype.ctype ->
  Soteria_c_lib__Interp.Ctype.ctype option

type state = SState.t

val cast_aggregate_to_ptr : Aggregate_val.t -> [ `Ptr ] Typed.t Csymex.t

val cast_to_int : 
  [< Soteria_c_lib.Typed.T.cval ] Typed.t ->
  [> Soteria__Bv_values__Typed.T.sint ] Typed.t Csymex.t

val cast_aggregate_to_int : 
  Aggregate_val.t ->
  [> Soteria__Bv_values__Typed.T.sint ] Typed.t Csymex.t

val cast_to_bool : 
  [< Soteria_c_lib.Typed.T.cval ] Typed.t ->
  [> Typed.sbool ] Typed.t Csymex.t

val cast_aggregate_to_bool : 
  Aggregate_val.t ->
  [> Typed.sbool ] Typed.t Csymex.t

type fun_exec =
  args:Aggregate_val.t list ->
  (Aggregate_val.t, Error.with_trace, SState.syn list) InterpM.StateM.Result.t

val get_param_tys : 
  Cerb_frontend.Symbol.sym ->
  Cerb_frontend.Ctype.ctype list Csymex.t

val fold_bindings : 
  Soteria_c_lib__Interp.AilSyntax.bindings ->
  init:'a ->
  f:
    ('a ->
      (Soteria_c_lib__Interp.AilSyntax.ail_identifier
       * Cerb_frontend.Ctype.ctype) ->
      'a) ->
  'a

val try_with_unsupported : (Store.t -> Store.t) -> unit InterpM.t

val attach_bindings : 
  Soteria_c_lib__Interp.AilSyntax.bindings ->
  unit InterpM.t

val remove_bindings : 
  Soteria_c_lib__Interp.AilSyntax.bindings ->
  unit InterpM.t

val free_bindings : Soteria_c_lib__Interp.AilSyntax.bindings -> unit InterpM.t

val pp_bindings : Soteria_c_lib__Interp.AilSyntax.bindings Fmt.t

val remove_and_free_bindings : 
  Soteria_c_lib__Interp.AilSyntax.bindings ->
  unit InterpM.t

val mk_store : 
  (Cerb_frontend.Symbol.sym * Ail_tys.ctype * Aggregate_val.t) list ->
  Store.t

val dealloc_store : unit -> unit InterpM.t

val get_stack_address : 
  Ail_tys.sym ->
  Soteria_c_lib.Typed.T.sptr Typed.t option InterpM.t

val try_immediate_load : 
  'a Soteria_c_lib__Interp.AilSyntax.expression ->
  (Aggregate_val.t option, Error.with_trace, SState.syn list)
    InterpM.SSM.Result.t

val try_immediate_store : 
  'a Soteria_c_lib__Interp.AilSyntax.expression ->
  Aggregate_val.t ->
  [> `NotImmediate | `Success ] InterpM.t

val aggregate_of_constant_exn : 
  loc:Cerb_location.t ->
  ty:Soteria_c_lib__Interp.Ctype.ctype ->
  Ail_tys.constant ->
  Aggregate_val.t

val aggregate_of_constant : 
  ty:Soteria_c_lib__Interp.Ctype.ctype ->
  Ail_tys.constant ->
  Aggregate_val.t Csymex.t

val unwrap_expr : 
  Ail_tys.expr ->
  Cerb_frontend.GenTypes.genTypeCategory Cerb_frontend.AilSyntax.expression_

val cast_basic : 
  old_ty:Soteria_c_lib__Interp.Ctype.ctype ->
  new_ty:Soteria_c_lib__Interp.Ctype.ctype ->
  Soteria_c_lib.Typed.T.cval Typed.t ->
  'a Typed.t Csymex.t

val cast : 
  old_ty:Soteria_c_lib__Interp.Ctype.ctype ->
  new_ty:Soteria_c_lib__Interp.Ctype.ctype ->
  Aggregate_val.t ->
  Aggregate_val.t Csymex.t

val equality_check : 
  ty:Soteria_c_lib__Interp.Ctype.ctype ->
  (Soteria_c_lib.Typed.T.cval Typed.t * Soteria_c_lib__Interp.Ctype.ctype) ->
  (Soteria_c_lib.Typed.T.cval Typed.t * Soteria_c_lib__Interp.Ctype.ctype) ->
  [> Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t InterpM.t

val aggregate_equality_check : 
  ty:Soteria_c_lib__Interp.Ctype.ctype ->
  (Soteria_c_lib.Typed.T.cval Typed.t Aggregate_val.agv
   * Soteria_c_lib__Interp.Ctype.ctype) ->
  (Soteria_c_lib.Typed.T.cval Typed.t Aggregate_val.agv
   * Soteria_c_lib__Interp.Ctype.ctype) ->
  [> Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t InterpM.t

val arith_add : 
  signed:bool ->
  ([< Soteria_c_lib.Typed.T.cval ] as 'a) Typed.t ->
  'a Typed.t ->
  ([> `NonZero | `Ptr | `Zero ] Soteria__Bv_values__Typed.t,
    Error.with_trace,
    SState.syn list)
    InterpM.SSM.Result.t

val arith_sub : 
  signed:bool ->
  [< Soteria_c_lib.Typed.T.cval ] Typed.t ->
  [< Soteria_c_lib.Typed.T.cval ] Typed.t ->
  ([> `NonZero | `Ptr | `Zero ] Soteria__Bv_values__Typed.t,
    Error.with_trace,
    SState.syn list)
    InterpM.SSM.Result.t

val arith_mul : 
  signed:bool ->
  [< Soteria_c_lib.Typed.T.cval ] Typed.t ->
  [< Soteria_c_lib.Typed.T.cval ] Typed.t ->
  ([> Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t,
    Error.with_trace,
    SState.syn list)
    InterpM.SSM.Result.t

val arith : 
  Soteria_c_lib__Interp.Ctype.ctype ->
  (Soteria_c_lib.Typed.T.cval Typed.t * Soteria_c_lib__Interp.Ctype.ctype) ->
  Soteria_c_lib__Interp.AilSyntax.arithmeticOperator ->
  (Soteria_c_lib.Typed.T.cval Typed.t * Soteria_c_lib__Interp.Ctype.ctype) ->
  [> `Float | `NonZero | `Ptr | `Zero ] Typed.t InterpM.t

val try_immediate_postfix_op : 
  apply_op:
    (Aggregate_val.t ->
      (Aggregate_val.t, Error.with_trace, SState.syn list) InterpM.SSM.Result.t) ->
  'a Soteria_c_lib__Interp.AilSyntax.expression ->
  (Aggregate_val.t option, Error.with_trace, SState.syn list)
    InterpM.SSM.Result.t

val ineq_comparison : 
  int_cmp_op:
    ([> Soteria__Bv_values__Typed.T.sint ] Typed.t ->
      [> Soteria__Bv_values__Typed.T.sint ] Typed.t ->
      [< Soteria__Bv_values__Typed.sbool ] Soteria__Bv_values__Typed.t) ->
  float_cmp_op:
    ('a Typed.t ->
      'b Typed.t ->
      [< Soteria__Bv_values__Typed.sbool ] Soteria__Bv_values__Typed.t) ->
  'c Typed.t Aggregate_val.agv ->
  'd Typed.t Aggregate_val.agv ->
  ([> Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t
     Aggregate_val.agv,
    Error.with_trace,
    SState.syn list)
    InterpM.SSM.Result.t

module Stmt_exec_result : sig ... end

val resolve_function : 
  Cerb_frontend.GenTypes.genTypeCategory
    Soteria_c_lib__Interp.AilSyntax.expression ->
  (fun_exec * Ail_tys.ctype list option * Stubs.Arg_filter.t) InterpM.t

val eval_expr_list : 
  Ail_tys.expr list ->
  (Aggregate_val.t list, Error.with_trace, SState.syn list)
    InterpM.SSM.Result.t

val eval_expr : 
  Ail_tys.expr ->
  (Aggregate_val.t, Error.with_trace, SState.syn list) InterpM.SSM.Result.t

val exec_body : 
  ret_ty:Soteria_c_lib__Interp.Ctype.ctype option ->
  Ail_tys.stmt ->
  Aggregate_val.t InterpM.t

val exec_stmt_list : 
  Stmt_exec_result.t ->
  Ail_tys.stmt list ->
  Stmt_exec_result.t InterpM.t

val exec_goto : Ail_tys.sym -> Ail_tys.stmt -> Stmt_exec_result.t InterpM.t

val exec_case : 
  Soteria_c_lib.Typed.T.sint Typed.t ->
  Ail_tys.stmt ->
  Stmt_exec_result.t InterpM.t

val exec_stmt : Ail_tys.stmt -> Stmt_exec_result.t InterpM.t

val exec_fun : Ail_tys.fundef -> fun_exec

val init_prog_state : 
  Ail_tys.linked_program ->
  (unit, Error.with_trace, SState.syn list) InterpM.StateM.Result.t