Module Soteria_rust_lib.Frontend

exception PluginError of string

Something wrong internally with plugins

exception FrontendError of string

Something wrong during compilation to ULLBC

exception CompilationError of string

Compilation of the code failed at the rustc level

val plugin_err : string -> 'a
val frontend_err : string -> 'a
val compilation_err : string -> 'a
val (/) : string -> string -> string
module Exe : sig ... end

Utilities to run commands

module Cleaner : sig ... end

Simple utility to create and then delete files

module Cmd : sig ... end

Organise commands to send to the Soteria-Rust frontend

module Lib : sig ... end
type entry_point_filter = {
  1. filter : Cmd.entry list;
  2. expect_error : Cmd.entry list;
}
type entry_point = {
  1. fun_decl : Charon.UllbcAst.fun_decl;
  2. expect_error : bool;
  3. fuel : Soteria.Symex.Fuel_gauge.t;
}
type mk_cmd = ?input:string -> output:string -> unit -> Cmd.t
val default : unit -> Cmd.t
val kani : unit -> Cmd.t
val miri : unit -> Cmd.t
val filter_name : Charon.UllbcAst.crate -> Charon.Types.name -> bool

Filters a name, according to the current Config.t.filter and Config.t.exclude settings. If there are no filters, all names are included; otherwise, a name is included if it matches any filter and doesn't match any exclude.

val get_entry_point : entry_point_filter -> Charon.UllbcAst.crate -> Charon.UllbcAst.fun_decl -> entry_point option
val create_using_current_config : unit -> mk_cmd * entry_point_filter
val modify_mk_cmd : ('a -> 'b) -> (?input:'c -> output:'d -> unit -> 'a) -> ?input:'c -> output:'d -> unit -> 'b
val with_entry_points : filter:entry_point_filter -> Charon.UllbcAst.crate -> Charon.UllbcAst.crate * entry_point list
val parse_ullbc_of_file : mk_cmd:mk_cmd -> string -> Charon.UllbcAst.crate

Given a Rust file, parse it into LLBC, using Charon.

val parse_ullbc_of_crate : mk_cmd:mk_cmd -> string -> Charon.UllbcAst.crate

Given a Rust file, parse it into LLBC, using Charon.

val parse_ullbc_raw : mk_cmd:mk_cmd -> [< `Dir of string | `File of string ] -> Charon.UllbcAst.crate
val parse_ullbc : [< `Dir of string | `File of string ] -> Charon.UllbcAst.crate

Given a path, if it's a file will parse the ULLBC of that single file using rustc; otherwise will assume it's a path to a crate and use cargo. Will translate all functions in the crate, without filtering entry-points.

val parse_ullbc_with_entry_points : [< `Dir of string | `File of string ] -> Charon.UllbcAst.crate * entry_point list

Given a path, will check if it has a .rs extension, in which case it will parse the ULLBC of that single file using rustc; otherwise will assume it's a path to a crate and use cargo. Will only start translation from functions considered entry-points.

val compile_all_plugins : unit -> unit