cprover
Loading...
Searching...
No Matches
jsil_language.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Jsil Language
4
5Author: Michael Tautschnig, tautschn@amazon.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_JSIL_JSIL_LANGUAGE_H
13#define CPROVER_JSIL_JSIL_LANGUAGE_H
14
15#include <memory>
16
17#include <util/make_unique.h>
18
19#include <langapi/language.h>
20
21#include "jsil_parse_tree.h"
22
24{
25public:
26 bool preprocess(
27 std::istream &instream,
28 const std::string &path,
29 std::ostream &outstream) override;
30
31 bool parse(std::istream &instream, const std::string &path) override;
32
33 bool generate_support_functions(symbol_table_baset &symbol_table) override;
34
35 bool
36 typecheck(symbol_table_baset &context, const std::string &module) override;
37
38 void show_parse(std::ostream &out) override;
39
40 virtual ~jsil_languaget();
42
43 bool from_expr(const exprt &expr, std::string &code, const namespacet &ns)
44 override;
45
46 bool from_type(const typet &type, std::string &code, const namespacet &ns)
47 override;
48
49 bool to_expr(
50 const std::string &code,
51 const std::string &module,
52 exprt &expr,
53 const namespacet &ns) override;
54
55 std::unique_ptr<languaget> new_language() override
57
58 std::string id() const override
59 {
60 return "jsil";
61 }
62 std::string description() const override
63 { return "Javascript Intermediate Language"; }
64 std::set<std::string> extensions() const override;
65
66 void modules_provided(std::set<std::string> &modules) override;
67 bool interfaces(symbol_table_baset &symbol_table) override;
68
69protected:
71 std::string parse_path;
72};
73
74std::unique_ptr<languaget> new_jsil_language();
75
76#endif // CPROVER_JSIL_JSIL_LANGUAGE_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Base class for all expressions.
Definition expr.h:56
bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
jsil_parse_treet parse_tree
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
std::string parse_path
std::unique_ptr< languaget > new_language() override
bool parse(std::istream &instream, const std::string &path) override
virtual ~jsil_languaget()
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::set< std::string > extensions() const override
std::string id() const override
bool typecheck(symbol_table_baset &context, const std::string &module) override
Converting from parse tree and type checking.
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
bool generate_support_functions(symbol_table_baset &symbol_table) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
bool interfaces(symbol_table_baset &symbol_table) override
Adding symbols for all procedure declarations.
void show_parse(std::ostream &out) override
void modules_provided(std::set< std::string > &modules) override
std::string description() const override
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
std::unique_ptr< languaget > new_jsil_language()
Jsil Language.
Abstract interface to support a programming language.