Module StmtSemantics.MakeSource

Parameters

Signature

Sourcetype node = Cfg.node
Sourcetype goal = {
  1. goal_pred : Cfg.P.t;
  2. goal_prop : WpPropId.prop_id;
}
Sourcetype cfg = Cfg.cfg
Sourcetype paths = {
  1. paths_cfg : cfg;
  2. paths_goals : goal Frama_c_kernel.Bag.t;
}
Sourceexception LabelNotFound of Clabels.c_label

Compilation environment

Sourcetype env
Sourceval bind : Clabels.c_label -> node -> env -> env
Sourceval result : env -> Lang.F.var
Sourceval (@^) : paths -> paths -> paths

Same as Cfg.concat

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

fold bind

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

LabelMap.find with refined excpetion.

Sourceval (@-) : env -> (Clabels.c_label -> bool) -> env
Sourceval 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.

Sourceval 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.

Sourceval 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.

Sourceval return : env -> Frama_c_kernel.Cil_types.exp option -> paths
Sourceval assume : Cfg.P.t -> paths

ACSL Compilation

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

Automata Compilation

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

Full Compilation

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