Module IR__PredSymb

The Smallfoot Intermediate Language: Predicate Symbols

Programs and Types

type access =
| Default
| Public
| Private
| Protected

Visibility modifiers.

val compare_access : access -> access -> int
val equal_access : access -> access -> bool
val string_of_access : access -> string
type mem_kind =
| Mmalloc

memory allocated with malloc

| Mnew

memory allocated with new

| Mnew_array

memory allocated with new

| Mobjc

memory allocated with objective-c alloc

val compare_mem_kind : mem_kind -> mem_kind -> int
type resource =
| Rmemory of mem_kind
| Rfile
| Rignore
| Rlock

resource that can be allocated

val compare_resource : resource -> resource -> int
type res_act_kind =
| Racquire
| Rrelease

kind of resource action

val compare_res_act_kind : res_act_kind -> res_act_kind -> int
val equal_res_act_kind : res_act_kind -> res_act_kind -> bool
type dangling_kind =
| DAuninit

pointer is dangling because it is uninitialized

| DAaddr_stack_var

pointer is dangling because it is the address of a stack variable which went out of scope

| DAminusone

pointer is -1

kind of dangling pointers

type path_pos = IR.Procname.t * int

position in a path: proc name, node id

val compare_path_pos : path_pos -> path_pos -> int
val equal_path_pos : path_pos -> path_pos -> bool
type res_action = {
ra_kind : res_act_kind;

kind of action

ra_res : resource;

kind of resource

ra_pname : IR.Procname.t;

name of the procedure used to acquire/release the resource

ra_loc : IBase.Location.t;

location of the acquire/release

ra_vpath : IR.DecompiledExp.vpath;

vpath of the resource value

}

acquire/release action on a resource

type t =
| Aresource of res_action

resource acquire/release

| Aautorelease
| Adangling of dangling_kind

dangling pointer

| Aundef of IR.Procname.t * IR.Annot.Item.t * IBase.Location.t * path_pos
| Alocked
| Aunlocked
| Adiv0 of path_pos

value appeared in second argument of division at given path position

| Aobjc_null

attributed exp is null due to a call to a method with given path as null receiver

| Aretval of IR.Procname.t * IR.Annot.Item.t

value was returned from a call to the given procedure, plus the annots of the return value

| Aobserver

denotes an object registered as an observers to a notification center

| Aunsubscribed_observer

denotes an object unsubscribed from observers of a notification center

| Awont_leak

value do not participate in memory leak analysis

Attributes are nary function symbols that are applied to expression arguments in Apred and Anpred atomic formulas. Many operations don't make much sense for nullary predicates, and are generally treated as no-ops. The first argument is treated specially, as the "anchor" of the predicate application. For example, adding or removing an attribute uses the anchor to identify the atom to operate on. Also, abstraction and normalization operations treat the anchor specially and maintain more information on it than other arguments. Therefore when attaching an attribute to an expression, that expression should be the first argument, optionally followed by additional related expressions.

val compare : t -> t -> int
val equal : t -> t -> bool
val mem_alloc_pname : mem_kind -> IR.Procname.t

name of the allocation function for the given memory kind

val mem_dealloc_pname : mem_kind -> IR.Procname.t

name of the deallocation function for the given memory kind

type category =
| ACresource
| ACautorelease
| AClock
| ACdiv0
| ACobjc_null
| ACundef
| ACretval
| ACobserver
| ACwontleak

Categories of attributes

val compare_category : category -> category -> int
val equal_category : category -> category -> bool
val to_category : t -> category

Return the category to which the attribute belongs.

val is_undef : t -> bool
val to_string : IStdlib.Pp.env -> t -> string

convert the attribute to a string

val d_attribute : t -> unit

Dump an attribute.