CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
cpp_language.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: C++ Language Module
4
5Author: 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{
25public:
26 void
28 {
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
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
100protected:
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
114std::unique_ptr<languaget> new_cpp_language();
115
116#endif // CPROVER_CPP_CPP_LANGUAGE_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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.
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
c_object_factory_parameterst object_factory_params
std::string parse_path
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
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::unique_ptr< languaget > new_language() override
std::string main_symbol()
~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
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:91
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.