Module `Mlang.Bir_interface`

type bir_function = { func_variable_inputs : unit Mlang.Bir.VariableMap.t; func_constant_inputs : Bir.expression Pos.marked Mlang.Bir.VariableMap.t; func_outputs : unit Mlang.Bir.VariableMap.t; func_conds : Bir.condition_data Mlang.Mir.RuleMap.t; }: Input-output data necessary to interpret a BIR program

val translate_external_conditions : Pos.t Mlang.StrMap.t Pos.marked Mlang.Mir.CatVarMap.t -> Mir.idmap -> Mast.expression Pos.marked list -> Bir.condition_data Mlang.Mir.RuleMap.t: translate_external_conditions idmap conditions translates a series of boolean expressions conditions into M verification conditions ready to be added to a BIR program

val generate_function_all_vars : Bir.program -> bir_function: Function used to generate a bir_function that includes all possible inputs and outputs

val read_function_from_spec : Bir.program -> string -> bir_function: read_function_from_spec program spec_file reads and parses spec_file and extracts all the inputs, outputs and conditions from it.

val read_inputs_from_stdin : bir_function -> Mir.literal Mlang.Bir.VariableMap.t: Given an input-output specification, prompts the user on stdin for the values of the inputs and returns them as a map

val adapt_program_to_function : Bir.program -> bir_function -> Bir.program * int: adapt_program_to_function program io modifies program according to the input-output specification of io