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
std::unique_ptr< languaget > new_ansi_c_language()
bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
~ansi_c_languaget() override
std::set< std::string > extensions() const override
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
void show_parse(std::ostream &out) override
bool parse(std::istream &instream, const std::string &path) override
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
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::unique_ptr< languaget > new_language() override
bool generate_support_functions(symbol_tablet &symbol_table) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
std::string parse_path
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
void set_language_options(const optionst &options) override
Set language-specific options.
std::string description() const override
void modules_provided(std::set< std::string > &modules) override
bool type_to_name(const typet &type, std::string &name, const namespacet &ns) override
Encodes the given type in a language-specific way.
bool can_keep_file_local() override
Is it possible to call three-argument typecheck() on this object?
bool typecheck(symbol_tablet &symbol_table, const std::string &module) override
ansi_c_parse_treet parse_tree
c_object_factory_parameterst object_factory_params
std::string id() const 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
The symbol table.
Definition: symbol_table.h:14
The type of an expression, extends irept.
Definition: type.h:28
Abstract interface to support a programming language.
void set(const optionst &)
Assigns the parameters from given options.