module Interp: sig
.. end
Interpretation of logic terms.
Parsing logic terms and annotations
val lval : (Cil_types.kernel_function -> Cil_types.stmt -> string -> Cil_types.term_lval)
Pervasives.ref
val expr : (Cil_types.kernel_function -> Cil_types.stmt -> string -> Cil_types.term)
Pervasives.ref
val code_annot : (Cil_types.kernel_function ->
Cil_types.stmt -> string -> Cil_types.code_annotation)
Pervasives.ref
From logic terms to C terms
val term_lval_to_lval : (result:Cil_types.varinfo option -> Cil_types.term_lval -> Cil_types.lval)
Pervasives.ref
Raises Invalid_argument
if the argument is not a left value.
val term_to_lval : (result:Cil_types.varinfo option -> Cil_types.term -> Cil_types.lval)
Pervasives.ref
Raises Invalid_argument
if the argument is not a left value.
val term_to_exp : (result:Cil_types.varinfo option -> Cil_types.term -> Cil_types.exp)
Pervasives.ref
Raises Invalid_argument
if the argument is not a valid expression.
val loc_to_exp : (result:Cil_types.varinfo option -> Cil_types.term -> Cil_types.exp list)
Pervasives.ref
Raises Invalid_argument
if the argument is not a valid set of
expressions.
Returns a list of C expressions.
val loc_to_lval : (result:Cil_types.varinfo option -> Cil_types.term -> Cil_types.lval list)
Pervasives.ref
Raises Invalid_argument
if the argument is not a valid set of
left values.
Returns a list of C locations.
val term_offset_to_offset : (result:Cil_types.varinfo option -> Cil_types.term_offset -> Cil_types.offset)
Pervasives.ref
Raises Invalid_argument
if the argument is not a valid offset.
val loc_to_offset : (result:Cil_types.varinfo option -> Cil_types.term -> Cil_types.offset list)
Pervasives.ref
Returns a list of C offset provided the term denotes location who
have all the same base address.
From logic terms to Locations.location
val loc_to_loc : (result:Cil_types.varinfo option ->
Db.Value.state -> Cil_types.term -> Locations.location)
Pervasives.ref
Raises Invalid_argument
if the translation fails.
val loc_to_loc_under_over : (result:Cil_types.varinfo option ->
Db.Value.state ->
Cil_types.term -> Locations.location * Locations.location * Locations.Zone.t)
Pervasives.ref
Same as
Db.Properties.Interp.loc_to_loc
, except that we return simultaneously an
under-approximation of the term (first location), and an
over-approximation (second location). The under-approximation
is particularly useful when evaluating Tsets. The zone returned is an
over-approximation of locations that have been read during evaluation.
Warning: This API is not stabilized, and may change in
the future.
Raises Invalid_argument
in some cases.
From logic terms to Zone.t
module To_zone: sig
.. end
val to_result_from_pred : (Cil_types.predicate Cil_types.named -> bool) Pervasives.ref
Does the interpretation of the predicate rely on the intepretation
of the term result?
Since Carbon-20110201