cprover
jsil_parse_tree.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Jsil Language
4 
5 Author: 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 
20 static bool insert_at_label(
21  const codet &code,
22  const irep_idt &label,
23  code_blockt &dest)
24 {
25  Forall_operands(it, dest)
26  {
27  codet &c=to_code(*it);
28 
29  if(c.get_statement()!=ID_label)
30  continue;
31 
33  if(l.get_label()!=label)
34  continue;
35 
36  assert(l.code().get_statement()==ID_skip);
37  l.code()=code;
38 
39  return false;
40  }
41 
42  return true;
43 }
44 
46 {
47  symbol.clear();
48 
50  static_cast<const exprt&>(find(ID_declarator))));
51 
52  code_typet symbol_type=to_code_type(s.type());
53 
54  irep_idt proc_type=s.get("proc_type");
55 
56  if(proc_type=="builtin")
57  symbol_type=jsil_builtin_code_typet(symbol_type);
58  else if(proc_type=="spec")
59  symbol_type=jsil_spec_code_typet(symbol_type);
60 
61  symbol.name=s.get_identifier();
62  symbol.base_name=s.get_identifier();
63  symbol.mode="jsil";
64  symbol.type=symbol_type;
65  symbol.location=s.source_location();
66 
68  static_cast<const codet&>(find(ID_value))));
69 
70  irept returns(find(ID_return));
71  code_returnt r(symbol_exprt(returns.get(ID_value)));
72 
73  irept throws(find(ID_throw));
75  symbol_exprt(throws.get(ID_value)), nil_typet(), s.source_location());
76  code_expressiont ct(t);
77 
78  if(insert_at_label(r, returns.get(ID_label), code))
79  throw "return label "+returns.get_string(ID_label)+" not found";
80  if(insert_at_label(ct, throws.get(ID_label), code))
81  throw "throw label "+throws.get_string(ID_label)+" not found";
82 
83  symbol.value.swap(code);
84 }
85 
86 void jsil_declarationt::output(std::ostream &out) const
87 {
88  out << "Declarator: " << find(ID_declarator).pretty() << "\n";
89  out << "Returns: " << find(ID_return).pretty() << "\n";
90  out << "Throws: " << find(ID_throw).pretty() << "\n";
91  out << "Value: " << find(ID_value).pretty() << "\n";
92 }
93 
94 void jsil_parse_treet::output(std::ostream &out) const
95 {
96  for(itemst::const_iterator
97  it=items.begin();
98  it!=items.end();
99  it++)
100  {
101  it->output(out);
102  out << "\n";
103  }
104 }
const irep_idt & get_statement() const
Definition: std_code.h:40
irep_idt name
The unique identifier.
Definition: symbol.h:43
static int8_t r
Definition: irep_hash.h:59
Base type of functions.
Definition: std_types.h:764
Symbol table entry.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
irep_idt mode
Language mode.
Definition: symbol.h:52
void clear()
Definition: symbol.h:76
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:993
const irep_idt & get_identifier() const
Definition: std_expr.h:128
void to_symbol(symbolt &symbol) const
Jsil Language.
exprt value
Initial value of symbol.
Definition: symbol.h:37
typet & type()
Definition: expr.h:56
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
An expression statement.
Definition: std_code.h:1220
A side effect that throws an exception.
Definition: std_code.h:1491
codet & code()
Definition: std_code.h:1010
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
A label for branch targets.
Definition: std_code.h:977
Base class for tree-like data structures with sharing.
Definition: irep.h:156
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
void output(std::ostream &out) const
static bool insert_at_label(const codet &code, const irep_idt &label, code_blockt &dest)
Jsil Language.
typet type
Type of symbol.
Definition: symbol.h:34
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:40
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
const source_locationt & source_location() const
Definition: expr.h:125
The NIL type.
Definition: std_types.h:44
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:272
void swap(irept &irep)
Definition: irep.h:303
#define Forall_operands(it, expr)
Definition: expr.h:23
Sequential composition.
Definition: std_code.h:89
const codet & to_code(const exprt &expr)
Definition: std_code.h:75
const irep_idt & get_label() const
Definition: std_code.h:1000
Expression to hold a symbol (variable)
Definition: std_expr.h:90
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:165
A statement in a programming language.
Definition: std_code.h:21
Return from a function.
Definition: std_code.h:923
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1031
void output(std::ostream &) const
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285