CBMC
cpp_language.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: C++ Language Module
4 
5 Author: Daniel Kroening, kroening@cs.cmu.edu
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_CPP_CPP_LANGUAGE_H
13 #define CPROVER_CPP_CPP_LANGUAGE_H
14 
15 #include <memory>
16 
18 
19 #include <langapi/language.h>
20 
21 #include "cpp_parse_tree.h"
22 
24 {
25 public:
26  void
27  set_language_options(const optionst &options, message_handlert &) override
28  {
29  object_factory_params.set(options);
30  }
31 
32  bool preprocess(
33  std::istream &instream,
34  const std::string &path,
35  std::ostream &outstream,
36  message_handlert &message_handler) override;
37 
38  bool parse(
39  std::istream &instream,
40  const std::string &path,
41  message_handlert &message_handler) override;
42 
44  symbol_table_baset &symbol_table,
45  message_handlert &message_handler) override;
46 
47  bool typecheck(
48  symbol_table_baset &symbol_table,
49  const std::string &module,
50  message_handlert &message_handler) override;
51 
53  symbol_table_baset &dest,
54  symbol_table_baset &src,
55  const std::string &module,
56  class replace_symbolt &replace_symbol) const;
57 
58  void show_parse(std::ostream &out, message_handlert &) override;
59 
60  // constructor, destructor
61  ~cpp_languaget() override;
63 
64  // conversion from expression into string
65  bool from_expr(
66  const exprt &expr,
67  std::string &code,
68  const namespacet &ns) override;
69 
70  // conversion from type into string
71  bool from_type(
72  const typet &type,
73  std::string &code,
74  const namespacet &ns) override;
75 
76  bool type_to_name(
77  const typet &type,
78  std::string &name,
79  const namespacet &ns) override;
80 
81  // conversion from string into expression
82  bool to_expr(
83  const std::string &code,
84  const std::string &module,
85  exprt &expr,
86  const namespacet &ns,
87  message_handlert &message_handler) override;
88 
89  std::unique_ptr<languaget> new_language() override
90  {
91  return std::make_unique<cpp_languaget>();
92  }
93 
94  std::string id() const override { return "cpp"; }
95  std::string description() const override { return "C++"; }
96  std::set<std::string> extensions() const override;
97 
98  void modules_provided(std::set<std::string> &modules) override;
99 
100 protected:
102  std::string parse_path;
103 
105 
106  void show_parse(std::ostream &out, const cpp_itemt &item);
107 
108  std::string main_symbol()
109  {
110  return "main";
111  }
112 };
113 
114 std::unique_ptr<languaget> new_cpp_language();
115 
116 #endif // CPROVER_CPP_CPP_LANGUAGE_H
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
bool parse(std::istream &instream, const std::string &path, message_handlert &message_handler) override
void set_language_options(const optionst &options, message_handlert &) override
Set language-specific options.
Definition: cpp_language.h:27
bool type_to_name(const typet &type, std::string &name, const namespacet &ns) override
Encodes the given type in a language-specific way.
std::string id() const override
Definition: cpp_language.h:94
c_object_factory_parameterst object_factory_params
Definition: cpp_language.h:104
std::unique_ptr< languaget > new_language() override
Definition: cpp_language.h:89
std::string parse_path
Definition: cpp_language.h:102
bool typecheck(symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler) override
bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream, message_handlert &message_handler) override
ANSI-C preprocessing.
std::string description() const override
Definition: cpp_language.h:95
bool merge_symbol_table(symbol_table_baset &dest, symbol_table_baset &src, const std::string &module, class replace_symbolt &replace_symbol) const
void show_parse(std::ostream &out, message_handlert &) override
bool generate_support_functions(symbol_table_baset &symbol_table, message_handlert &message_handler) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
std::set< std::string > extensions() const override
std::string main_symbol()
Definition: cpp_language.h:108
~cpp_languaget() override
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
void modules_provided(std::set< std::string > &modules) override
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns, message_handlert &message_handler) override
Parses the given string into an expression.
cpp_parse_treet cpp_parse_tree
Definition: cpp_language.h:101
Base class for all expressions.
Definition: expr.h:56
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
Replace a symbol expression by a given expression.
The symbol table base class interface.
The type of an expression, extends irept.
Definition: type.h:29
std::unique_ptr< languaget > new_cpp_language()
C++ Parser.
Abstract interface to support a programming language.
void set(const optionst &)
Assigns the parameters from given options.