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,
57  const bool keep_file_local) override;
58 
59  bool can_keep_file_local() override
60  {
61  return true;
62  }
63 
64  bool
65  typecheck(symbol_tablet &symbol_table, const std::string &module) override
66  {
67  return typecheck(symbol_table, module, true);
68  }
69 
70  void show_parse(std::ostream &out) override;
71 
72  ~ansi_c_languaget() override;
74 
75  bool from_expr(
76  const exprt &expr,
77  std::string &code,
78  const namespacet &ns) override;
79 
80  bool from_type(
81  const typet &type,
82  std::string &code,
83  const namespacet &ns) override;
84 
85  bool type_to_name(
86  const typet &type,
87  std::string &name,
88  const namespacet &ns) override;
89 
90  bool to_expr(
91  const std::string &code,
92  const std::string &module,
93  exprt &expr,
94  const namespacet &ns) override;
95 
96  std::unique_ptr<languaget> new_language() override
97  { return util_make_unique<ansi_c_languaget>(); }
98 
99  std::string id() const override { return "C"; }
100  std::string description() const override { return "ANSI-C 99"; }
101  std::set<std::string> extensions() const override;
102 
103  void modules_provided(std::set<std::string> &modules) override;
104 
105 protected:
107  std::string parse_path;
108 
110 };
111 
112 std::unique_ptr<languaget> new_ansi_c_language();
113 
114 #endif // CPROVER_ANSI_C_ANSI_C_LANGUAGE_H
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
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:166
optionst
Definition: options.h:23
typet
The type of an expression, extends irept.
Definition: type.h:29
ansi_c_parse_tree.h
ansi_c_languaget::~ansi_c_languaget
~ansi_c_languaget() override
Definition: ansi_c_language.cpp:224
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:175
exprt
Base class for all expressions.
Definition: expr.h:53
ansi_c_languaget::id
std::string id() const override
Definition: ansi_c_language.h:99
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:157
ansi_c_languaget::can_keep_file_local
bool can_keep_file_local() override
Is it possible to call three-argument typecheck() on this object?
Definition: ansi_c_language.h:59
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
make_unique.h
c_object_factory_parameters.h
c_object_factory_parameterst
Definition: c_object_factory_parameters.h:15
language.h
Abstract interface to support a programming language.
ansi_c_parse_treet
Definition: ansi_c_parse_tree.h:18
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:109
object_factory_parameterst::set
void set(const optionst &)
Assigns the parameters from given options.
Definition: object_factory_parameters.cpp:15
ansi_c_languaget::parse_tree
ansi_c_parse_treet parse_tree
Definition: ansi_c_language.h:106
ansi_c_languaget::new_language
std::unique_ptr< languaget > new_language() override
Definition: ansi_c_language.h:96
ansi_c_languaget::show_parse
void show_parse(std::ostream &out) override
Definition: ansi_c_language.cpp:138
new_ansi_c_language
std::unique_ptr< languaget > new_ansi_c_language()
Definition: ansi_c_language.cpp:143
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:40
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:130
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:148
ansi_c_languaget::description
std::string description() const override
Definition: ansi_c_language.h:100
ansi_c_languaget::typecheck
bool typecheck(symbol_tablet &symbol_table, const std::string &module, const bool keep_file_local) override
typecheck without removing specified entries from the symbol table
Definition: ansi_c_language.cpp:105
ansi_c_languaget::parse_path
std::string parse_path
Definition: ansi_c_language.h:107
ansi_c_languaget
Definition: ansi_c_language.h:35
ansi_c_languaget::typecheck
bool typecheck(symbol_tablet &symbol_table, const std::string &module) override
Definition: ansi_c_language.h:65
ansi_c_languaget::ansi_c_languaget
ansi_c_languaget()
Definition: ansi_c_language.h:73
ansi_c_languaget::set_language_options
void set_language_options(const optionst &options) override
Set language-specific options.
Definition: ansi_c_language.h:37