Typedefs for the library datatypes and related symbolic constants. More...

Typedefs
typedef size_t	ppl_dimension_type
	An unsigned integral type for representing space dimensions. More...

typedef const char *	ppl_io_variable_output_function_type(ppl_dimension_type var)
	The type of output functions used for printing variables. More...

Enumerations
enum	ppl_enum_Constraint_Type { PPL_CONSTRAINT_TYPE_LESS_THAN, PPL_CONSTRAINT_TYPE_LESS_OR_EQUAL, PPL_CONSTRAINT_TYPE_EQUAL, PPL_CONSTRAINT_TYPE_GREATER_OR_EQUAL, PPL_CONSTRAINT_TYPE_GREATER_THAN }
	Describes the relations represented by a constraint. More...

enum	ppl_enum_Generator_Type { PPL_GENERATOR_TYPE_LINE, PPL_GENERATOR_TYPE_RAY, PPL_GENERATOR_TYPE_POINT, PPL_GENERATOR_TYPE_CLOSURE_POINT }
	Describes the different kinds of generators. More...

enum	ppl_enum_Grid_Generator_Type { PPL_GRID_GENERATOR_TYPE_LINE, PPL_GRID_GENERATOR_TYPE_PARAMETER, PPL_GRID_GENERATOR_TYPE_POINT }
	Describes the different kinds of grid generators. More...

enum	ppl_enum_Bounded_Integer_Type_Width { PPL_BITS_8, PPL_BITS_16, PPL_BITS_32, PPL_BITS_64, PPL_BITS_128 }
	Widths of bounded integer types. More...

enum	ppl_enum_Bounded_Integer_Type_Representation { PPL_UNSIGNED, PPL_SIGNED_2_COMPLEMENT }
	Representation of bounded integer types. More...

enum	ppl_enum_Bounded_Integer_Type_Overflow { PPL_OVERFLOW_WRAPS, PPL_OVERFLOW_UNDEFINED, PPL_OVERFLOW_IMPOSSIBLE }
	Overflow behavior of bounded integer types. More...

Functions
int	ppl_max_space_dimension (ppl_dimension_type *m)
	Writes to `m` the maximum space dimension this library can handle. More...

int	ppl_not_a_dimension (ppl_dimension_type *m)
	Writes to `m` a value that does not designate a valid dimension. More...

int	ppl_io_print_variable (ppl_dimension_type var)
	Pretty-prints `var` to `stdout`. More...

int	ppl_io_fprint_variable (FILE *stream, ppl_dimension_type var)
	Pretty-prints `var` to the given output `stream`. More...

int	ppl_io_asprint_variable (char **strp, ppl_dimension_type var)
	Pretty-prints `var` to a malloc-allocated string, a pointer to which is returned via `strp`. More...

int	ppl_io_set_variable_output_function (ppl_io_variable_output_function_type *p)
	Sets the output function to be used for printing variables to `p`. More...

int	ppl_io_get_variable_output_function (ppl_io_variable_output_function_type **pp)
	Writes a pointer to the current variable output function to `pp`. More...

char *	ppl_io_wrap_string (const char *src, unsigned indent_depth, unsigned preferred_first_line_length, unsigned preferred_line_length)
	Utility function for the wrapping of lines of text. More...

Variables
unsigned int	PPL_COMPLEXITY_CLASS_POLYNOMIAL
	Code of the worst-case polynomial complexity class. More...

unsigned int	PPL_COMPLEXITY_CLASS_SIMPLEX
	Code of the worst-case exponential but typically polynomial complexity class. More...

unsigned int	PPL_COMPLEXITY_CLASS_ANY
	Code of the universal complexity class. More...

unsigned int	PPL_POLY_CON_RELATION_IS_DISJOINT
	Individual bit saying that the polyhedron and the set of points satisfying the constraint are disjoint. More...

unsigned int	PPL_POLY_CON_RELATION_STRICTLY_INTERSECTS
	Individual bit saying that the polyhedron intersects the set of points satisfying the constraint, but it is not included in it. More...

unsigned int	PPL_POLY_CON_RELATION_IS_INCLUDED
	Individual bit saying that the polyhedron is included in the set of points satisfying the constraint. More...

unsigned int	PPL_POLY_CON_RELATION_SATURATES
	Individual bit saying that the polyhedron is included in the set of points saturating the constraint. More...

unsigned int	PPL_POLY_GEN_RELATION_SUBSUMES
	Individual bit saying that adding the generator would not change the polyhedron. More...

Detailed Description

Typedefs for the library datatypes and related symbolic constants.

The datatypes provided by the library should be manipulated by means of the corresponding opaque pointer types and the functions working on them.

Note: To simplify the detection of common programming mistakes, we provide both pointer-to-const and pointer-to-nonconst opaque pointers, with implicit conversions mapping each pointer-to-nonconst to the corresponding pointer-to-const when needed. The user of the C interface is therefore recommended to adopt the pointer-to-const type whenever read-only access is meant.

Typedef Documentation

typedef size_t ppl_dimension_type

An unsigned integral type for representing space dimensions.

Definition at line 506 of file ppl_c.h.

typedef const char* ppl_io_variable_output_function_type(ppl_dimension_type var)

