symex_invariant.cpp File Reference

#include <cstdio>
#include <cstdlib>
#include <goto-symex/symex_invariant.h>
#include <util/message/message.h>

Include dependency graph for symex_invariant.cpp:

Functions
void	symex_invariant_violated (const char *file, unsigned line, const char *function, const char *condition, const char *reason)
	Release-checked invariant for goto-symex.

Function Documentation

symex_invariant_violated()

void symex_invariant_violated	(	const char *	file,
		unsigned	line,
		const char *	function,
		const char *	condition,
		const char *	reason )

Release-checked invariant for goto-symex.

Every shipping configuration compiles with -DNDEBUG, so a violated invariant here means the verifier's own state is inconsistent and any verdict after it rests on nothing.

Reserved for checks no costlier than a comparison — see docs/roadmap/goto-symex-verification-plan.md, finding R1.