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"
21 
22 // clang-format off
23 #define OPT_ANSI_C_LANGUAGE \
24  "(max-nondet-tree-depth):" \
25  "(min-null-tree-depth):"
26 
27 #define HELP_ANSI_C_LANGUAGE \
28  " --max-nondet-tree-depth N limit size of nondet (e.g. input) object tree;\n" /* NOLINT(*) */\
29  " at level N pointers are set to null\n" \
30  " --min-null-tree-depth N minimum level at which a pointer can first be\n" /* NOLINT(*) */\
31  " NULL in a recursively nondet initialized struct\n" /* NOLINT(*) */
32 // clang-format on
33 
35 {
36 public:
37  void set_language_options(const optionst &options) override
38  {
39  object_factory_params.set(options);
40  }
41 
42  bool preprocess(
43  std::istream &instream,
44  const std::string &path,
45  std::ostream &outstream) override;
46 
47  bool parse(
48  std::istream &instream,
49  const std::string &path) override;
50 
52  symbol_tablet &symbol_table) override;
53 
54  bool typecheck(
55  symbol_tablet &symbol_table,
56  const std::string &module) override;
57 
58  void show_parse(std::ostream &out) override;
59 
60  ~ansi_c_languaget() override;
62 
63  bool from_expr(
64  const exprt &expr,
65  std::string &code,
66  const namespacet &ns) override;
67 
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  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
85  { return util_make_unique<ansi_c_languaget>(); }
86 
87  std::string id() const override { return "C"; }
88  std::string description() const override { return "ANSI-C 99"; }
89  std::set<std::string> extensions() const override;
90 
91  void modules_provided(std::set<std::string> &modules) override;
92 
93 protected:
95  std::string parse_path;
96 
98 };
99 
100 std::unique_ptr<languaget> new_ansi_c_language();
101 
102 #endif // CPROVER_ANSI_C_ANSI_C_LANGUAGE_H
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
ansi_c_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: ansi_c_language.cpp:165
optionst
Definition: options.h:22
typet
The type of an expression, extends irept.
Definition: type.h:27
ansi_c_parse_tree.h
ansi_c_languaget::~ansi_c_languaget
~ansi_c_languaget() override
Definition: ansi_c_language.cpp:221
ansi_c_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: ansi_c_language.cpp:174
exprt
Base class for all expressions.
Definition: expr.h:54
ansi_c_languaget::id
std::string id() const override
Definition: ansi_c_language.h:87
ansi_c_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: ansi_c_language.cpp:156
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
language.h
ansi_c_parse_treet
Definition: ansi_c_parse_tree.h:17
ansi_c_languaget::preprocess
bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
Definition: ansi_c_language.cpp:40
ansi_c_languaget::object_factory_params
c_object_factory_parameterst object_factory_params
Definition: ansi_c_language.h:97
object_factory_parameterst::set
void set(const optionst &)
Assigns the parameters from given options.
Definition: object_factory_parameters.cpp:14
ansi_c_languaget::parse_tree
ansi_c_parse_treet parse_tree
Definition: ansi_c_language.h:94
ansi_c_languaget::new_language
std::unique_ptr< languaget > new_language() override
Definition: ansi_c_language.h:84
ansi_c_languaget::show_parse
void show_parse(std::ostream &out) override
Definition: ansi_c_language.cpp:137
new_ansi_c_language
std::unique_ptr< languaget > new_ansi_c_language()
Definition: ansi_c_language.cpp:142
ansi_c_languaget::parse
bool parse(std::istream &instream, const std::string &path) override
Definition: ansi_c_language.cpp:52
ansi_c_languaget::extensions
std::set< std::string > extensions() const override
Definition: ansi_c_language.cpp:29
ansi_c_languaget::modules_provided
void modules_provided(std::set< std::string > &modules) override
Definition: ansi_c_language.cpp:34
languaget
Definition: language.h:39
ansi_c_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: ansi_c_language.cpp:129
ansi_c_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: ansi_c_language.cpp:147
ansi_c_languaget::description
std::string description() const override
Definition: ansi_c_language.h:88
ansi_c_languaget::parse_path
std::string parse_path
Definition: ansi_c_language.h:95
ansi_c_languaget
Definition: ansi_c_language.h:34
ansi_c_languaget::typecheck
bool typecheck(symbol_tablet &symbol_table, const std::string &module) override
Definition: ansi_c_language.cpp:106
ansi_c_languaget::ansi_c_languaget
ansi_c_languaget()
Definition: ansi_c_language.h:61
ansi_c_languaget::set_language_options
void set_language_options(const optionst &options) override
Set language-specific options.
Definition: ansi_c_language.h:37