Ail_helpers (soteria-c.Soteria_c_lib.Ail

type Stdlib.Effect.t +=

| Get_prog : Ail_tys.linked_program Stdlib.Effect.t

val get_prog : unit -> Ail_tys.linked_program

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

val sym_is_id : Cerb_frontend.Symbol.sym -> string -> bool

val pp_sym_hum : Stdlib.Format.formatter -> Cerb_frontend.Symbol.sym -> unit

val resolve_sym : 
  ?prog:Ail_tys.linked_program ->
  Cerb_frontend.Symbol.sym ->
  Cerb_frontend.Symbol.sym

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

val get_return_ty : 
  Cerb_frontend.Symbol.sym ->
  Cerb_frontend.Ctype.ctype option

val find_fun_name : 
  prog: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))
    option

val find_fun_loc : Cerb_frontend.Symbol.sym -> Cerb_location.t option

val find_fun_def : 
  Cerb_frontend.Symbol.sym ->
  Cerb_frontend.GenTypes.genTypeCategory
    Cerb_frontend.AilSyntax.sigma_function_definition
    option

val find_obj_def : 
  prog:Ail_tys.linked_program ->
  Cerb_frontend.Symbol.sym ->
  Cerb_frontend.GenTypes.genTypeCategory Cerb_frontend.AilSyntax.expression
    option

val find_obj_decl : 
  prog:Ail_tys.linked_program ->
  Cerb_frontend.Symbol.sym ->
  ((Cerb_frontend.AilSyntax.storageDuration * bool)
   * Cerb_frontend.Ctype.alignment option
   * Cerb_frontend.Ctype.qualifiers
   * Cerb_frontend.Ctype.ctype)
    option

val sure_side_effect_free : Ail_tys.expr -> bool

Returns true if the expression is guaranteed to be side-effect free.

val cerb_loc_to_yojson : 
  Cerb_location.t ->
  [> `List of [> `List of [> `Int of int ] list ] list ]

val yojson_loc_to_range : Yojson.Safe.t -> Linol.Lsp.Types.Range.t

val cerb_loc_to_range : Cerb_location.t -> Linol.Lsp.Types.Range.t