module Make:
Parameters: |
|
module Cfg:CfgCompiler.Cfg
with module S = Compiler.M.Sigma
typenode =
Cfg.node
type
goal = {
|
goal_pred : |
|
goal_prop : |
typecfg =
Cfg.cfg
type
paths = {
|
paths_cfg : |
|
paths_goals : |
val goals_nodes : goal Bag.t -> Cfg.Node.Set.t
exception LabelNotFound of Clabels.c_label
Compilation environment
type
env
val empty_env : 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.
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.
executed possibly at the same time
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 ->
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
val spec : env -> Cil_types.spec -> paths
val assume_ : env ->
Sigs.polarity -> Cil_types.predicate -> paths
val assigns : env -> Cil_types.assigns -> paths
val froms : env -> Cil_types.from list -> paths
val automaton : env ->
Interpreted_automata.automaton -> paths
val init : is_pre_main:bool -> env -> paths
connect init to here. is_pre_main
indicate if here is the
pre-state of main.
val compute_kf : Kernel_function.t -> paths * node
Returns the set of all paths for the function, with all proof
obligations. The returned node corresponds to the Init
label.