validate_expressions.cpp File Reference

#include "validate_expressions.h"
#include "validate_helpers.h"
#include "bitvector_expr.h"
#include "pointer_expr.h"
#include "ssa_expr.h"

Include dependency graph for validate_expressions.cpp:

Go to the source code of this file.

Macros
#define	CALL_ON_EXPR(expr_type)    C<exprt, expr_type>()(expr, std::forward<Args>(args)...)

Functions
template<template< typename, typename > class C, typename... Args>
void	call_on_expr (const exprt &expr, Args &&... args)
void	check_expr (const exprt &expr, const validation_modet vm)
	Check that the given expression is well-formed (shallow checks only, i.e., subexpressions and its type are not checked) More...
void	validate_expr (const exprt &expr, const namespacet &ns, const validation_modet vm)
	Check that the given expression is well-formed, assuming that its subexpression and type have already been checked for well-formedness. More...
void	validate_full_expr (const exprt &expr, const namespacet &ns, const validation_modet vm)
	Check that the given expression is well-formed (full check, including checks of all subexpressions and the type) More...

Macro Definition Documentation

CALL_ON_EXPR

#define CALL_ON_EXPR

(

expr_type

)

C<exprt, expr_type>()(expr, std::forward<Args>(args)...)

Definition at line 20 of file validate_expressions.cpp.

Function Documentation

call_on_expr()

template<template< typename, typename > class C, typename... Args>

void call_on_expr	(	const exprt &	expr,
		Args &&...	args
	)

Definition at line 24 of file validate_expressions.cpp.

check_expr()

void check_expr	(	const exprt &	expr,
		const validation_modet	vm
	)

Check that the given expression is well-formed (shallow checks only, i.e., subexpressions and its type are not checked)

The function determines the type T of the expression expr (by inspecting the id() field) and then calls T::check(expr, vm).

The validation mode indicates whether well-formedness check failures are reported via DATA_INVARIANT violations or exceptions.

Definition at line 85 of file validate_expressions.cpp.

validate_expr()

void validate_expr	(	const exprt &	expr,
		const namespacet &	ns,
		const validation_modet	vm
	)

Check that the given expression is well-formed, assuming that its subexpression and type have already been checked for well-formedness.

The function determines the type T of the expression expr (by inspecting the id() field) and then calls T::validate(expr, ns, vm).

The validation mode indicates whether well-formedness check failures are reported via DATA_INVARIANT violations or exceptions.

Definition at line 98 of file validate_expressions.cpp.

validate_full_expr()

void validate_full_expr	(	const exprt &	expr,
		const namespacet &	ns,
		const validation_modet	vm
	)

Check that the given expression is well-formed (full check, including checks of all subexpressions and the type)

The function determines the type T of the expression expr (by inspecting the id() field) and then calls T::validate_full(expr, ns, vm).

The validation mode indicates whether well-formedness check failures are reported via DATA_INVARIANT violations or exceptions.

Definition at line 114 of file validate_expressions.cpp.