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 " {y--max-nondet-tree-depth} {uN} \t " \
29 "limit size of nondet (e.g. input) object tree; at level {uN} pointers are " \
30 "set to null\n" \
31 " {y--min-null-tree-depth} {uN} \t " \
32 "minimum level at which a pointer can first be NULL in a recursively " \
33 "nondet initialized struct\n" \
34// clang-format on
35
37{
38public:
39 void set_language_options(const optionst &options) override
40 {
42 }
43
44 bool preprocess(
45 std::istream &instream,
46 const std::string &path,
47 std::ostream &outstream) override;
48
49 bool parse(
50 std::istream &instream,
51 const std::string &path) override;
52
53 bool generate_support_functions(symbol_table_baset &symbol_table) override;
54
55 bool typecheck(
56 symbol_table_baset &symbol_table,
57 const std::string &module,
58 const bool keep_file_local) override;
59
60 bool typecheck(
61 symbol_table_baset &symbol_table,
62 const std::string &module,
63 const bool keep_file_local,
64 const std::set<irep_idt> &keep);
65
66 bool can_keep_file_local() override
67 {
68 return true;
69 }
70
71 bool typecheck(symbol_table_baset &symbol_table, const std::string &module)
72 override
73 {
74 return typecheck(symbol_table, module, true);
75 }
76
77 void show_parse(std::ostream &out) override;
78
79 ~ansi_c_languaget() override;
81
82 bool from_expr(
83 const exprt &expr,
84 std::string &code,
85 const namespacet &ns) override;
86
87 bool from_type(
88 const typet &type,
89 std::string &code,
90 const namespacet &ns) override;
91
92 bool type_to_name(
93 const typet &type,
94 std::string &name,
95 const namespacet &ns) override;
96
97 bool to_expr(
98 const std::string &code,
99 const std::string &module,
100 exprt &expr,
101 const namespacet &ns) override;
102
103 std::unique_ptr<languaget> new_language() override
105
106 std::string id() const override { return "C"; }
107 std::string description() const override { return "ANSI-C 99"; }
108 std::set<std::string> extensions() const override;
109
110 void modules_provided(std::set<std::string> &modules) override;
111
112protected:
114 std::string parse_path;
115
117};
118
119std::unique_ptr<languaget> new_ansi_c_language();
120
121#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
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 typecheck(symbol_table_baset &symbol_table, const std::string &module, const bool keep_file_local) override
typecheck without removing specified entries from the symbol table
std::string parse_path
bool typecheck(symbol_table_baset &symbol_table, const std::string &module) override
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?
ansi_c_parse_treet parse_tree
c_object_factory_parameterst object_factory_params
std::unique_ptr< languaget > new_language() override
bool generate_support_functions(symbol_table_baset &symbol_table) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
std::string id() const override
Base class for all expressions.
Definition expr.h:56
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 base class interface.
The type of an expression, extends irept.
Definition type.h:29
Abstract interface to support a programming language.
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition make_unique.h:19
void set(const optionst &)
Assigns the parameters from given options.