CBMC: /home/runner/work/cbmc/cbmc/src/ansi-c/goto-conversion/goto_check_c.cpp File Reference

CBMC

Loading...

Searching...

No Matches

Classes | Functions

goto_check_c.cpp File Reference

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

#include "goto_check_c.h"
#include <util/arith_tools.h>
#include <util/array_name.h>
#include <util/bitvector_expr.h>
#include <util/c_types.h>
#include <util/config.h>
#include <util/cprover_prefix.h>
#include <util/expr_util.h>
#include <util/find_symbols.h>
#include <util/floatbv_expr.h>
#include <util/ieee_float.h>
#include <util/invariant.h>
#include <util/mathematical_expr.h>
#include <util/message.h>
#include <util/options.h>
#include <util/pointer_expr.h>
#include <util/pointer_offset_size.h>
#include <util/pointer_predicates.h>
#include <util/simplify_expr.h>
#include <util/std_code.h>
#include <util/std_expr.h>
#include <goto-programs/goto_model.h>
#include <goto-programs/remove_skip.h>
#include <analyses/local_bitvector_analysis.h>
#include <ansi-c/c_expr.h>
#include <langapi/language.h>
#include <langapi/mode.h>
#include <algorithm>

+ Include dependency graph for goto_check_c.cpp:

Go to the source code of this file.

Classes

class goto_check_ct

struct goto_check_ct::conditiont

class flag_overridet

Allows to: More...

Functions

static exprt implication (exprt lhs, exprt rhs)

void goto_check_c (const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options, message_handlert &message_handler)

void goto_check_c (const namespacet &ns, const optionst &options, goto_functionst &goto_functions, message_handlert &message_handler)

void goto_check_c (const optionst &options, goto_modelt &goto_model, message_handlert &message_handler)

Detailed Description

Checks for Errors in C/C++ Programs.

Definition in file goto_check_c.cpp.

Function Documentation

◆ goto_check_c() [1/3]

void goto_check_c ( const irep_idt & function_identifier,

goto_functionst::goto_functiont & goto_function,

const namespacet & ns,

const optionst & options,

message_handlert & message_handler

)

Definition at line 2470 of file goto_check_c.cpp.

◆ goto_check_c() [2/3]

void goto_check_c ( const namespacet & ns,

const optionst & options,

goto_functionst & goto_functions,

message_handlert & message_handler

)

Definition at line 2481 of file goto_check_c.cpp.

◆ goto_check_c() [3/3]

void goto_check_c ( const optionst & options,

goto_modelt & goto_model,

message_handlert & message_handler

)

Definition at line 2497 of file goto_check_c.cpp.

◆ implication()

static exprt implication ( exprt lhs,

exprt rhs

)

static

Definition at line 421 of file goto_check_c.cpp.