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 virtual bool preprocess(
27 std::istream &instream,
28 const std::string &path,
29 std::ostream &outstream) override;
30
31 virtual bool parse(
32 std::istream &instream,
33 const std::string &path) override;
34
35 virtual bool generate_support_functions(
36 symbol_tablet &symbol_table) override;
37
38 virtual bool typecheck(
39 symbol_tablet &context,
40 const std::string &module) override;
41
42 virtual void show_parse(std::ostream &out) override;
43
44 virtual ~jsil_languaget();
46
47 virtual bool from_expr(
48 const exprt &expr,
49 std::string &code,
50 const namespacet &ns) override;
51
52 virtual bool from_type(
53 const typet &type,
54 std::string &code,
55 const namespacet &ns) override;
56
57 virtual bool to_expr(
58 const std::string &code,
59 const std::string &module,
60 exprt &expr,
61 const namespacet &ns) override;
62
63 virtual std::unique_ptr<languaget> new_language() override
64 { return util_make_unique<jsil_languaget>(); }
65
66 virtual std::string id() const override { return "jsil"; }
67 virtual std::string description() const override
68 { return "Javascript Intermediate Language"; }
69 virtual std::set<std::string> extensions() const override;
70
71 virtual void modules_provided(std::set<std::string> &modules) override;
72 virtual bool interfaces(symbol_tablet &symbol_table) override;
73
74protected:
76 std::string parse_path;
77};
78
79std::unique_ptr<languaget> new_jsil_language();
80
81#endif // CPROVER_JSIL_JSIL_LANGUAGE_H
Base class for all expressions.
Definition: expr.h:54
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
jsil_parse_treet parse_tree
Definition: jsil_language.h:75
virtual 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
Definition: jsil_language.h:76
virtual bool parse(std::istream &instream, const std::string &path) override
virtual ~jsil_languaget()
virtual bool generate_support_functions(symbol_tablet &symbol_table) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
virtual bool typecheck(symbol_tablet &context, const std::string &module) override
Converting from parse tree and type checking.
virtual std::string description() const override
Definition: jsil_language.h:67
virtual bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
Parses the given string into an expression.
virtual std::set< std::string > extensions() const override
virtual bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
virtual void show_parse(std::ostream &out) override
virtual void modules_provided(std::set< std::string > &modules) override
virtual bool interfaces(symbol_tablet &symbol_table) override
Adding symbols for all procedure declarations.
virtual std::string id() const override
Definition: jsil_language.h:66
virtual std::unique_ptr< languaget > new_language() override
Definition: jsil_language.h:63
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:29
std::unique_ptr< languaget > new_jsil_language()
Jsil Language.
Abstract interface to support a programming language.