module Interp:sig
..end
Interpretation of logic terms.
For the three functions below, env
can be used to specify which
logic labels are parsed. By default, only Here
is accepted. All
the C labels inside the function are also accepted, regardless of
env
. loc
is used as the source for the beginning of the string.
All three functions may raise Logic_interp.Error
or
Parsing.Parse_error
.
val term_lval : (Cil_types.kernel_function ->
?loc:Cil_types.location ->
?env:Logic_typing.Lenv.t -> string -> Cil_types.term_lval)
Stdlib.ref
val term : (Cil_types.kernel_function ->
?loc:Cil_types.location ->
?env:Logic_typing.Lenv.t -> string -> Cil_types.term)
Stdlib.ref
val predicate : (Cil_types.kernel_function ->
?loc:Cil_types.location ->
?env:Logic_typing.Lenv.t -> string -> Cil_types.predicate)
Stdlib.ref
val code_annot : (Cil_types.kernel_function ->
Cil_types.stmt -> string -> Cil_types.code_annotation)
Stdlib.ref
exception No_conversion
Exception raised by the functions below when their given argument cannot be interpreted in the C world.
val term_lval_to_lval : (result:Cil_types.varinfo option -> Cil_types.term_lval -> Cil_types.lval)
Stdlib.ref
No_conversion
if the argument is not a left value.val term_to_lval : (result:Cil_types.varinfo option -> Cil_types.term -> Cil_types.lval)
Stdlib.ref
No_conversion
if the argument is not a left value.val term_to_exp : (result:Cil_types.varinfo option -> Cil_types.term -> Cil_types.exp)
Stdlib.ref
No_conversion
if the argument is not a valid expression.val loc_to_exp : (result:Cil_types.varinfo option -> Cil_types.term -> Cil_types.exp list)
Stdlib.ref
No_conversion
if the argument is not a valid set of
expressions.val loc_to_lval : (result:Cil_types.varinfo option -> Cil_types.term -> Cil_types.lval list)
Stdlib.ref
No_conversion
if the argument is not a valid set of
left values.val term_offset_to_offset : (result:Cil_types.varinfo option -> Cil_types.term_offset -> Cil_types.offset)
Stdlib.ref
No_conversion
if the argument is not a valid offset.val loc_to_offset : (result:Cil_types.varinfo option -> Cil_types.term -> Cil_types.offset list)
Stdlib.ref
No_conversion
if the given term does not match the preconditionval loc_to_loc : (result:Cil_types.varinfo option ->
Db.Value.state -> Cil_types.term -> Locations.location)
Stdlib.ref
No_conversion
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)
Stdlib.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.
No_conversion
if the translation fails.module To_zone:sig
..end
val to_result_from_pred : (Cil_types.predicate -> bool) Stdlib.ref
Does the interpretation of the predicate rely on the interpretation of the term result?