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.

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

typedef struct ppl_Coefficient_tag *	ppl_Coefficient_t
	Opaque pointer.

typedef struct ppl_Coefficient_tag const *	ppl_const_Coefficient_t
	Opaque pointer to const object.

typedef struct ppl_Linear_Expression_tag *	ppl_Linear_Expression_t
	Opaque pointer.

typedef struct ppl_Linear_Expression_tag const *	ppl_const_Linear_Expression_t
	Opaque pointer to const object.

typedef struct ppl_Constraint_tag *	ppl_Constraint_t
	Opaque pointer.

typedef struct ppl_Constraint_tag const *	ppl_const_Constraint_t
	Opaque pointer to const object.

typedef struct ppl_Constraint_System_tag *	ppl_Constraint_System_t
	Opaque pointer.

typedef struct ppl_Constraint_System_tag const *	ppl_const_Constraint_System_t
	Opaque pointer to const object.

typedef struct ppl_Constraint_System_const_iterator_tag *	ppl_Constraint_System_const_iterator_t
	Opaque pointer.

typedef struct ppl_Constraint_System_const_iterator_tag const *	ppl_const_Constraint_System_const_iterator_t
	Opaque pointer to const object.

typedef struct ppl_Generator_tag *	ppl_Generator_t
	Opaque pointer.

typedef struct ppl_Generator_tag const *	ppl_const_Generator_t
	Opaque pointer to const object.

typedef struct ppl_Generator_System_tag *	ppl_Generator_System_t
	Opaque pointer.

typedef struct ppl_Generator_System_tag const *	ppl_const_Generator_System_t
	Opaque pointer to const object.

typedef struct ppl_Generator_System_const_iterator_tag *	ppl_Generator_System_const_iterator_t
	Opaque pointer.

typedef struct ppl_Generator_System_const_iterator_tag const *	ppl_const_Generator_System_const_iterator_t
	Opaque pointer to const object.

typedef struct ppl_Congruence_tag *	ppl_Congruence_t
	Opaque pointer.

typedef struct ppl_Congruence_tag const *	ppl_const_Congruence_t
	Opaque pointer to const object.

typedef struct ppl_Congruence_System_tag *	ppl_Congruence_System_t
	Opaque pointer.

typedef struct ppl_Congruence_System_tag const *	ppl_const_Congruence_System_t
	Opaque pointer to const object.

typedef struct ppl_Congruence_System_const_iterator_tag *	ppl_Congruence_System_const_iterator_t
	Opaque pointer.

typedef struct ppl_Congruence_System_const_iterator_tag const *	ppl_const_Congruence_System_const_iterator_t
	Opaque pointer to const object.

typedef struct ppl_Grid_Generator_tag *	ppl_Grid_Generator_t
	Opaque pointer.

typedef struct ppl_Grid_Generator_tag const *	ppl_const_Grid_Generator_t
	Opaque pointer to const object.

typedef struct ppl_Grid_Generator_System_tag *	ppl_Grid_Generator_System_t
	Opaque pointer.

typedef struct ppl_Grid_Generator_System_tag const *	ppl_const_Grid_Generator_System_t
	Opaque pointer to const object.

typedef struct ppl_Grid_Generator_System_const_iterator_tag *	ppl_Grid_Generator_System_const_iterator_t
	Opaque pointer.

typedef struct ppl_Grid_Generator_System_const_iterator_tag const *	ppl_const_Grid_Generator_System_const_iterator_t
	Opaque pointer to const object.

typedef struct ppl_MIP_Problem_tag *	ppl_MIP_Problem_t
	Opaque pointer.

typedef struct ppl_MIP_Problem_tag const *	ppl_const_MIP_Problem_t
	Opaque pointer to const object.

typedef struct ppl_PIP_Problem_tag *	ppl_PIP_Problem_t
	Opaque pointer.

typedef struct ppl_PIP_Problem_tag const *	ppl_const_PIP_Problem_t
	Opaque pointer to const object.

typedef struct ppl_PIP_Tree_Node_tag *	ppl_PIP_Tree_Node_t
	Opaque pointer.

typedef struct ppl_PIP_Tree_Node_tag const *	ppl_const_PIP_Tree_Node_t
	Opaque pointer to const object.

typedef struct ppl_PIP_Decision_Node_tag *	ppl_PIP_Decision_Node_t
	Opaque pointer.

typedef struct ppl_PIP_Decision_Node_tag const *	ppl_const_PIP_Decision_Node_t
	Opaque pointer to const object.

typedef struct ppl_PIP_Solution_Node_tag *	ppl_PIP_Solution_Node_t
	Opaque pointer.

typedef struct ppl_PIP_Solution_Node_tag const *	ppl_const_PIP_Solution_Node_t
	Opaque pointer to const object.

typedef struct ppl_Artificial_Parameter_tag *	ppl_Artificial_Parameter_t
	Opaque pointer.

typedef struct ppl_Artificial_Parameter_tag const *	ppl_const_Artificial_Parameter_t
	Opaque pointer to const object.

typedef struct ppl_Artificial_Parameter_Sequence_tag *	ppl_Artificial_Parameter_Sequence_t
	Opaque pointer.

typedef struct ppl_Artificial_Parameter_Sequence_tag const *	ppl_const_Artificial_Parameter_Sequence_t
	Opaque pointer to const object.

typedef struct ppl_Artificial_Parameter_Sequence_const_iterator_tag *	ppl_Artificial_Parameter_Sequence_const_iterator_t
	Opaque pointer.

typedef struct ppl_Artificial_Parameter_Sequence_const_iterator_tag const *	ppl_const_Artificial_Parameter_Sequence_const_iterator_t
	Opaque pointer to const object.

typedef struct ppl_Polyhedron_tag *	ppl_Polyhedron_t
	Opaque pointer.

typedef struct ppl_Polyhedron_tag const *	ppl_const_Polyhedron_t
	Opaque pointer to const object.

typedef struct ppl_Pointset_Powerset_C_Polyhedron_tag *	ppl_Pointset_Powerset_C_Polyhedron_t
	Opaque pointer.

typedef struct ppl_Pointset_Powerset_C_Polyhedron_tag const *	ppl_const_Pointset_Powerset_C_Polyhedron_t
	Opaque pointer to const object.

typedef struct ppl_Pointset_Powerset_C_Polyhedron_iterator_tag *	ppl_Pointset_Powerset_C_Polyhedron_iterator_t
	Opaque pointer.

typedef struct ppl_Pointset_Powerset_C_Polyhedron_iterator_tag const *	ppl_const_Pointset_Powerset_C_Polyhedron_iterator_t
	Opaque pointer to const object.

typedef struct ppl_Pointset_Powerset_C_Polyhedron_const_iterator_tag *	ppl_Pointset_Powerset_C_Polyhedron_const_iterator_t
	Opaque pointer.

typedef struct ppl_Pointset_Powerset_C_Polyhedron_const_iterator_tag const *	ppl_const_Pointset_Powerset_C_Polyhedron_const_iterator_t
	Opaque pointer to const object.

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.

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

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

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

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`.

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`.

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`.

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.

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

unsigned int	PPL_COMPLEXITY_CLASS_ANY
	Code of the universal complexity class.

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

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.

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

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

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

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 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.

Enumeration Type Documentation

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 .

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.

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.

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.

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.

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.

Function Documentation

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.

Returns: The wrapped string in a malloc-allocated buffer.

Typedefs

Enumerations

Functions

Variables

Detailed Description

Typedef Documentation

Enumeration Type Documentation

Function Documentation