ellipsis-contracts.h File Reference

Implement preconditions, postconditions and similar features. More...

Go to the source code of this file.

Macros
#define	ELLIPSIS_CONTRACT_ASSERT_IMPL(CTYPE, COND, CSTR, ...)
	Intermediate macro that remains from an assertion after a first step of preprocessing by eĿlipsis.
#define	ELLIPSIS_CONTRACT_ASSUME_IMPL(CTYPE, COND, CSTR, ...)
	Intermediate macro that remains from an assumption after a first step of preprocessing by eĿlipsis.

Detailed Description

Implement preconditions, postconditions and similar features.

This implements macros that can be used to assert or assume specific properties:

• An assertion is a condition that is checked each time the execution reaches it and if it is not fulfilled leads to the abortion of the program
• An assumption is a condition that is known hold and if it is not fulfilled leads to undefined behavior.

Both types of conditions are considered to be bugs if they are not fulfilled. Therefore if such a condition can be proven not to hold at compile time, at static_assert triggers and ends the compilation, and that even if assertions are set to be ignored.

The closest to assertions in the C library is the macro assert from <assert.h>, but which has two drawbacks

• If it is switched off by setting NDEBUG (no-debug), the condition is not even checked syntactically. This makes it difficult to maintain assertions through the life cycle of a code and has it that sometimes warnings for unused variables appear.
• If it is switched off by setting NDEBUG the control flow of the code after the assert changes. If the assert is active, the compiler can assume that a condition holds after it, if it is inactive such optimizations cannot be made any more. So code without the assert might be slower instead of faster.

The macros for assertion and assumption contracts are meant to avoid these problems. They avoid the first, by ensuring that the condition is always visible to the compiler, even if it is possible to switch the test off for assertions. The second is not well addressed by assertions, only assumptions warrant that the condition is always taken into account after them.

For each of these two strategies of dealing with conditions, there are four macros that situate the condition at a specific time during the execution of a function. For assertions these are

• At a specific point in the function: ellipsis_contracts_assert
• Before the call: ellipsis_contracts_pre
• After the call: ellipsis_contracts_post
• Before and after the call: ellipsis_contracts_invariant

Currently, ellipsis is not able to implement the latter three really on the caller side. Instead, "preconditions" are tested at the beginning of the execution, "postconditions" are scheduled at the end (by using defer), and "invariants" combine the two. To have the same effects as pre- and postconditions as C++ has them in the function interface, the function code should be visible to the caller, e.g by having it as an inline function.

For assumptions there are four macros with similar specification:

• At a specific point in the function: ellipsis_contracts_assume
• Before the call: ellipsis_contracts_premise
• After the call: ellipsis_contracts_conclusion
• Before and after the call: ellipsis_contracts_fact

Note the difference to assertions. Here, the user guarantees that the condition holds, it is not even necessary to test it, and the compiler can then rely on this knowledge. Whether or not the condition is really checked is at the discretion of the compiler. A macro ELLIPSIS_CONTRACTS_VERBOSE can be used to force the check of the condition and produces a report if it failed.

Policies

Assertions can be regulated by policies, but in general messing with this is not a good idea because this might change the behavior of the program. Assertions may be turned off by defining the macro ELLIPSIS_CONTRACTS_UNCHECKED. If set, runtime checks of assertions are disabled. A second macro, ELLIPSIS_CONTRACTS_PROCEED, allows execution to continue after an assertion failed and that failure has been reported. Alternatively, by setting ELLIPSIS_CONTRACTS_DYNAMIC, these policy choices can be delayed to execution time, see below.

For both modes, assertion and assumption, the macro ELLIPSIS_CONTRACTS_DYNAMIC switches to runtime driven dynamic policies. If used assertions and assumptions expect bool variables ellipsis∷contracts∷ignore∷dynamic, ellipsis∷contracts∷proceed∷dynamic and ellipsis∷contracts∷verbose∷dynamic to be defined somewhere. This can be done on a per function base and so each function can e.g have its own policy. For example one function could have

constexpr bool ellipsis∷contracts∷ignore∷dynamic = false;
constexpr bool ellipsis∷contracts∷proceed∷dynamic = false;
constexpr bool ellipsis∷contracts∷verbose∷dynamic = true;

to have a compile-time fixed policy, and another function could have

bool ellipsis∷contracts∷ignore∷dynamic = false;
bool ellipsis∷contracts∷proceed∷dynamic = false;
bool ellipsis∷contracts∷verbose∷dynamic = true;

that would for example make it possible to change the policy within a debugger.

If no such local variables are defined, three global variables are expected to be defined in some of the .o files. They have to have the following signatures:

thread_local bool volatile ellipsis∷contracts∷ignore∷dynamic;
thread_local bool volatile ellipsis∷contracts∷proceed∷dynamic;
thread_local bool volatile ellipsis∷contracts∷verbose∷dynamic;

But as indicated, messing around with these settings may have an impact on the control flow and should only be done occasionally for debugging, for example.

Macro Definition Documentation

ELLIPSIS_CONTRACT_ASSERT_IMPL

#define ELLIPSIS_CONTRACT_ASSERT_IMPL	(		CTYPE,
			COND,
			CSTR,
			...
	)

Intermediate macro that remains from an assertion after a first step of preprocessing by eĿlipsis.

This should be fully expanded after complete preprocessing.

See also

ellipsis-contracts.h

ellipsis-contracts-macros.h

ellipsis-interface.h

Warning

This macro may not be undefined or changed otherwise

ELLIPSIS_CONTRACT_ASSUME_IMPL

#define ELLIPSIS_CONTRACT_ASSUME_IMPL	(		CTYPE,
			COND,
			CSTR,
			...
	)

Intermediate macro that remains from an assumption after a first step of preprocessing by eĿlipsis.

This should be fully expanded after complete preprocessing.

See also

ellipsis-contracts.h

ellipsis-contracts-macros.h

ellipsis-interface.h

Warning

This macro may not be undefined or changed otherwise