Module CTrans_utils.PriorityNode
priority_node is used to enforce some kind of policy for creating nodes in the cfg. Certain elements of the AST _must_ create nodes therefore there is no need for them to use priority_node. Certain elements instead need or need not to create a node depending of certain factors. When an element of the latter kind wants to create a node it must claim priority first (like taking a lock). priority can be claimes only when it is free. If an element of AST succedes in claiming priority its id (pointer) is recorded in priority. After an element has finished it frees the priority. In general an AST element E checks if an ancestor has claimed priority. If priority is already claimed E does not have to create a node. If priority is free then it means E has to create the node. Then E claims priority and release it afterward.
type t
= priority_node
val is_priority_free : trans_state -> bool
val try_claim_priority_node : trans_state -> ATDGenerated.Clang_ast_t.stmt_info -> trans_state
val force_claim_priority_node : trans_state -> ATDGenerated.Clang_ast_t.stmt_info -> trans_state
val own_priority_node : t -> ATDGenerated.Clang_ast_t.stmt_info -> bool
val compute_controls_to_parent : trans_state -> IBase.Location.t -> IR.Procdesc.Node.stmt_nodekind -> ATDGenerated.Clang_ast_t.stmt_info -> control list -> control
Used by translation functions to handle potential cfg nodes. It connects nodes returned by the translation of stmt children and deals with creating or not a cfg node depending of owning the priority_node. It returns the
control
that should be passed to the parent.
val compute_control_to_parent : trans_state -> IBase.Location.t -> IR.Procdesc.Node.stmt_nodekind -> ATDGenerated.Clang_ast_t.stmt_info -> control -> control
like
compute_controls_to_parent
but for a singleton, so the only possible effect is creating a node
val compute_results_to_parent : trans_state -> IBase.Location.t -> IR.Procdesc.Node.stmt_nodekind -> ATDGenerated.Clang_ast_t.stmt_info -> return:(IR.Exp.t * IR.Typ.t) -> trans_result list -> trans_result
convenience wrapper around
compute_controls_to_parent
val compute_result_to_parent : trans_state -> IBase.Location.t -> IR.Procdesc.Node.stmt_nodekind -> ATDGenerated.Clang_ast_t.stmt_info -> trans_result -> trans_result
convenience function like
compute_results_to_parent
when there is a singletrans_result
to consider
val force_sequential : IBase.Location.t -> IR.Procdesc.Node.stmt_nodekind -> trans_state -> ATDGenerated.Clang_ast_t.stmt_info -> mk_first_opt:(trans_state -> ATDGenerated.Clang_ast_t.stmt_info -> trans_result option) -> mk_second:(trans_state -> ATDGenerated.Clang_ast_t.stmt_info -> trans_result) -> mk_return:(fst:trans_result -> snd:trans_result -> IR.Exp.t * IR.Typ.t) -> trans_result
val force_sequential_with_acc : IBase.Location.t -> IR.Procdesc.Node.stmt_nodekind -> trans_state -> ATDGenerated.Clang_ast_t.stmt_info -> mk_first:(trans_state -> ATDGenerated.Clang_ast_t.stmt_info -> trans_result * 'a) -> mk_second:('a -> trans_state -> ATDGenerated.Clang_ast_t.stmt_info -> trans_result) -> mk_return:(fst:trans_result -> snd:trans_result -> IR.Exp.t * IR.Typ.t) -> trans_result