Checks for Errors in C/C++ Programs. More...

#include "c_safety_checks.h"
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/pointer_expr.h>
#include <util/pointer_offset_size.h>
#include <util/pointer_predicates.h>
#include <goto-programs/goto_model.h>
#include <ansi-c/expr2c.h>

Include dependency graph for c_safety_checks.cpp:

Go to the source code of this file.

Enumerations
enum class	access_typet { R , W }

Functions
exprt	index_array_size (const typet &type)

void	c_safety_checks_rec (goto_functionst::function_mapt::value_type &, const exprt::operandst &guards, const exprt &, access_typet, const namespacet &, goto_programt &)

void	c_safety_checks_address_rec (goto_functionst::function_mapt::value_type &f, const exprt::operandst &guards, const exprt &expr, const namespacet &ns, goto_programt &dest)

static exprt	guard (const exprt::operandst &guards, exprt cond)

void	c_safety_checks (goto_functionst::function_mapt::value_type &f, const exprt &expr, access_typet access_type, const namespacet &ns, goto_programt &dest)

static exprt	offset_is_zero (const exprt &pointer)

void	c_safety_checks (goto_functionst::function_mapt::value_type &f, const namespacet &ns)

void	c_safety_checks (goto_modelt &goto_model)

void	no_assertions (goto_functionst::function_mapt::value_type &f)

void	no_assertions (goto_modelt &goto_model)

Detailed Description

Checks for Errors in C/C++ Programs.

Definition in file c_safety_checks.cpp.

Enumeration Type Documentation

◆ access_typet

enum class access_typet

strong

Enumerator
R
W

Definition at line 34 of file c_safety_checks.cpp.

Function Documentation

◆ c_safety_checks() [1/3]

void c_safety_checks	(	goto_functionst::function_mapt::value_type &	f,
		const exprt &	expr,
		access_typet	access_type,
		const namespacet &	ns,
		goto_programt &	dest
	)

Definition at line 224 of file c_safety_checks.cpp.

◆ c_safety_checks() [2/3]

void c_safety_checks	(	goto_functionst::function_mapt::value_type &	f,
		const namespacet &	ns
	)

Definition at line 241 of file c_safety_checks.cpp.

◆ c_safety_checks() [3/3]

void c_safety_checks ( goto_modelt & goto_model )

Definition at line 418 of file c_safety_checks.cpp.

◆ c_safety_checks_address_rec()

void c_safety_checks_address_rec	(	goto_functionst::function_mapt::value_type &	f,
		const exprt::operandst &	guards,
		const exprt &	expr,
		const namespacet &	ns,
		goto_programt &	dest
	)

Definition at line 48 of file c_safety_checks.cpp.

◆ c_safety_checks_rec()

void c_safety_checks_rec	(	goto_functionst::function_mapt::value_type &	f,
		const exprt::operandst &	guards,
		const exprt &	expr,
		access_typet	access_type,
		const namespacet &	ns,
		goto_programt &	dest
	)

Definition at line 77 of file c_safety_checks.cpp.

◆ guard()

static exprt guard	(	const exprt::operandst &	guards,
		exprt	cond
	)

static

Definition at line 69 of file c_safety_checks.cpp.

◆ index_array_size()

exprt index_array_size ( const typet & type )

Definition at line 24 of file c_safety_checks.cpp.

◆ no_assertions() [1/2]

void no_assertions ( goto_functionst::function_mapt::value_type & f )

Definition at line 429 of file c_safety_checks.cpp.

◆ no_assertions() [2/2]

void no_assertions ( goto_modelt & goto_model )

Definition at line 444 of file c_safety_checks.cpp.

◆ offset_is_zero()

static exprt offset_is_zero ( const exprt & pointer )