#include "invariant.h"
#include <string>

Include dependency graph for invariant_utils.h:

This graph shows which files directly or indirectly include this file:

Macros
#define	INVARIANT_WITH_IREP(CONDITION, DESCRIPTION, IREP)
	Equivalent to `INVARIANT_STRUCTURED(CONDITION, invariant_failedt, pretty_print_invariant_with_irep(IREP, DESCRIPTION))` More...

#define	PRECONDITION_WITH_IREP(CONDITION, DESCRIPTION, IREP) INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP))
	See `INVARIANT_WITH_IREP` More...

#define	POSTCONDITION_WITH_IREP(CONDITION, DESCRIPTION, IREP) INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP))

#define	CHECK_RETURN_WITH_IREP(CONDITION, DESCRIPTION, IREP) INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP))

#define	UNREACHABLE_WITH_IREP(CONDITION, DESCRIPTION, IREP) INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP))

#define	DATA_INVARIANT_WITH_IREP(CONDITION, DESCRIPTION, IREP) INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP))

Functions
std::string	pretty_print_invariant_with_irep (const irept &problem_node, const std::string &description)
	Produces a plain string error description from an irep and some explanatory text. More...

Macro Definition Documentation

◆ CHECK_RETURN_WITH_IREP

#define CHECK_RETURN_WITH_IREP	(	CONDITION,
		DESCRIPTION,
		IREP
	)	INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP))

Definition at line 41 of file invariant_utils.h.

◆ DATA_INVARIANT_WITH_IREP

#define DATA_INVARIANT_WITH_IREP	(	CONDITION,
		DESCRIPTION,
		IREP
	)	INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP))

Definition at line 45 of file invariant_utils.h.

◆ INVARIANT_WITH_IREP

#define INVARIANT_WITH_IREP	(	CONDITION,
		DESCRIPTION,
		IREP
	)

Value:

  INVARIANT_STRUCTURED(                                                 \
    CONDITION,                                                          \
    invariant_failedt,                                                  \
    pretty_print_invariant_with_irep((IREP), (DESCRIPTION)))

Equivalent to INVARIANT_STRUCTURED(CONDITION, invariant_failedt, pretty_print_invariant_with_irep(IREP, DESCRIPTION))

Definition at line 30 of file invariant_utils.h.

◆ POSTCONDITION_WITH_IREP

#define POSTCONDITION_WITH_IREP	(	CONDITION,
		DESCRIPTION,
		IREP
	)	INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP))

Definition at line 39 of file invariant_utils.h.

◆ PRECONDITION_WITH_IREP

#define PRECONDITION_WITH_IREP	(	CONDITION,
		DESCRIPTION,
		IREP
	)	INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP))

See INVARIANT_WITH_IREP

Definition at line 37 of file invariant_utils.h.

◆ UNREACHABLE_WITH_IREP

#define UNREACHABLE_WITH_IREP	(	CONDITION,
		DESCRIPTION,
		IREP
	)	INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP))

Definition at line 43 of file invariant_utils.h.

Function Documentation

◆ pretty_print_invariant_with_irep()

std::string pretty_print_invariant_with_irep	(	const irept &	problem_node,
		const std::string &	description
	)

Produces a plain string error description from an irep and some explanatory text.

If problem_node is nil, returns description.

Parameters

problem_node	irep to pretty-print
description	descriptive text to prepend

Returns: error message

Definition at line 16 of file invariant_utils.cpp.

Macros

Functions