The type of output functions used for printing variables.

An output function for variables must write a textual representation for var to a character buffer, null-terminate it, and return a pointer to the beginning of the buffer. In case the operation fails, 0 should be returned and perhaps errno should be set in a meaningful way. The library does nothing with the buffer, besides printing its contents.

Definition at line 550 of file ppl_c.h.

Enumeration Type Documentation

enum ppl_enum_Bounded_Integer_Type_Overflow

Overflow behavior of bounded integer types.

Enumerator

PPL_OVERFLOW_WRAPS

On overflow, wrapping takes place.

This means that, for a $w$ -bit bounded integer, the computation happens modulo $2^w$ .

PPL_OVERFLOW_UNDEFINED

On overflow, the result is undefined.

This simply means that the result of the operation resulting in an overflow can take any value.

Note: Even though something more serious can happen in the system being analyzed —due to, e.g., C's undefined behavior—, here we are only concerned with the results of arithmetic operations. It is the responsibility of the analyzer to ensure that other manifestations of undefined behavior are conservatively approximated.

PPL_OVERFLOW_IMPOSSIBLE

Overflow is impossible.

This is for the analysis of languages where overflow is trapped before it affects the state, for which, thus, any indication that an overflow may have affected the state is necessarily due to the imprecision of the analysis.

Definition at line 2414 of file ppl_c.h.

enum ppl_enum_Bounded_Integer_Type_Representation

Representation of bounded integer types.

Enumerator
PPL_UNSIGNED	Unsigned binary.
PPL_SIGNED_2_COMPLEMENT	Signed binary where negative values are represented by the two's complement of the absolute value.

Definition at line 2401 of file ppl_c.h.

enum ppl_enum_Bounded_Integer_Type_Width

Widths of bounded integer types.

Enumerator
PPL_BITS_8	8 bits.
PPL_BITS_16	16 bits.
PPL_BITS_32	32 bits.
PPL_BITS_64	64 bits.
PPL_BITS_128	128 bits.

Definition at line 2385 of file ppl_c.h.

enum ppl_enum_Constraint_Type

Describes the relations represented by a constraint.

Enumerator
PPL_CONSTRAINT_TYPE_LESS_THAN	The constraint is of the form .
PPL_CONSTRAINT_TYPE_LESS_OR_EQUAL	The constraint is of the form $e \leq 0$ .
PPL_CONSTRAINT_TYPE_EQUAL	The constraint is of the form .
PPL_CONSTRAINT_TYPE_GREATER_OR_EQUAL	The constraint is of the form $e \geq 0$ .
PPL_CONSTRAINT_TYPE_GREATER_THAN	The constraint is of the form .

Definition at line 1134 of file ppl_c.h.

enum ppl_enum_Generator_Type

Describes the different kinds of generators.

Enumerator
PPL_GENERATOR_TYPE_LINE	The generator is a line.
PPL_GENERATOR_TYPE_RAY	The generator is a ray.
PPL_GENERATOR_TYPE_POINT	The generator is a point.
PPL_GENERATOR_TYPE_CLOSURE_POINT	The generator is a closure point.

Definition at line 1444 of file ppl_c.h.

enum ppl_enum_Grid_Generator_Type

Describes the different kinds of grid generators.

Enumerator
PPL_GRID_GENERATOR_TYPE_LINE	The grid generator is a line.
PPL_GRID_GENERATOR_TYPE_PARAMETER	The grid generator is a parameter.
PPL_GRID_GENERATOR_TYPE_POINT	The grid generator is a point.

Definition at line 2036 of file ppl_c.h.

Function Documentation

int ppl_io_asprint_variable	(	char **	strp,
		ppl_dimension_type	var
	)

Pretty-prints var to a malloc-allocated string, a pointer to which is returned via strp.

Definition at line 2573 of file ppl_c_implementation_common.cc.

References PPL_ERROR_OUT_OF_MEMORY, and PPL_STDIO_ERROR.

int ppl_io_fprint_variable	(	FILE *	stream,
		ppl_dimension_type	var
	)

Pretty-prints var to the given output stream.

Definition at line 2564 of file ppl_c_implementation_common.cc.

References PPL_STDIO_ERROR.

int ppl_io_get_variable_output_function ( ppl_io_variable_output_function_type ** pp )

Writes a pointer to the current variable output function to pp.

Definition at line 2637 of file ppl_c_implementation_common.cc.

int ppl_io_print_variable ( ppl_dimension_type var )

Pretty-prints var to stdout.

Definition at line 2555 of file ppl_c_implementation_common.cc.

References PPL_STDIO_ERROR.

int ppl_io_set_variable_output_function ( ppl_io_variable_output_function_type * p )

Sets the output function to be used for printing variables to p.

Definition at line 2629 of file ppl_c_implementation_common.cc.

char* ppl_io_wrap_string	(	const char *	src,
		unsigned	indent_depth,
		unsigned	preferred_first_line_length,
		unsigned	preferred_line_length
	)

Utility function for the wrapping of lines of text.

Parameters

src	The source string holding the text to wrap.
indent_depth	The indentation depth.
preferred_first_line_length	The preferred length for the first line of text.
preferred_line_length	The preferred length for all the lines but the first one.