module Mem_lvalue: sig
.. end
Does the evaluation of stmt
modifies the eventual value of X.lv
?
module KernelFile: File
val debug : bool
val lv_is_precise : Cil_types.lval -> bool
val lv_has_exact_loc : Cil_types.stmt -> Cil_types.lval -> bool
val lv_imprecise_loc : Cil_types.stmt -> Cil_types.lval -> bool
type
found =
module LatticeDirty: sig
.. end
module Compute: functor (
X
:
sig
end
) ->
sig
.. end
val compute : unit -> unit
val reemit : Property.identified_property -> bool
val good_emitter : Emitter.Usable_emitter.t -> bool
val copy_ppt : Project.t -> Project.t -> Property.t -> Property.t -> unit
val dup_spec_status : Project.t -> Kernel_function.t -> unit
Assumes the current project is old_prj
module HLV: Cil_datatype.LvalStructEq.Hashtbl
type
action =
val lv_name : Cil_types.lval -> string
val instrument : Cil_types.fundec ->
Cil_types.lval ->
(found * Cil_datatype.Stmt.Hashtbl.key * LatticeDirty.t)
list ->
[> `Assert of Cil_types.lval
| `Read of Cil_types.lval
| `Write of Cil_types.lval ]
Cil_datatype.Stmt.Hashtbl.t -> Cil_types.varinfo HLV.t -> unit
type
skip_change =
| |
SkipChangeDeep |
| |
SkipOneChange |
module GraphDeps: sig
.. end
module TopologicalBefore: Graph.Topological.Make
(
GraphDeps
)
class instrument : Project.t -> [< `Assert of 'a | `Read of HLV.key | `Write of HLV.key ]
Cil_datatype.Stmt.Hashtbl.t -> Cil_types.varinfo HLV.t ->
object
.. end
val print_lv : Cil_types.lval ->
(found * Cil_datatype.Stmt.t) list ->
(found * Cil_datatype.Stmt.t * LatticeDirty.t) list
class reused_lval :
object
.. end
val compute : unit -> unit