CBMC
Loading...
Searching...
No Matches
gcc_mode.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Base class for command line interpretation
4
5Author: CM Wintersteiger
6
7Date: June 2006
8
9\*******************************************************************/
10
13
14#ifndef CPROVER_GOTO_CC_GCC_MODE_H
15#define CPROVER_GOTO_CC_GCC_MODE_H
16
17#include "gcc_message_handler.h"
18#include "goto_cc_mode.h"
19
20#include <ansi-c/gcc_version.h>
21
22#include <map>
23#include <set>
24
25class compilet;
26
28{
29public:
30 int doit() final;
31 void help_mode() final;
32
35 const std::string &_base_name,
37
38protected:
40
42
43 std::string native_tool_name;
44
45 const std::string goto_binary_tmp_suffix;
46
48 const std::map<std::string, std::set<std::string>> arch_map;
49
50 int preprocess(
51 const std::string &language,
52 const std::string &src,
53 const std::string &dest,
54 bool act_as_bcc);
55
57 int run_gcc(const compilet &compiler);
58
60
61 int asm_output(
62 bool act_as_bcc,
63 const std::list<std::string> &preprocessed_source_files,
64 const compilet &compiler);
65
66 static bool needs_preprocessing(const std::string &);
67
69};
70
71#endif // CPROVER_GOTO_CC_GCC_MODE_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
std::string native_tool_name
Definition gcc_mode.h:43
int preprocess(const std::string &language, const std::string &src, const std::string &dest, bool act_as_bcc)
call gcc for preprocessing
Definition gcc_mode.cpp:837
static bool needs_preprocessing(const std::string &)
Definition gcc_mode.cpp:294
int doit() final
does it.
Definition gcc_mode.cpp:309
const std::string goto_binary_tmp_suffix
Definition gcc_mode.h:45
int run_gcc(const compilet &compiler)
call gcc with original command line
Definition gcc_mode.cpp:916
gcc_message_handlert gcc_message_handler
Definition gcc_mode.h:39
void help_mode() final
display command line help
const std::map< std::string, std::set< std::string > > arch_map
Associate CBMC architectures with processor names.
Definition gcc_mode.h:48
gcc_versiont gcc_version
Definition gcc_mode.h:68
const bool produce_hybrid_binary
Definition gcc_mode.h:41
int asm_output(bool act_as_bcc, const std::list< std::string > &preprocessed_source_files, const compilet &compiler)
int gcc_hybrid_binary(compilet &compiler)
Definition gcc_mode.cpp:960
Command line interpretation for goto-cc.