module Value_util: sig
.. end
type
call_site = Cil_types.kernel_function * Cil_types.kinstr
A call_stack is a list, telling which function was called at which
site. The head of the list tells about the latest call.
type
callstack = call_site list
val clear_call_stack : unit -> unit
Functions dealing with call stacks.
val pop_call_stack : unit -> unit
val push_call_stack : Cil_types.kernel_function -> Cil_types.kinstr -> unit
val current_kf : unit -> Cil_types.kernel_function
The current function is the one on top of the call stack.
val call_stack : unit -> callstack
val pp_callstack : Format.formatter -> unit
Prints the current callstack.
Others
val emitter : Emitter.t
val get_slevel : Kernel_function.t -> Value_parameters.SlevelFunction.value
val get_subdivision : Cil_types.stmt -> int
val pretty_actuals : Format.formatter -> (Cil_types.exp * Cvalue.V.t * 'b) list -> unit
val pretty_current_cfunction_name : Format.formatter -> unit
val warning_once_current : ('a, Format.formatter, unit) Pervasives.format -> 'a
val alarm_report : 'a Log.pretty_printer
module DegenerationPoints: State_builder.Hashtbl
with type key = stmt and type data = bool
val create_new_var : string -> Cil_types.typ -> Cil_types.varinfo
Create and register a new variable inside Frama-C. The variable
has its vlogic
field set, meaning it is not a source variable. The
freshness of the name must be ensured by the user.
val is_const_write_invalid : Cil_types.typ -> bool
Detect that the type is const, and that option -global-const
is set. In
this case, we forbid writing in a l-value that has this type.
val postconditions_mention_result : Cil_types.funspec -> bool
Does the post-conditions of this specification mention \result
?
val conv_comp : Cil_types.binop -> Abstract_interp.Comp.t
val conv_relation : Cil_types.relation -> Abstract_interp.Comp.t
val normalize_as_cond : Cil_types.exp -> bool -> Cil_types.exp
normalize_as_cond e positive
returns the expression corresponding to
e != 0
when positive
is true, and e == 0
otherwise. The
resulting expression will always have a comparison operation at its
root.
val is_value_zero : Cil_types.exp -> bool
val lval_to_exp : Cil_types.lval -> Cil_types.exp
This function is memoized to avoid creating too many expressions
val dump_garbled_mix : unit -> unit
print information on the garbled mix created during evaluation
Dependences of expressions and lvalues.
val zone_of_expr : (Cil_types.lval -> Precise_locs.precise_location) ->
Cil_types.exp -> Locations.Zone.t
Given a function computing the location of lvalues, computes the memory zone
on which the value of an expression depends.
val indirect_zone_of_lval : (Cil_types.lval -> Precise_locs.precise_location) ->
Cil_types.lval -> Locations.Zone.t
Given a function computing the location of lvalues, computes the memory zone
on which the offset and the pointer expression (if any) of an lvalue depend.
val height_expr : Cil_types.exp -> int
Computes the height of an expression, that is the maximum number of nested
operations in this expression.
val height_lval : Cil_types.lval -> int
Computes the height of an lvalue.
val skip_specifications : Cil_types.kernel_function -> bool
Should we skip the specifications of this function, according to
-eva-skip-stdlib-specs