Frama-C API - `Make`

Parameters

module Compiler : Sigs.Compiler

Signature

module Cfg : CfgCompiler.Cfg with module S = Compiler.M.Sigma

type node = Cfg.node

type goal = {

goal_pred : Cfg.P.t;
goal_prop : WpPropId.prop_id;

}

type cfg = Cfg.cfg

type paths = {

paths_cfg : cfg;
paths_goals : goal Frama_c_kernel.Bag.t;

}

val goals_nodes : goal Frama_c_kernel.Bag.t -> Cfg.Node.Set.t

exception LabelNotFound of Clabels.c_label

Compilation environment

type env

val empty_env : Frama_c_kernel.Kernel_function.t -> env

val bind : Clabels.c_label -> node -> env -> env

val result : env -> Lang.F.var

val (@^) : paths -> paths -> paths

Same as Cfg.concat

val (@*) : env -> (Clabels.c_label * node) list -> env

fold bind

val (@:) : env -> Clabels.c_label -> node

LabelMap.find with refined excpetion.

raises LabelNotFound
instead of Not_found

val (@-) : env -> (Clabels.c_label -> bool) -> env

val sequence : (env -> 'a -> paths) -> env -> 'a list -> paths

Chain compiler by introducing fresh nodes between each element of the list. For each consecutive x;y elements, a fresh node n is created, and x is compiled with Next:n and y is compiled with Here:n.

val choice : ?pre:Clabels.c_label -> ?post:Clabels.c_label -> (env -> 'a -> paths) -> env -> 'a list -> paths

Chain compiler in parallel, between labels ~pre and ~post, which defaults to resp. here and next. The list of eventualities is exhastive, hence an either assumption is also inserted.

val parallel : ?pre:Clabels.c_label -> ?post:Clabels.c_label -> (env -> 'a -> Cfg.C.t * paths) -> env -> 'a list -> paths

Chain compiler in parallel, between labels ~pre and ~post, which defaults to resp. here and next. The list of eventualities is exhastive, hence an either assumption is also inserted.

Instructions Compilation

Each instruction or statement is typically compiled between Here and Next nodes in the flow. Pre, Post and Exit are reserved for the entry and exit points of current function. in flow are used when needed such as Break and Continue and should be added before calling.

val set : env -> Frama_c_kernel.Cil_types.lval -> Frama_c_kernel.Cil_types.exp -> paths

val scope : env -> Sigs.scope -> Frama_c_kernel.Cil_types.varinfo list -> paths

val instr : env -> Frama_c_kernel.Cil_types.instr -> paths

val return : env -> Frama_c_kernel.Cil_types.exp option -> paths

val assume : Cfg.P.t -> paths

val call_kf : env -> Frama_c_kernel.Cil_types.lval option -> Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.exp list -> paths

val call : env -> Frama_c_kernel.Cil_types.lval option -> Frama_c_kernel.Cil_types.exp -> Frama_c_kernel.Cil_types.exp list -> paths

ACSL Compilation

val spec : env -> Frama_c_kernel.Cil_types.spec -> paths

val assume_ : env -> Sigs.polarity -> Frama_c_kernel.Cil_types.predicate -> paths

val assigns : env -> Frama_c_kernel.Cil_types.assigns -> paths

val froms : env -> Frama_c_kernel.Cil_types.from list -> paths

Automata Compilation

val automaton : env -> Frama_c_kernel.Interpreted_automata.automaton -> paths

val init : is_pre_main:bool -> env -> paths

val compute_kf : Frama_c_kernel.Kernel_function.t -> paths * node

Full Compilation

Returns the set of all paths for the function, with all proof obligations. The returned node corresponds to the Init label.