cprover
ansi_c_language.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_ANSI_C_ANSI_C_LANGUAGE_H
11 #define CPROVER_ANSI_C_ANSI_C_LANGUAGE_H
12 
13 #include <memory>
14 
15 #include <util/make_unique.h>
16 
17 #include <langapi/language.h>
18 
19 #include "ansi_c_parse_tree.h"
20 
22 {
23 public:
24  bool preprocess(
25  std::istream &instream,
26  const std::string &path,
27  std::ostream &outstream) override;
28 
29  bool parse(
30  std::istream &instream,
31  const std::string &path) override;
32 
34  symbol_tablet &symbol_table) override;
35 
36  bool typecheck(
37  symbol_tablet &symbol_table,
38  const std::string &module) override;
39 
40  void show_parse(std::ostream &out) override;
41 
42  ~ansi_c_languaget() override;
44 
45  bool from_expr(
46  const exprt &expr,
47  std::string &code,
48  const namespacet &ns) override;
49 
50  bool from_type(
51  const typet &type,
52  std::string &code,
53  const namespacet &ns) override;
54 
55  bool type_to_name(
56  const typet &type,
57  std::string &name,
58  const namespacet &ns) override;
59 
60  bool to_expr(
61  const std::string &code,
62  const std::string &module,
63  exprt &expr,
64  const namespacet &ns) override;
65 
66  std::unique_ptr<languaget> new_language() override
67  { return util_make_unique<ansi_c_languaget>(); }
68 
69  std::string id() const override { return "C"; }
70  std::string description() const override { return "ANSI-C 99"; }
71  std::set<std::string> extensions() const override;
72 
73  void modules_provided(std::set<std::string> &modules) override;
74 
75 protected:
77  std::string parse_path;
78 };
79 
80 std::unique_ptr<languaget> new_ansi_c_language();
81 
82 #endif // CPROVER_ANSI_C_ANSI_C_LANGUAGE_H
The type of an expression.
Definition: type.h:22
~ansi_c_languaget() override
std::string parse_path
bool typecheck(symbol_tablet &symbol_table, const std::string &module) override
ansi_c_parse_treet parse_tree
std::unique_ptr< languaget > new_language() override
bool parse(std::istream &instream, const std::string &path) override
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 description() const override
bool generate_support_functions(symbol_tablet &symbol_table) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
The symbol table.
Definition: symbol_table.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
Abstract interface to support a programming language.
bool type_to_name(const typet &type, std::string &name, const namespacet &ns) override
Encodes the given type in a language-specific way.
void show_parse(std::ostream &out) override
Base class for all expressions.
Definition: expr.h:42
std::string id() const override
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
std::set< std::string > extensions() const override
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
std::unique_ptr< languaget > new_ansi_c_language()
void modules_provided(std::set< std::string > &modules) override