otawa::concept::AbstractDomain< T, G > Class Template Reference

Concept used to implements AbsIntLite domain. More...

#include </home/casse/otawa/otawa/src/prog/concepts.h>

Public Types
typedef T	t
	Type of the values of the domain. More...

Public Member Functions
t	initial (void)
	Get the initial value (at graph entry). More...
t	bottom (void)
	Get the smallest value of the domain "_" such that forall d in domain, join(_, d) = joind(d, _) = d. More...
void	join (t &d, t s)
	Perform the join of two values, d = join(d1, d2) and must satisfy the property: d1 <= d and d2 <= d. More...
bool	equals (t v1, t v2)
	Test if two values are equal. More...
void	set (t &d, t s)
	Assign the value s to the value d. More...
void	dump (io::Output &out, t c)
	Only required if you use debug capabilities. More...
void	update (const typename G::Vertex &vertex, t &d)
	Update the value according to the given graph vertex. More...

Detailed Description

template<class T, class G>
class otawa::concept::AbstractDomain< T, G >

Concept used to implements AbsIntLite domain.

The soundness and the termination of the analysis requires a CPO (complete partial order) denoted "<=" on the domain values.

Member Typedef Documentation

template<class T , class G >

typedef T otawa::concept::AbstractDomain< T, G >::t

Type of the values of the domain.

Member Function Documentation

template<class T , class G >

t otawa::concept::AbstractDomain< T, G >::bottom

(

void

)

Get the smallest value of the domain "_" such that forall d in domain, join(_, d) = joind(d, _) = d.

template<class T , class G >

void otawa::concept::AbstractDomain< T, G >::dump	(	io::Output &	out,
		t	c
	)

Only required if you use debug capabilities.

It allows to display value.

Parameters

out	Stream to output to.
c	Value to output.

template<class T , class G >

bool otawa::concept::AbstractDomain< T, G >::equals	(	t	v1,
		t	v2
	)

Test if two values are equal.

Parameters

v1	First value.
v2	Secondd value.

Returns

True if both values are equal.

template<class T , class G >

t otawa::concept::AbstractDomain< T, G >::initial

(

void

)

Get the initial value (at graph entry).

template<class T , class G >

void otawa::concept::AbstractDomain< T, G >::join	(	t &	d,
		t	s
	)

Perform the join of two values, d = join(d1, d2) and must satisfy the property: d1 <= d and d2 <= d.

Parameters

d	First value to join and recipient of the result.
s	Second value to join.

template<class T , class G >

void otawa::concept::AbstractDomain< T, G >::set	(	t &	d,
		t	s
	)

Assign the value s to the value d.

Parameters

d	Assigned value.
s	Value to assign.

template<class T , class G >

void otawa::concept::AbstractDomain< T, G >::update	(	const typename G::Vertex &	vertex,
		t &	d
	)

Update the value according to the given graph vertex.

Notice that this function must be monotonic: forall domain values v1, v2 such that v1 <= v2, update(v1) <= update(v2).

Parameters

vertex	Current vertex.
d	Input value and result value.

---

The documentation for this class was generated from the following file:

• src/prog/concepts.h