cprover
Loading...
Searching...
No Matches
ansi_c_language.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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{
36public:
37 void set_language_options(const optionst &options) override
38 {
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
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
105protected:
107 std::string parse_path;
108
110};
111
112std::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()
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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.
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::unique_ptr< languaget > new_language() override
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.
The type of an expression, extends irept.
Definition type.h:29
Abstract interface to support a programming language.
void set(const optionst &)
Assigns the parameters from given options.