cprover
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 <util/make_unique.h> // unique_ptr
20 
21 #include <langapi/language.h>
22 
23 #include "cpp_parse_tree.h"
24 
26 {
27 public:
28  void set_language_options(const optionst &options) override
29  {
30  object_factory_params.set(options);
31  }
32 
33  bool preprocess(
34  std::istream &instream,
35  const std::string &path,
36  std::ostream &outstream) override;
37 
38  bool parse(
39  std::istream &instream,
40  const std::string &path) override;
41 
43  symbol_tablet &symbol_table) override;
44 
45  bool typecheck(
46  symbol_tablet &symbol_table,
47  const std::string &module) override;
48 
49  bool merge_symbol_table(
50  symbol_tablet &dest,
51  symbol_tablet &src,
52  const std::string &module,
53  class replace_symbolt &replace_symbol) const;
54 
55  void show_parse(std::ostream &out) override;
56 
57  // constructor, destructor
58  ~cpp_languaget() override;
60 
61  // conversion from expression into string
62  bool from_expr(
63  const exprt &expr,
64  std::string &code,
65  const namespacet &ns) override;
66 
67  // conversion from type into string
68  bool from_type(
69  const typet &type,
70  std::string &code,
71  const namespacet &ns) override;
72 
73  bool type_to_name(
74  const typet &type,
75  std::string &name,
76  const namespacet &ns) override;
77 
78  // conversion from string into expression
79  bool to_expr(
80  const std::string &code,
81  const std::string &module,
82  exprt &expr,
83  const namespacet &ns) override;
84 
85  std::unique_ptr<languaget> new_language() override
86  { return util_make_unique<cpp_languaget>(); }
87 
88  std::string id() const override { return "cpp"; }
89  std::string description() const override { return "C++"; }
90  std::set<std::string> extensions() const override;
91 
92  void modules_provided(std::set<std::string> &modules) override;
93 
94 protected:
96  std::string parse_path;
97 
99 
100  void show_parse(std::ostream &out, const cpp_itemt &item);
101 
102  std::string main_symbol()
103  {
104  return "main";
105  }
106 };
107 
108 std::unique_ptr<languaget> new_cpp_language();
109 
110 #endif // CPROVER_CPP_CPP_LANGUAGE_H
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
cpp_languaget::new_language
std::unique_ptr< languaget > new_language() override
Definition: cpp_language.h:85
cpp_parse_treet
Definition: cpp_parse_tree.h:19
optionst
Definition: options.h:22
cpp_languaget::generate_support_functions
bool generate_support_functions(symbol_tablet &symbol_table) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
Definition: cpp_language.cpp:137
typet
The type of an expression, extends irept.
Definition: type.h:27
cpp_languaget::main_symbol
std::string main_symbol()
Definition: cpp_language.h:102
cpp_languaget::show_parse
void show_parse(std::ostream &out) override
Definition: cpp_language.cpp:144
cpp_languaget::set_language_options
void set_language_options(const optionst &options) override
Set language-specific options.
Definition: cpp_language.h:28
cpp_languaget::preprocess
bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
Definition: cpp_language.cpp:57
exprt
Base class for all expressions.
Definition: expr.h:54
cpp_languaget::cpp_languaget
cpp_languaget()
Definition: cpp_language.h:59
cpp_languaget::to_expr
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
Parses the given string into an expression.
Definition: cpp_language.cpp:229
cpp_languaget::description
std::string description() const override
Definition: cpp_language.h:89
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
make_unique.h
c_object_factory_parameters.h
c_object_factory_parameterst
Definition: c_object_factory_parameters.h:14
cpp_languaget::modules_provided
void modules_provided(std::set< std::string > &modules) override
Definition: cpp_language.cpp:51
language.h
new_cpp_language
std::unique_ptr< languaget > new_cpp_language()
Definition: cpp_language.cpp:197
cpp_languaget::from_type
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
Definition: cpp_language.cpp:211
cpp_languaget::typecheck
bool typecheck(symbol_tablet &symbol_table, const std::string &module) override
Definition: cpp_language.cpp:121
cpp_parse_tree.h
object_factory_parameterst::set
void set(const optionst &)
Assigns the parameters from given options.
Definition: object_factory_parameters.cpp:14
cpp_languaget::id
std::string id() const override
Definition: cpp_language.h:88
cpp_languaget::parse
bool parse(std::istream &instream, const std::string &path) override
Definition: cpp_language.cpp:83
cpp_languaget::cpp_parse_tree
cpp_parse_treet cpp_parse_tree
Definition: cpp_language.h:95
cpp_languaget::type_to_name
bool type_to_name(const typet &type, std::string &name, const namespacet &ns) override
Encodes the given type in a language-specific way.
Definition: cpp_language.cpp:220
cpp_languaget::parse_path
std::string parse_path
Definition: cpp_language.h:96
cpp_languaget
Definition: cpp_language.h:25
cpp_languaget::merge_symbol_table
bool merge_symbol_table(symbol_tablet &dest, symbol_tablet &src, const std::string &module, class replace_symbolt &replace_symbol) const
languaget
Definition: language.h:39
cpp_languaget::object_factory_params
c_object_factory_parameterst object_factory_params
Definition: cpp_language.h:98
cpp_languaget::from_expr
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
Definition: cpp_language.cpp:202
cpp_languaget::extensions
std::set< std::string > extensions() const override
Definition: cpp_language.cpp:33
cpp_itemt
Definition: cpp_item.h:23
replace_symbolt
Replace expression or type symbols by an expression or type, respectively.
Definition: replace_symbol.h:24
cpp_languaget::~cpp_languaget
~cpp_languaget() override
Definition: cpp_language.cpp:267