module Interp: sig
.. end
Interpretation of logic terms.
Parsing logic terms and annotations
Parsing logic terms and annotations
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)
Pervasives.ref
val term : (Cil_types.kernel_function ->
?loc:Cil_types.location ->
?env:Logic_typing.Lenv.t -> string -> Cil_types.term)
Pervasives.ref
val predicate : (Cil_types.kernel_function ->
?loc:Cil_types.location ->
?env:Logic_typing.Lenv.t -> string -> Cil_types.predicate)
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
exception No_conversion
Exception raised by the functions below when their given argument
cannot be interpreted in the C world.
Since Aluminium-20160501
val term_lval_to_lval : (result:Cil_types.varinfo option -> Cil_types.term_lval -> Cil_types.lval)
Pervasives.ref
Raises No_conversion
if the argument is not a left value.
Change in Aluminium-20160501: raises a custom exn instead of generic Invalid_arg
val term_to_lval : (result:Cil_types.varinfo option -> Cil_types.term -> Cil_types.lval)
Pervasives.ref
Raises No_conversion
if the argument is not a left value.
Change in Aluminium-20160501: raises a custom exn instead of generic Invalid_arg
val term_to_exp : (result:Cil_types.varinfo option -> Cil_types.term -> Cil_types.exp)
Pervasives.ref
Raises No_conversion
if the argument is not a valid expression.
Change in Aluminium-20160501: raises a custom exn instead of generic Invalid_arg
val loc_to_exp : (result:Cil_types.varinfo option -> Cil_types.term -> Cil_types.exp list)
Pervasives.ref
Raises No_conversion
if the argument is not a valid set of
expressions.
Returns a list of C expressions.
Change in Aluminium-20160501: raises a custom exn instead of generic Invalid_arg
val loc_to_lval : (result:Cil_types.varinfo option -> Cil_types.term -> Cil_types.lval list)
Pervasives.ref
Raises No_conversion
if the argument is not a valid set of
left values.
Returns a list of C locations.
Change in Aluminium-20160501: raises a custom exn instead of generic Invalid_arg
val term_offset_to_offset : (result:Cil_types.varinfo option -> Cil_types.term_offset -> Cil_types.offset)
Pervasives.ref
Raises No_conversion
if the argument is not a valid offset.
Change in Aluminium-20160501: raises a custom exn instead of generic Invalid_arg
val loc_to_offset : (result:Cil_types.varinfo option -> Cil_types.term -> Cil_types.offset list)
Pervasives.ref
Raises No_conversion
if the given term does not match the precondition
Returns a list of C offset provided the term denotes locations who
have all the same base address.
Change in Aluminium-20160501: raises a custom exn instead of generic Invalid_arg
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 No_conversion
if the translation fails.
Change in Aluminium-20160501: raises a custom exn instead of generic
Invalid_arg
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 No_conversion
if the translation fails.
Change in Aluminium-20160501: raises a custom exn instead of generic
Invalid_arg
From logic terms to Zone.t
module To_zone: sig
.. end
val to_result_from_pred : (Cil_types.predicate -> bool) Pervasives.ref
Does the interpretation of the predicate rely on the interpretation
of the term result?
Since Carbon-20110201