Module Db.Properties.Interp

module Interp: sig .. end

Interpretation of logic terms.

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)
       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

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)
       Stdlib.ref

Raises No_conversion if the argument is not a left value.

Change in Aluminium-20160501

val term_to_lval : (result:Cil_types.varinfo option -> Cil_types.term -> Cil_types.lval)
       Stdlib.ref

Raises No_conversion if the argument is not a left value.

Change in Aluminium-20160501

val term_to_exp : (result:Cil_types.varinfo option -> Cil_types.term -> Cil_types.exp)
       Stdlib.ref

Raises No_conversion if the argument is not a valid expression.

Change in Aluminium-20160501

val loc_to_exp : (result:Cil_types.varinfo option -> Cil_types.term -> Cil_types.exp list)
       Stdlib.ref

Raises No_conversion if the argument is not a valid set of expressions.
Returns a list of C expressions.

Change in Aluminium-20160501

val loc_to_lval : (result:Cil_types.varinfo option -> Cil_types.term -> Cil_types.lval list)
       Stdlib.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

val term_offset_to_offset : (result:Cil_types.varinfo option -> Cil_types.term_offset -> Cil_types.offset)
       Stdlib.ref

Raises No_conversion if the argument is not a valid offset.

Change in Aluminium-20160501

val loc_to_offset : (result:Cil_types.varinfo option -> Cil_types.term -> Cil_types.offset list)
       Stdlib.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

From logic terms to Locations.location

val loc_to_loc : (result:Cil_types.varinfo option ->
        Db.Value.state -> Cil_types.term -> Locations.location)
       Stdlib.ref

Raises No_conversion if the translation fails.

Change in Aluminium-20160501

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.

Raises No_conversion if the translation fails.

Change in Aluminium-20160501

From logic terms to Zone.t

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?

Since Carbon-20110201