CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
read_goto_binary.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Read Goto Programs
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_PROGRAMS_READ_GOTO_BINARY_H
13#define CPROVER_GOTO_PROGRAMS_READ_GOTO_BINARY_H
14
15#include <list>
16#include <optional>
17#include <string>
18
19class goto_modelt;
21
22std::optional<goto_modelt>
23read_goto_binary(const std::string &filename, message_handlert &);
24
25bool is_goto_binary(const std::string &filename, message_handlert &);
26
33 const std::list<std::string> &file_names,
34 goto_modelt &dest,
35 message_handlert &message_handler);
36
37#endif // CPROVER_GOTO_PROGRAMS_READ_GOTO_BINARY_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
bool read_objects_and_link(const std::list< std::string > &file_names, goto_modelt &dest, message_handlert &message_handler)
Reads object files and updates the config if any files were read.
bool is_goto_binary(const std::string &filename, message_handlert &)
std::optional< goto_modelt > read_goto_binary(const std::string &filename, message_handlert &)
Read a goto binary from a file, but do not update config.