cprover
goto_check.h File Reference

Checks for Errors in C and Java Programs. More...

+ Include dependency graph for goto_check.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

void goto_check (const namespacet &, const optionst &, goto_functionst &, message_handlert &)
 
void goto_check (const irep_idt &function_identifier, goto_functionst::goto_functiont &, const namespacet &, const optionst &, message_handlert &)
 
void goto_check (const optionst &, goto_modelt &, message_handlert &)
 

Detailed Description

Checks for Errors in C and Java Programs.

Definition in file goto_check.h.

Function Documentation

◆ goto_check() [1/3]

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

Definition at line 18 of file goto_check.cpp.

◆ goto_check() [2/3]

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

Definition at line 34 of file goto_check.cpp.

◆ goto_check() [3/3]

void goto_check ( const optionst options,
goto_modelt goto_model,
message_handlert message_handler 
)

Definition at line 43 of file goto_check.cpp.