Module C2Codex.Make

Parameters

Signature

val exploring_pure_function : bool Stdlib.ref
val exp_to_value : (Frama_c_kernel.Cil_types.kinstr * Frama_c_kernel.Cil_types.exp) -> string Stdlib.Hashtbl.Make(CallingContext).t
val exp_has_value : (Frama_c_kernel.Cil_types.kinstr * Frama_c_kernel.Cil_types.exp) -> bool
val iter_on_alarms : (Frama_c_kernel.Alarms.t -> Frama_c_kernel.Cil_types.location -> Codex.Lattices.Quadrivalent.t -> unit) -> unit

Iterate on all registered alarms.

val reset_alarms : unit -> unit

Delete all the registered alarms, use only if you know what you are doing

val reset_assertions : unit -> unit

Delete all the registered assertions, use only if you know what you are doing

val iter_on_assertions : (Frama_c_kernel.Cil_types.location -> string -> string -> unit) -> unit

Iterate f on all registered assertions. f receives the location of the assertion, and strings indicating the status and method to solve the assertion.

type context = {
  1. loop_nesting_level : int;
  2. kinstr : Frama_c_kernel.Cil_types.kinstr;
  3. ctx : Domain.Context.t;
}
type state = {
  1. mem : Domain.memory;
  2. var_addresses : Domain.binary VarMap.t;
  3. string_addresses : Domain.binary StringMap.t;
  4. context : context;
}
val block_entry : state -> Frama_c_kernel.Cil_types.block -> state
val block_close : state -> Frama_c_kernel.Cil_types.block -> state
type funcall = Frama_c_kernel.Kernel_function.t -> (Units.In_bits.t * Domain.binary) list -> state -> (Units.In_bits.t * Domain.binary) option * state option
val analyze_summary : Types.TypedC.typ -> (Units.In_bits.t * Domain.binary) list -> state -> (Units.In_bits.t * Domain.binary) option * state
val init_function_args : state -> Frama_c_kernel.Kernel_function.t -> (Units.In_bits.t * Domain.binary) list -> state
val free_function_args : state -> Frama_c_kernel.Kernel_function.t -> state
val instruction : funcall:funcall -> Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Cil_types.instr -> state -> state option
type return_result =
  1. | Return_fails
  2. | Return_result of {
    1. return_state : state;
    2. return_value : (Units.In_bits.t * Domain.binary) option;
    }

Result of the analysis of a return instruction:

  • Return_fails means that the execution always trigger an undefined behaviour (e.g. return 1/0).
  • Return_result{state;return_value=None} is for return; statements;
  • Return_result{state;return_value=(size,value)} is for return value; statements, where size=8*sizeof(value) (i.e. the size of value in bits).
type ret_transition =
  1. | State of state option
  2. | Return of return_result

Transitions can be a regular instruction or a return instruction:

  • return instructions return a return_result;
  • normal instruction return (State None) when the result is Bottom, or State(Some _) otherwise.
val transition : funcall:funcall -> Frama_c_kernel.Interpreted_automata.vertex Frama_c_kernel.Interpreted_automata.transition -> state -> ret_transition
val cond_node : Frama_c_kernel.Cil_types.exp -> state -> (Domain.boolean * state) option
val expression : Frama_c_kernel.Cil_types.exp -> state -> (Domain.binary * state) option
val initial_state_ret : Frama_c_kernel.Kernel_function.t -> CallingContext.t -> state option * (Units.In_bits.t * Domain.binary) list * Types.TypedC.typ

initial_state_ret kf root receives a kernel function and the root calling context, and returns the initial state, the arguments and the expected return type.

val pretty_state : Stdlib.Format.formatter -> state -> unit
val pretty_state_option : Stdlib.Format.formatter -> state option -> unit