Loading...

Searching...

No Matches

c_safety_checks.cpp File Reference

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 )

static

Definition at line 234 of file c_safety_checks.cpp.