Module Register

module Register: sig .. end
Function of the value plugin registered in the kernel

val dkey_card : Log.category
val display : ?fmt:Format.formatter -> Kernel_function.t -> unit
val display_results : unit -> unit
val main : unit -> unit
val lval_to_loc_with_deps_state : with_alarms:CilE.warn_mode ->
Cvalue.Model.t ->
deps:Locations.Zone.t ->
Cil_types.lval -> Locations.Zone.t * Locations.location
val lval_to_loc_with_deps : Cil_types.kinstr ->
with_alarms:CilE.warn_mode ->
deps:Locations.Zone.t ->
Cil_types.lval -> Locations.Zone.t * Locations.location
val lval_to_loc_kinstr : Cil_types.kinstr ->
with_alarms:CilE.warn_mode -> Cil_types.lval -> Locations.location
val lval_to_precise_loc_with_deps_state_alarm : with_alarms:CilE.warn_mode ->
Cvalue.Model.t ->
deps:Locations.Zone.t option ->
Cil_types.lval -> Locations.Zone.t * Precise_locs.precise_location
val lval_to_precise_loc_with_deps_state : Cvalue.Model.t ->
deps:Locations.Zone.t option ->
Cil_types.lval -> Locations.Zone.t * Precise_locs.precise_location
val lval_to_zone : Cil_types.kinstr ->
with_alarms:CilE.warn_mode -> Cil_types.lval -> Locations.Zone.t
val lval_to_zone_state : Cvalue.Model.t -> Cil_types.lval -> Locations.Zone.t
val lval_to_zone_with_deps_state : Cvalue.Model.t ->
for_writing:bool ->
deps:Locations.Zone.t option ->
Cil_types.lval -> Locations.Zone.t * Locations.Zone.t * bool
val expr_to_kernel_function_state : Cvalue.Model.t ->
deps:Locations.Zone.t option ->
Cil_types.exp -> Locations.Zone.t * Kernel_function.Hptset.t
val expr_to_kernel_function : Cil_types.kinstr ->
with_alarms:CilE.warn_mode ->
deps:Locations.Zone.t option ->
Cil_types.exp -> Locations.Zone.t * Kernel_function.Hptset.t
val expr_to_kernel_function_state : Cvalue.Model.t ->
deps:Locations.Zone.t option ->
Cil_types.exp -> Locations.Zone.t * Kernel_function.Hptset.t
val eval_error_reason : Format.formatter -> Eval_terms.logic_evaluation_error -> unit
val assigns_inputs_to_zone : Cvalue.Model.t ->
Cil_types.identified_term Cil_types.assigns -> Locations.Zone.t
val assigns_outputs_aux : eval:(Eval_terms.eval_env -> Cil_types.term -> 'a) ->
bot:'b ->
top:'a ->
join:('a -> 'b -> 'b) ->
Cvalue.Model.t ->
result:Cil_types.varinfo option ->
Cil_types.identified_term Cil_types.assigns -> 'b
val assigns_outputs_to_zone : Cvalue.Model.t ->
result:Cil_types.varinfo option ->
Cil_types.identified_term Cil_types.assigns -> Locations.Zone.t
val assigns_outputs_to_locations : Cvalue.Model.t ->
result:Cil_types.varinfo option ->
Cil_types.identified_term Cil_types.assigns -> Locations.location list
val lval_to_offsetmap_aux : with_alarms:CilE.warn_mode ->
Cvalue.Model.t -> Cil_types.lval -> Cvalue.Model.offsetmap option
val lval_to_offsetmap : Cil_types.kinstr ->
Cil_types.lval -> with_alarms:CilE.warn_mode -> Cvalue.Model.offsetmap option
val lval_to_offsetmap_state : Cvalue.Model.t -> Cil_types.lval -> Cvalue.Model.offsetmap option
val access_value_of_lval : Cil_types.kinstr -> Cil_types.lval -> Db.Value.t
val access_value_of_expr : Cil_types.kinstr -> Cil_types.exp -> Db.Value.t
val access_value_of_location : Cil_types.kinstr -> Locations.location -> Db.Value.t
val find_deps_term_no_transitivity_state : Cvalue.Model.t -> Cil_types.term -> Eval_terms.logic_deps
val use_spec_instead_of_definition : Kernel_function.t -> bool
val eval_predicate : pre:Cvalue.Model.t ->
here:Cvalue.Model.t ->
Cil_types.predicate Cil_types.named -> Property_status.emitted_status