Index of values

add obs adds the basic constraint obs to the global constraint set.

make two variables equal

extends the image of the mapping from type variables to types

add a new observer

add_wl obs adds the observer obs to the working list.

collects all locations from a program

Compares to program labels.

compare to values

compare to values

Compares two locations

compare type variables.

comapres two observers

compare to values

comapres to labels

comapre to program labels

compares to variables.

create a new location

create a new uniquie type variable

create_c_demonation_lenv lev1 mu lev2 creates a constraint that changes all precise pointers, for which the location is part of mu, into imprecise pointers.

create_c_demonation_lenv_ls lev1 mu ls lev2 creates a constraint that ensures that the intersection of the domain of variables lev1 and ls is empty.

create the constraints for an expression

Create a new unique exact pointer

Create a new unique inexact pointer

creates a new label

create a lower bound

create a lower bound

create a lower bound and a negative information

create a lower and an upper bound

create a lower and an upper bound

creates a negative information

create a new program label.

create a program label

create the constraints for a serious expression

creates an upper bound

creates an upper bound

create the constraints for a value

creates a new variable from a string

This function is called by observers every time something with the image of the variable changes.

Returns the domain of the map

returns the program label

Creates a let expression

Creates a mask expression (Maske)

Creates an expression from a serious expression

find' k map returns Some b if map(k) == b.

find_or_add ~create:c ~key:k ~map:m returns m(k) if k in domain(m).

this method is called if the image of the variable changes

Like a fold operator on a map

free_e e computes the free variables of e and returns it as a set.

free_s s computes the free variables of s and returns it as a set.

free_e v computes the free variables of v and returns it as a set.

IMPORTANT: Use this only, if you lex code.

Calling of full_visit adds all constraints that are part of the global constraint set to the work list.

If the upper and lower bound are equal, then the exact value is returned.

If the upper and lower bound are equal, then the exact value is returned.

returns the image

get_location p returns the location of the pointer.

If inter t1 t2 is called please compute a value t such that subset t t1 and subset t t2 holds.

is_empty t should returns true if t is the empty set, otherwise it returns false.

is_false str adds the constraint False (Some s) to the global constraint set and removes all other constraints from the set.

is_precise p returns true if the pointer is precise, otherwise false is returned.

hm, what happens here?

merge to sets

unions two LSetInEx.t values

merge these two images, such that the new image fulfills all properties of both old ones.

bring the image into a unique from

returns the program label

remove obs removes the basic constraint obs from the global constraint set.

remove a observer

IMPORTENT: Do only use this function for tests.

IMPORTANT: Use this only for testing.

IMPORTANT: Use this only for testing.

This function resets the global constraint.

Resets the internal counter that allows to differ variables from each other.

IMPORTENT: Do use this only for testing! Calls reset of P and Loc.

Creates a serious expression (application)

returns the program label

Creates a serious expression (method call)

Creates a serious expression (new)

Creates a serious expression (new) with the given abstract location

Creates a serious expression (read)

Creates a serious expression from a value

Creates a serious expression (write)

solve () starts the solving of the global constraint set.

Returns a string representation of a program label

Returns a string representation of a LSetInEx.t value

Returns a string representation of a LSetInEx.t value

Returns a string representation of a pointer

Returns a string represenation of a location

This returns a string representation of the global constraint.

converts a variable to a string

string representation of the observer

Returns a string representation of an expression

Returns an expression together with it's program locations as a string

Returns a string representation of a variable

Returns a string represenation of a lambda expression

Returns a lambda expression together with it's program locations as a string

convert the map into a string

Returns a string represenation of a program label

Returns a string representation of a value.

Returns a value together with it's program locations as a string

Returns a string representation of a value

Returns a string representation of a variable

subset t1 t2 should return Some true if t1 is a subset of t2.

compare type variables.

If union t1 t2 is called please compute a value t such that subset t1 t and subset t2 t holds.

returns the program label

Creates an integer as a value

Creates a value (lambda expression)

Creates a value (undefined)

Creates a value (var)