Up  

Module Db.Properties.Interp.To_zone

module To_zone: sig .. end
type t_ctx = {
   state_opt : bool option;
   ki_opt : (Cil_types.stmt * bool) option;
   kf : Kernel_function.t;
} 
val mk_ctx_func_contrat : (Cil_types.kernel_function ->
        state_opt:bool option -> t_ctx)
       Stdlib.ref

To build an interpretation context relative to function contracts.

val mk_ctx_stmt_contrat : (Cil_types.kernel_function ->
        Cil_types.stmt ->
        state_opt:bool option -> t_ctx)
       Stdlib.ref

To build an interpretation context relative to statement contracts.

val mk_ctx_stmt_annot : (Cil_types.kernel_function ->
        Cil_types.stmt -> t_ctx)
       Stdlib.ref

To build an interpretation context relative to statement annotations.

type t = {
   before : bool;
   ki : Cil_types.stmt;
   zone : Locations.Zone.t;
} 
type t_zone_info = t list option

list of zones at some program points. None means that the computation has failed.

type t_decl = {
   var : Cil_datatype.Varinfo.Set.t;
   lbl : Cil_datatype.Logic_label.Set.t;
} 
type t_pragmas = {
   ctrl : Cil_datatype.Stmt.Set.t;
   stmt : Cil_datatype.Stmt.Set.t;
} 
val from_term : (Cil_types.term ->
        t_ctx ->
        t_zone_info *
        t_decl)
       Stdlib.ref

Entry point to get zones needed to evaluate the term relative to the ctx of interpretation.

val from_terms : (Cil_types.term list ->
        t_ctx ->
        t_zone_info *
        t_decl)
       Stdlib.ref

Entry point to get zones needed to evaluate the list of terms relative to the ctx of interpretation.

val from_pred : (Cil_types.predicate ->
        t_ctx ->
        t_zone_info *
        t_decl)
       Stdlib.ref

Entry point to get zones needed to evaluate the predicate relative to the ctx of interpretation.

val from_preds : (Cil_types.predicate list ->
        t_ctx ->
        t_zone_info *
        t_decl)
       Stdlib.ref

Entry point to get zones needed to evaluate the list of predicates relative to the ctx of interpretation.

val from_zone : (Cil_types.identified_term ->
        t_ctx ->
        t_zone_info *
        t_decl)
       Stdlib.ref

Entry point to get zones needed to evaluate the zone relative to the ctx of interpretation.

val from_stmt_annot : (Cil_types.code_annotation ->
        Cil_types.stmt * Cil_types.kernel_function ->
        (t_zone_info *
         t_decl) *
        t_pragmas)
       Stdlib.ref

Entry point to get zones needed to evaluate an annotation on the given stmt.

val from_stmt_annots : ((Cil_types.code_annotation -> bool) option ->
        Cil_types.stmt * Cil_types.kernel_function ->
        (t_zone_info *
         t_decl) *
        t_pragmas)
       Stdlib.ref

Entry point to get zones needed to evaluate annotations of this stmt.

val from_func_annots : (((Cil_types.stmt -> unit) -> Cil_types.kernel_function -> unit) ->
        (Cil_types.code_annotation -> bool) option ->
        Cil_types.kernel_function ->
        (t_zone_info *
         t_decl) *
        t_pragmas)
       Stdlib.ref

Entry point to get zones needed to evaluate annotations of this kf.

val code_annot_filter : (Cil_types.code_annotation ->
        threat:bool ->
        user_assert:bool ->
        slicing_pragma:bool -> loop_inv:bool -> loop_var:bool -> others:bool -> bool)
       Stdlib.ref

To quickly build an annotation filter