Module Olf

type lvalue
type tau
type absloc
exception UnknownLocation

Raised if a pointer flows to an undefined function. We assume that such a function can have any effect on the pointer's contents

val debug : bool ref
val debug_constraints : bool ref
val debug_aliases : bool ref
val smart_aliases : bool ref
val finished_constraints : unit -> unit
val print_constraints : bool ref
val no_flow : bool ref
val no_sub : bool ref
val analyze_mono : bool ref
val solve_constraints : unit -> unit
val rvalue : lvalue -> tau
val deref : tau -> lvalue
val join : tau -> tau -> tau
val join_inits : tau list -> tau
val address : lvalue -> tau
val instantiate : lvalue -> int -> lvalue
val assign : lvalue -> tau -> unit
val assign_ret : int -> lvalue -> tau -> unit
val apply : tau -> tau list -> tau * int
val apply_undefined : tau list -> tau * int
val assign_undefined : lvalue -> unit
val make_function : string -> lvalue list -> tau -> tau
val make_lvalue : bool -> string -> Cil.varinfo option -> lvalue
val bottom : unit -> tau
val return : tau -> tau -> unit
val make_fresh : string -> tau
val points_to_names : lvalue -> string list
val points_to : lvalue -> Cil.varinfo list
val epoints_to : tau -> Cil.varinfo list
val string_of_lvalue : lvalue -> string
val may_alias : tau -> tau -> bool
val absloc_points_to : lvalue -> absloc list
val absloc_epoints_to : tau -> absloc list
val absloc_of_lvalue : lvalue -> absloc
val absloc_eq : (absloc * absloc) -> bool
val d_absloc : unit -> absloc -> Pretty.doc