Functor Wp.StmtSemantics.Make

module Make: 
functor (Compiler : Wp.Sigs.Compiler-> sig .. end
Parameters:
Compiler : Wp.Sigs.Compiler

module Cfg: Wp.CfgCompiler.Cfg  with module S = Compiler.M.Sigma
type node = Cfg.node 
type goal = {
   goal_pred : Cfg.P.t;
   goal_prop : Wp.WpPropId.prop_id;
}
type cfg = Cfg.cfg 
type paths = {
   paths_cfg : cfg;
   paths_goals : goal Bag.t;
}
val goals_nodes : goal Bag.t -> Cfg.Node.Set.t
exception LabelNotFound of Wp.Clabels.c_label

Compilation environment
type env 
val empty_env : Kernel_function.t -> env
val bind : Wp.Clabels.c_label ->
node ->
env -> env
val result : env -> Wp.Lang.F.var
val (@^) : paths ->
paths -> paths
Same as Cfg.concat
val ( @* ) : env ->
(Wp.Clabels.c_label * node) list ->
env
fold bind
val (@:) : env -> Wp.Clabels.c_label -> node
LabelMap.find with refined excpetion.
Raises LabelNotFound instead of Not_found
val (@-) : env ->
(Wp.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:Wp.Clabels.c_label ->
?post:Wp.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:Wp.Clabels.c_label ->
?post:Wp.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 ->
Cil_types.lval -> Cil_types.exp -> paths
val scope : env ->
Wp.Sigs.scope -> Cil_types.varinfo list -> paths
val instr : env -> Cil_types.instr -> paths
val return : env ->
Cil_types.exp option -> paths
val assume : Cfg.P.t -> paths
val call_kf : env ->
Cil_types.lval option ->
Cil_types.kernel_function ->
Cil_types.exp list -> paths
val call : env ->
Cil_types.lval option ->
Cil_types.exp -> Cil_types.exp list -> paths

ACSL Compilation


val spec : env -> Cil_types.spec -> paths
val assume_ : env ->
Wp.Sigs.polarity -> Cil_types.predicate -> paths
val assigns : env -> Cil_types.assigns -> paths
val froms : env ->
Cil_types.from list -> paths

Automata Compilation


val automaton : env ->
Interpreted_automata.automaton -> paths
val init : is_pre_main:bool -> env -> paths
val compute_kf : 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.