cprover
Loading...
Searching...
No Matches
compile.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Compile and link source and object files.
4
5Author: CM Wintersteiger
6
7Date: June 2006
8
9\*******************************************************************/
10
13
14#ifndef CPROVER_GOTO_CC_COMPILE_H
15#define CPROVER_GOTO_CC_COMPILE_H
16
17#include <util/message.h>
18#include <util/std_types.h>
19#include <util/symbol.h>
20
21#include <map>
22
23class cmdlinet;
24class goto_functionst;
25class goto_modelt;
26class language_filest;
27class languaget;
28class symbol_tablet;
29
31{
32public:
33 // configuration
35 bool validate_goto_model = false;
36
37 enum { PREPROCESS_ONLY, // gcc -E
38 COMPILE_ONLY, // gcc -c
39 ASSEMBLE_ONLY, // gcc -S
40 LINK_LIBRARY, // ld -r
41 COMPILE_LINK, // gcc -shared
44
45 std::list<std::string> library_paths;
46 std::list<std::string> source_files;
47 std::list<std::string> object_files;
48 std::list<std::string> libraries;
49
52
53 // the two options below are mutually exclusive -- use either or
55
56 compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror);
57
58 ~compilet();
59
60 bool add_input_file(const std::string &);
61 bool find_library(const std::string &);
62 bool add_files_from_archive(const std::string &file_name, bool thin_archive);
63
64 bool parse(const std::string &filename, language_filest &);
65 bool parse_stdin(languaget &);
66 bool doit();
68 bool link(optionalt<symbol_tablet> &&symbol_table);
69
70 optionalt<symbol_tablet> parse_source(const std::string &);
71
79 static bool write_bin_object_file(
80 const std::string &file_name,
81 const goto_modelt &src_goto_model,
83 message_handlert &message_handler);
84
86 bool wrote_object_files() const { return wrote_object; }
87
94 std::size_t> &cprover_macros) const
95 {
97 for(const auto &pair : written_macros)
98 cprover_macros.insert({pair.first,
99 to_code_type(pair.second.type).parameters().size()});
100 }
101
102protected:
103 std::string working_directory;
104 std::string override_language;
105
106 std::list<std::string> tmp_dirs;
107 std::list<irep_idt> seen_modes;
108
112
114 const bool keep_file_local;
115
117 const std::string file_local_mangle_suffix;
118
119 static std::size_t function_body_count(const goto_functionst &);
120
122 const std::string &file_name,
123 const goto_modelt &src_goto_model)
124 {
126 file_name,
127 src_goto_model,
130 {
131 return true;
132 }
133
134 wrote_object = true;
135
136 return false;
137 }
138
140
142
143 bool add_written_cprover_symbols(const symbol_tablet &symbol_table);
144 std::map<irep_idt, symbolt> written_macros;
145
146 // clients must only call add_written_cprover_symbols() if an object
147 // file has been written. The case where an object file was written
148 // but there were no __CPROVER symbols in the goto-program is distinct
149 // from the case where the user forgot to write an object file before
150 // calling add_written_cprover_symbols().
152};
153
154#endif // CPROVER_GOTO_CC_COMPILE_H
const parameterst & parameters() const
Definition: std_types.h:655
@ ASSEMBLE_ONLY
Definition: compile.h:39
@ LINK_LIBRARY
Definition: compile.h:40
@ PREPROCESS_ONLY
Definition: compile.h:37
@ COMPILE_LINK_EXECUTABLE
Definition: compile.h:42
@ COMPILE_ONLY
Definition: compile.h:38
@ COMPILE_LINK
Definition: compile.h:41
void add_compiler_specific_defines() const
Definition: compile.cpp:691
cmdlinet & cmdline
Definition: compile.h:110
bool wrote_object
Definition: compile.h:151
bool parse_stdin(languaget &)
parses a source file (low-level parsing)
Definition: compile.cpp:538
bool parse(const std::string &filename, language_filest &)
parses a source file (low-level parsing)
Definition: compile.cpp:451
std::string working_directory
Definition: compile.h:103
std::list< std::string > tmp_dirs
Definition: compile.h:106
bool echo_file_name
Definition: compile.h:34
std::string override_language
Definition: compile.h:104
std::string output_file_object
Definition: compile.h:54
bool write_bin_object_file(const std::string &file_name, const goto_modelt &src_goto_model)
Definition: compile.h:121
bool add_input_file(const std::string &)
puts input file names into a list and does preprocessing for libraries.
Definition: compile.cpp:173
std::list< std::string > libraries
Definition: compile.h:48
std::list< irep_idt > seen_modes
Definition: compile.h:107
bool link(optionalt< symbol_tablet > &&symbol_table)
parses object files and links them
Definition: compile.cpp:315
std::string output_directory_object
Definition: compile.h:54
void cprover_macro_arities(std::map< irep_idt, std::size_t > &cprover_macros) const
__CPROVER_... macros written to object files and their arities
Definition: compile.h:93
std::list< std::string > object_files
Definition: compile.h:47
bool doit()
reads and source and object files, compiles and links them into goto program objects.
Definition: compile.cpp:60
std::list< std::string > source_files
Definition: compile.h:46
~compilet()
cleans up temporary files
Definition: compile.cpp:672
bool wrote_object_files() const
Has this compiler written any object files?
Definition: compile.h:86
bool add_written_cprover_symbols(const symbol_tablet &symbol_table)
Definition: compile.cpp:739
std::string object_file_extension
Definition: compile.h:50
bool validate_goto_model
Definition: compile.h:35
const bool keep_file_local
Whether to keep implementations of file-local symbols.
Definition: compile.h:114
bool warning_is_fatal
Definition: compile.h:111
static std::size_t function_body_count(const goto_functionst &)
Definition: compile.cpp:680
optionalt< symbol_tablet > parse_source(const std::string &)
Parses and type checks a source file located at file_name.
Definition: compile.cpp:620
void convert_symbols(goto_modelt &)
Definition: compile.cpp:697
std::map< irep_idt, symbolt > written_macros
Definition: compile.h:144
bool add_files_from_archive(const std::string &file_name, bool thin_archive)
extracts goto binaries from AR archive and add them as input files.
Definition: compile.cpp:214
bool find_library(const std::string &)
tries to find a library object file that matches the given library name.
Definition: compile.cpp:274
enum compilet::@3 mode
messaget log
Definition: compile.h:109
static bool write_bin_object_file(const std::string &file_name, const goto_modelt &src_goto_model, bool validate_goto_model, message_handlert &message_handler)
Writes the goto functions of src_goto_model to a binary format object file.
Definition: compile.cpp:574
const std::string file_local_mangle_suffix
String to include in all mangled names.
Definition: compile.h:117
optionalt< symbol_tablet > compile()
Parses source files and writes object files, or keeps the symbols in the symbol_table if not compilin...
Definition: compile.cpp:369
std::list< std::string > library_paths
Definition: compile.h:45
std::string output_file_executable
Definition: compile.h:51
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
A collection of goto functions.
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
message_handlert & get_message_handler()
Definition: message.h:184
The symbol table.
Definition: symbol_table.h:14
nonstd::optional< T > optionalt
Definition: optional.h:35
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
Pre-defined types.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
Symbol table entry.