Analysis.Loc
type value = Val.t
val top : location
val pretty_loc : Stdlib.Format.formatter -> location -> unit
val pretty_offset : Stdlib.Format.formatter -> offset -> unit
val to_value : location -> value Eva.Eval.or_bottom
val size : location -> Frama_c_kernel.Int_Base.t
val enumerate_valid_bits :
Frama_c_kernel.Locations.access ->
location ->
Frama_c_kernel.Locations.Zone.t
Given an access type and a location, return the zone corresponding to the valid bits of the location.
val replace_base : Frama_c_kernel.Base.substitution -> location -> location
replace_base substitution location
replaces the variables represented by the location
according to substitution
.
These functions are used to create the alarms that report undesirable behaviors, when a location abstraction does not meet the prerequisites of an operation. Thereafter, the location is assumed to meet them to continue the analysis. See the documentation of Abstract_value.truth
for more details.
val assume_no_overlap :
partial:bool ->
location ->
location ->
[ `False
| `Unknown of location * location
| `True
| `TrueReduced of location * location
| `Unreachable ]
Assumes that two locations do not overlap. If partial
is true, the concrete locations may be equal, but different locations must not overlap. Otherwise, the locations must be completely separate.
val assume_valid_location :
for_writing:bool ->
bitfield:bool ->
location ->
[ `False
| `Unknown of location
| `True
| `TrueReduced of location
| `Unreachable ]
Assumes that the given location is valid for a read or write operation, according to the for_writing
boolean. Used to emit memory access alarms. If the location is not completely valid, reduces it to its valid part. bitfield
indicates whether the location may be the one of a bitfield; if it is false, the location can be assumed to be byte aligned.
val no_offset : offset
val forward_field :
Frama_c_kernel.Cil_types.typ ->
Frama_c_kernel.Cil_types.fieldinfo ->
offset ->
offset
Computes the field offset of a fieldinfo, with the given remaining offset. The given type must the one of the structure or the union.
val forward_index : Frama_c_kernel.Cil_types.typ -> value -> offset -> offset
forward_index typ value offset
computes the array index offset of (Index (ind, off)), where the index expression ind
evaluates to value
and the remaining offset off
evaluates to offset
. typ
must be the type pointed by the array.
Evaluation of the location of an lvalue, when the offset has already been evaluated. In case of a pointer, its expression has also been evaluated to a value.
val forward_variable :
Frama_c_kernel.Cil_types.typ ->
Frama_c_kernel.Cil_types.varinfo ->
offset ->
location Eva.Eval.or_bottom
Var case in the AST: the host is a variable.
val forward_pointer :
Frama_c_kernel.Cil_types.typ ->
value ->
offset ->
location Eva.Eval.or_bottom
Mem case in the AST: the host is a pointer.
val eval_varinfo : Frama_c_kernel.Cil_types.varinfo -> location
For an unary forward operation F, the inverse backward operator B tries to reduce the argument values of the operation, given its result.
It must satisfy: if B arg res
= v then ∀ a ⊆ arg such that F a
⊆ res, a ⊆ v
i.e. B arg res
returns a value v
larger than all subvalues of arg
whose result through F is included in res
.
If F arg
∈ res
is impossible, then v
should be bottom.
Any n-ary operator may be considered as a unary operator on a vector of values, the inclusion being lifted pointwise.
val backward_variable :
Frama_c_kernel.Cil_types.varinfo ->
location ->
offset Eva.Eval.or_bottom
val backward_field :
Frama_c_kernel.Cil_types.typ ->
Frama_c_kernel.Cil_types.fieldinfo ->
offset ->
offset Eva.Eval.or_bottom
val backward_index :
Frama_c_kernel.Cil_types.typ ->
index:value ->
remaining:offset ->
offset ->
(value * offset) Eva.Eval.or_bottom
val structure : location Eva__.Abstract.Location.structure
val get : 'a Eva__.Structure.Key_Location.key -> (location -> 'a) option
For a key of type k key
:
t
contain a subpart of type k
from a module identified by the key, then get key
returns an accessor for it.get key
returns None.For a key of type k key
:
t
contain a subpart of type k
from a module identified by the key, then set key v t
returns the value t
in which this subpart has been replaced by v
.set key _
is the identity function.Iterators on the components of a structure.
val iter : polymorphic_iter_fun -> location -> unit
val fold : 'b polymorphic_fold_fun -> location -> 'b -> 'b
val map : polymorphic_map_fun -> location -> location