Module Frontend.Cmd

Organise commands to send to the Soteria-Rust frontend

type entry =
  1. | Attrib of string
  2. | Name of string
  3. | Pub
val entry_as_flag : entry -> string list
val entry_matches_fn : Charon.UllbcAst.fun_decl -> entry -> bool
type t = {
  1. charon : string list;
    (*

    Arguments passed to Charon (only when using the Charon frontend)

    *)
  2. obol : string list;
    (*

    Arguments passed to Obol (only when using the Obol frontend)

    *)
  3. features : string list;
    (*

    Features to enable for compilation (as in --cfg)

    *)
  4. rustc : string list;
    (*

    DEPRECATED?: rustc flags. For Cargo we use RUSTFLAGS, but when possible it would be nicer to use the Cargo-specific command (as with features)?

    *)
  5. entry_points : entry list;
    (*

    Functions to mark as entry points, e.g. Attrib "soteriatool::test", when we are interested in filtering the entry-points.

    *)
  6. expect_error : entry list;
    (*

    Markers to know that an entry point is expected to fail. This is used to inverse the outcomes of the execution, so that we can use the same plugin for both expected-success and expected-failure tests.

    *)
}
val make : ?charon:string list -> ?obol:string list -> ?features:string list -> ?rustc:string list -> ?entry_points:entry list -> ?expect_error:entry list -> unit -> t
type mode =
  1. | Cargo
  2. | Rustc
val empty : t
val concat_cmd : t -> t -> t
val frontend_cmd : unit -> string
val toolchain_path : string lazy_t
val cargo : unit -> string
val rustc : unit -> string
val rustc_as_env : unit -> string list
val current_rustc_flags : unit -> string list
val is_crate_type_flag : string -> bool
val is_edition_flag : string -> bool
val flags_for_cargo : string list -> string list
val flags_as_rustc_env : string list -> string list
val build_cmd : mode:mode -> t -> string * string list * string list
val exec_in : mode:mode -> string -> t -> string list * string list * Unix.process_status