cprover
Loading...
Searching...
No Matches
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 <util/make_unique.h> // unique_ptr
20
21#include <langapi/language.h>
22
23#include "cpp_parse_tree.h"
24
26{
27public:
28 void set_language_options(const optionst &options) override
29 {
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
46 typecheck(symbol_tablet &symbol_table, const std::string &module) override;
47
50 symbol_tablet &src,
51 const std::string &module,
52 class replace_symbolt &replace_symbol) const;
53
54 void show_parse(std::ostream &out) override;
55
56 // constructor, destructor
57 ~cpp_languaget() override;
59
60 // conversion from expression into string
61 bool from_expr(
62 const exprt &expr,
63 std::string &code,
64 const namespacet &ns) override;
65
66 // conversion from type into string
67 bool from_type(
68 const typet &type,
69 std::string &code,
70 const namespacet &ns) override;
71
72 bool type_to_name(
73 const typet &type,
74 std::string &name,
75 const namespacet &ns) override;
76
77 // conversion from string into expression
78 bool to_expr(
79 const std::string &code,
80 const std::string &module,
81 exprt &expr,
82 const namespacet &ns) override;
83
84 std::unique_ptr<languaget> new_language() override
86
87 std::string id() const override { return "cpp"; }
88 std::string description() const override { return "C++"; }
89 std::set<std::string> extensions() const override;
90
91 void modules_provided(std::set<std::string> &modules) override;
92
93protected:
95 std::string parse_path;
96
98
99 void show_parse(std::ostream &out, const cpp_itemt &item);
100
101 std::string main_symbol()
102 {
103 return "main";
104 }
105};
106
107std::unique_ptr<languaget> new_cpp_language();
108
109#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:564
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
void set_language_options(const optionst &options) 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
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
Parses the given string into an expression.
std::string parse_path
std::string description() const override
std::set< std::string > extensions() const override
std::unique_ptr< languaget > new_language() override
std::string main_symbol()
~cpp_languaget() override
bool merge_symbol_table(symbol_tablet &dest, symbol_tablet &src, const std::string &module, class replace_symbolt &replace_symbol) const
bool generate_support_functions(symbol_tablet &symbol_table) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
bool parse(std::istream &instream, const std::string &path) override
void modules_provided(std::set< std::string > &modules) override
bool typecheck(symbol_tablet &symbol_table, const std::string &module) override
cpp_parse_treet cpp_parse_tree
void show_parse(std::ostream &out) override
Base class for all expressions.
Definition expr.h:54
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Replace expression or type symbols by an expression or type, respectively.
The symbol table.
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.