CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
get_goto_model_from_c.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Get goto model
4
5Author: Daniel Poetzl
6
7\*******************************************************************/
8
9#ifndef CPROVER_TESTING_UTILS_GET_GOTO_MODEL_FROM_C_H
10#define CPROVER_TESTING_UTILS_GET_GOTO_MODEL_FROM_C_H
11
13
14#include <iosfwd>
15
20goto_modelt get_goto_model_from_c(const std::string &code);
21
26goto_modelt get_goto_model_from_c(const std::istream &in);
27
28#endif /* CPROVER_TESTING_UTILS_GET_GOTO_MODEL_FROM_C_H_ */
goto_modelt get_goto_model_from_c(const std::string &code)
Convert C program to a goto model.
Symbol Table + CFG.