|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
#include <goto-programs/goto_functions.h>#include <goto-programs/goto_program.h>#include <util/symtab/namespace.h>#include <util/config/options.h>#include <util/expr/type_byte_size.h>Go to the source code of this file.
Functions | |
| void | goto_check (const namespacet &ns, optionst &options, goto_functionst &goto_functions) |
| void goto_check | ( | const namespacet & | ns, |
| optionst & | options, | ||
| goto_functionst & | goto_functions ) |