#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/make_unique.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/prefix.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 <langapi/language.h>
#include <langapi/mode.h>
#include <algorithm>
#include <optional>

Include dependency graph for goto_check_c.cpp:

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 2397 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 2408 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 2424 of file goto_check_c.cpp.

◆ implication()

static exprt implication	(	exprt	lhs,
		exprt	rhs
	)

static

Definition at line 408 of file goto_check_c.cpp.