cprover
Loading...
Searching...
No Matches
goto_check.cpp File Reference

GOTO Programs. More...

#include "goto_check.h"
#include "goto_check_c.h"
#include <util/symbol.h>
+ Include dependency graph for goto_check.cpp:

Go to the source code of this file.

Functions

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

Detailed Description

GOTO Programs.

Definition in file goto_check.cpp.

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.