CBMC
Loading...
Searching...
No Matches
Enumerations | Functions
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

 
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)
 
 
void  c_safety_checks (goto_functionst::function_mapt::value_type &f, const exprt &expr, access_typet access_type, const namespacet &ns, goto_programt &dest)
 
 
void  c_safety_checks (goto_functionst::function_mapt::value_type &f, const namespacet &ns)
 
 
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

Enumerator

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 exprtexpr,
access_typet  access_type,
const namespacetns,
goto_programtdest 
)

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 namespacetns 
)

Definition at line 241 of file c_safety_checks.cpp.

◆  c_safety_checks() [3/3]

void c_safety_checks ( goto_modeltgoto_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::operandstguards,
const exprtexpr,
const namespacetns,
goto_programtdest 
)

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::operandstguards,
const exprtexpr,
access_typet  access_type,
const namespacetns,
goto_programtdest 
)

Definition at line 77 of file c_safety_checks.cpp.

◆  guard()

static exprt guard ( const exprt::operandstguards,
exprt  cond 
)
static

Definition at line 69 of file c_safety_checks.cpp.

◆  index_array_size()

exprt index_array_size ( const typettype )

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_modeltgoto_model )

Definition at line 444 of file c_safety_checks.cpp.

◆  offset_is_zero()

static exprt offset_is_zero ( const exprtpointer )
static

Definition at line 234 of file c_safety_checks.cpp.

AltStyle によって変換されたページ (->オリジナル) /