cprover
Loading...
Searching...
No Matches
jsil_parse_tree.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Jsil Language
4
5Author: Michael Tautschnig, tautschn@amazon.com
6
7\*******************************************************************/
8
11
12#include "jsil_parse_tree.h"
13
14#include <ostream>
15
16#include <util/symbol.h>
17
18#include "jsil_types.h"
19
20static bool insert_at_label(
21 const codet &code,
22 const irep_idt &label,
23 code_blockt &dest)
24{
25 for(auto &c : dest.statements())
26 {
27 if(c.get_statement()!=ID_label)
28 continue;
29
31 if(l.get_label()!=label)
32 continue;
33
34 DATA_INVARIANT(l.code().get_statement() == ID_skip, "code should be skip");
35 l.code()=code;
36
37 return false;
38 }
39
40 return true;
41}
42
44{
46 static_cast<const exprt&>(find(ID_declarator))));
47
49
50 irep_idt proc_type=s.get("proc_type");
51
52 if(proc_type=="builtin")
54 else if(proc_type=="spec")
56
57 symbolt symbol{s.get_identifier(), symbol_type, "jsil"};
58 symbol.base_name=s.get_identifier();
59 symbol.location=s.source_location();
60
62 static_cast<const codet&>(find(ID_value))));
63
66
67 irept throws(find(ID_throw));
71
72 if(insert_at_label(r, returns.get(ID_label), code))
73 throw "return label "+returns.get_string(ID_label)+" not found";
74 if(insert_at_label(ct, throws.get(ID_label), code))
75 throw "throw label "+throws.get_string(ID_label)+" not found";
76
77 symbol.value.swap(code);
78
79 return symbol;
80}
81
82void jsil_declarationt::output(std::ostream &out) const
83{
84 out << "Declarator: " << find(ID_declarator).pretty() << "\n";
85 out << "Returns: " << find(ID_return).pretty() << "\n";
86 out << "Throws: " << find(ID_throw).pretty() << "\n";
87 out << "Value: " << find(ID_value).pretty() << "\n";
88}
89
90void jsil_parse_treet::output(std::ostream &out) const
91{
92 for(itemst::const_iterator
93 it=items.begin();
94 it!=items.end();
95 it++)
96 {
97 it->output(out);
98 out << "\n";
99 }
100}
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
Definition ai.cpp:39
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
A codet representing sequential composition of program statements.
Definition std_code.h:130
code_operandst & statements()
Definition std_code.h:138
codet representation of an expression statement.
Definition std_code.h:1394
codet representation of a "return from a function" statement.
Definition std_code.h:893
codet representation of a label for branch targets.
Definition std_code.h:959
const irep_idt & get_label() const
Definition std_code.h:967
codet & code()
Definition std_code.h:977
Base type of functions.
Definition std_types.h:539
Data structure for representing an arbitrary statement in a program.
const irep_idt & get_statement() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
const source_locationt & source_location() const
Definition expr.h:223
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:372
const irept & find(const irep_idt &name) const
Definition irep.cpp:101
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
void output(std::ostream &) const
symbolt to_symbol() const
void output(std::ostream &out) const
A side_effect_exprt representation of a side effect that throws an exception.
Definition std_code.h:1757
Expression to hold a symbol (variable)
Definition std_expr.h:113
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition std_expr.h:132
const irep_idt & get_identifier() const
Definition std_expr.h:142
Symbol table entry.
Definition symbol.h:28
The type of an expression, extends irept.
Definition type.h:29
static int8_t r
Definition irep_hash.h:60
static bool insert_at_label(const codet &code, const irep_idt &label, code_blockt &dest)
Jsil Language.
Jsil Language.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
const code_labelt & to_code_label(const codet &code)
Definition std_code.h:1004
const code_blockt & to_code_block(const codet &code)
Definition std_code.h:203
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
Symbol table entry.