cprover
goto_check.cpp File Reference

GOTO Programs. More...

#include "goto_check.h"
#include <algorithm>
#include <util/simplify_expr.h>
#include <util/array_name.h>
#include <util/ieee_float.h>
#include <util/arith_tools.h>
#include <util/expr_util.h>
#include <util/find_symbols.h>
#include <util/std_expr.h>
#include <util/std_types.h>
#include <util/guard.h>
#include <util/base_type.h>
#include <util/pointer_offset_size.h>
#include <util/pointer_predicates.h>
#include <util/cprover_prefix.h>
#include <util/options.h>
#include <langapi/language.h>
#include <langapi/mode.h>
#include <goto-programs/remove_skip.h>
#include "local_bitvector_analysis.h"
Include dependency graph for goto_check.cpp:

Go to the source code of this file.

Classes

class  goto_checkt
 

Functions

void goto_check (const namespacet &ns, const optionst &options, const irep_idt &mode, goto_functionst::goto_functiont &goto_function)
 
void goto_check (const namespacet &ns, const optionst &options, goto_functionst &goto_functions)
 
void goto_check (const optionst &options, goto_modelt &goto_model)
 

Detailed Description

GOTO Programs.

Definition in file goto_check.cpp.

Function Documentation

◆ goto_check() [1/3]

◆ goto_check() [2/3]

void goto_check ( const namespacet ns,
const optionst options,
goto_functionst goto_functions 
)

Definition at line 1773 of file goto_check.cpp.

References Forall_goto_functions, goto_check(), and namespacet::lookup().

◆ goto_check() [3/3]

void goto_check ( const optionst options,
goto_modelt goto_model 
)