cprover
Loading...
Searching...
No Matches
jsil_typecheck.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_typecheck.h"
13
15
17#include <util/prefix.h>
18#include <util/std_code.h>
19#include <util/symbol_table.h>
20
21#include "expr2jsil.h"
22#include "jsil_types.h"
23
24std::string jsil_typecheckt::to_string(const exprt &expr)
25{
26 return expr2jsil(expr, ns);
27}
28
29std::string jsil_typecheckt::to_string(const typet &type)
30{
31 return type2jsil(type, ns);
32}
33
36{
37 return id2string(proc_name) + "::" + id2string(ds);
38}
39
41{
42 expr.type()=type;
43
44 if(expr.id()==ID_symbol)
45 {
46 const irep_idt &id=to_symbol_expr(expr).get_identifier();
47
48 const auto maybe_symbol=symbol_table.get_writeable(id);
49 if(!maybe_symbol)
50 {
51 error() << "unexpected symbol: " << id << eom;
52 throw 0;
53 }
54
55 symbolt &s=*maybe_symbol;
56 if(s.type.id().empty() || s.type.is_nil())
57 s.type=type;
58 else
59 s.type=jsil_union(s.type, type);
60 }
61}
62
64 exprt &expr,
65 const typet &type,
66 bool must)
67{
68 if(type.id().empty() || type.is_nil())
69 {
71 error() << "make_type_compatible got empty type: " << expr.pretty() << eom;
72 throw 0;
73 }
74
75 if(expr.type().id().empty() || expr.type().is_nil())
76 {
77 // Type is not yet set
78 update_expr_type(expr, type);
79 return;
80 }
81
82 if(must)
83 {
84 if(jsil_incompatible_types(expr.type(), type))
85 {
87 error() << "failed to typecheck expr "
88 << expr.pretty() << " with type "
89 << expr.type().pretty()
90 << "; required type " << type.pretty() << eom;
91 throw 0;
92 }
93 }
94 else if(!jsil_is_subtype(type, expr.type()))
95 {
96 // Types are not compatible
97 typet upper=jsil_union(expr.type(), type);
98 update_expr_type(expr, upper);
99 }
100}
101
103{
104 if(type.id()==ID_code)
105 {
106 code_typet &parameters=to_code_type(type);
107
108 for(code_typet::parametert &p : parameters.parameters())
109 {
110 // create new symbol
111 parameter_symbolt new_symbol;
112 new_symbol.base_name=p.get_identifier();
113
114 // append procedure name to parameters
115 p.set_identifier(add_prefix(p.get_identifier()));
116 new_symbol.name=p.get_identifier();
117
119 new_symbol.type=jsil_value_or_empty_type();
120 else if(is_jsil_spec_code_type(type))
122 else
123 new_symbol.type=jsil_value_type(); // User defined function
124
125 new_symbol.mode="jsil";
126
127 // mark as already typechecked
128 new_symbol.is_extern=true;
129
130 if(symbol_table.add(new_symbol))
131 {
132 error() << "failed to add parameter symbol '" << new_symbol.name
133 << "' in the symbol table" << eom;
134 throw 0;
135 }
136 }
137 }
138}
139
141{
142 // first do sub-nodes
144
145 // now do case-split
147}
148
150{
151 Forall_operands(it, expr)
152 typecheck_expr(*it);
153}
154
156{
157 if(expr.id()==ID_code)
158 {
160 error() << "typecheck_expr_main got code: " << expr.pretty() << eom;
161 throw 0;
162 }
163 else if(expr.id()==ID_symbol)
165 else if(expr.id()==ID_constant)
166 {
167 }
168 else
169 {
170 // expressions are expected not to have type set just yet
171 assert(expr.type().is_nil() || expr.type().id().empty());
172
173 if(expr.id()==ID_null ||
174 expr.id()=="undefined" ||
175 expr.id()==ID_empty)
177 else if(expr.id()=="null_type" ||
178 expr.id()=="undefined_type" ||
179 expr.id()==ID_boolean ||
180 expr.id()==ID_string ||
181 expr.id()=="number" ||
182 expr.id()=="builtin_object" ||
183 expr.id()=="user_object" ||
184 expr.id()=="object" ||
185 expr.id()==ID_pointer ||
186 expr.id()==ID_member ||
187 expr.id()=="variable")
188 expr.type()=jsil_kind();
189 else if(expr.id()=="proto" ||
190 expr.id()=="fid" ||
191 expr.id()=="scope" ||
192 expr.id()=="constructid" ||
193 expr.id()=="primvalue" ||
194 expr.id()=="targetfunction" ||
195 expr.id()==ID_class)
196 {
197 // TODO: have a special type for builtin fields
198 expr.type()=string_typet();
199 }
200 else if(expr.id()==ID_not)
202 else if(expr.id()=="string_to_num")
204 else if(expr.id()==ID_unary_minus ||
205 expr.id()=="num_to_int32" ||
206 expr.id()=="num_to_uint32" ||
207 expr.id()==ID_bitnot)
208 {
210 expr.type()=floatbv_typet();
211 }
212 else if(expr.id()=="num_to_string")
213 {
215 expr.type()=string_typet();
216 }
217 else if(expr.id()==ID_equal)
219 else if(expr.id()==ID_lt ||
220 expr.id()==ID_le)
222 else if(expr.id()==ID_plus ||
223 expr.id()==ID_minus ||
224 expr.id()==ID_mult ||
225 expr.id()==ID_div ||
226 expr.id()==ID_mod ||
227 expr.id()==ID_bitand ||
228 expr.id()==ID_bitor ||
229 expr.id()==ID_bitxor ||
230 expr.id()==ID_shl ||
231 expr.id()==ID_shr ||
232 expr.id()==ID_lshr)
234 else if(expr.id()==ID_and ||
235 expr.id()==ID_or)
237 else if(expr.id()=="subtype_of")
239 else if(expr.id()==ID_concatenation)
241 else if(expr.id()=="ref")
242 typecheck_expr_ref(expr);
243 else if(expr.id()=="field")
245 else if(expr.id()==ID_base)
247 else if(expr.id()==ID_typeof)
248 expr.type()=jsil_kind();
249 else if(expr.id()=="new")
251 else if(expr.id()=="hasField")
253 else if(expr.id()==ID_index)
255 else if(expr.id()=="delete")
257 else if(expr.id()=="protoField")
259 else if(expr.id()=="protoObj")
261 else if(expr.id()==ID_side_effect)
263 else
264 {
266 error() << "unexpected expression: " << expr.pretty() << eom;
267 throw 0;
268 }
269 }
270}
271
274{
275 irept &excep_list=expr.add(ID_exception_list);
276 assert(excep_list.id()==ID_symbol);
277 symbol_exprt &s=static_cast<symbol_exprt &>(excep_list);
279}
280
282{
283 if(expr.id()==ID_null)
284 expr.type()=jsil_null_type();
285 else if(expr.id()=="undefined")
286 expr.type()=jsil_undefined_type();
287 else if(expr.id()==ID_empty)
288 expr.type()=jsil_empty_type();
289}
290
292{
293 if(expr.operands().size()!=2)
294 {
296 error() << "operator '" << expr.id() << "' expects two operands" << eom;
297 throw 0;
298 }
299
302
304}
305
307{
308 if(expr.operands().size()!=2)
309 {
311 error() << "operator '" << expr.id() << "' expects two operands";
312 throw 0;
313 }
314
317
318 expr.type()=bool_typet();
319}
320
322{
323 if(expr.operands().size()!=2)
324 {
326 error() << "operator '" << expr.id() << "' expects two operands" << eom;
327 throw 0;
328 }
329
332
333 expr.type()=bool_typet();
334}
335
337{
338 if(expr.operands().size()!=2)
339 {
341 error() << "operator '" << expr.id() << "' expects two operands" << eom;
342 throw 0;
343 }
344
347
348 // special case for function identifiers
349 if(
350 to_binary_expr(expr).op1().id() == "fid" ||
351 to_binary_expr(expr).op1().id() == "constructid")
352 expr.type() = code_typet({}, typet());
353 else
354 expr.type()=jsil_value_type();
355}
356
358{
359 if(expr.operands().size()!=2)
360 {
362 error() << "operator '" << expr.id() << "' expects two operands" << eom;
363 throw 0;
364 }
365
368
369 expr.type()=bool_typet();
370}
371
373{
374 if(expr.operands().size()!=1)
375 {
377 error() << "operator '" << expr.id() << "' expects single operand" << eom;
378 throw 0;
379 }
380
382
383 expr.type()=string_typet();
384}
385
387{
388 if(expr.operands().size()!=1)
389 {
391 error() << "operator '" << expr.id() << "' expects single operand" << eom;
392 throw 0;
393 }
394
396
397 expr.type()=jsil_value_type();
398}
399
401{
402 if(expr.operands().size()!=3)
403 {
405 error() << "operator '" << expr.id() << "' expects three operands" << eom;
406 throw 0;
407 }
408
411
412 exprt &operand3 = to_multi_ary_expr(expr).op2();
413 make_type_compatible(operand3, jsil_kind(), true);
414
415 if(operand3.id()==ID_member)
417 else if(operand3.id()=="variable")
419 else
420 {
422 error() << "operator '" << expr.id()
423 << "' expects reference type in the third parameter. Got:"
424 << operand3.pretty() << eom;
425 throw 0;
426 }
427}
428
430{
431 if(expr.operands().size()!=2)
432 {
434 error() << "operator '" << expr.id() << "' expects two operands" << eom;
435 throw 0;
436 }
437
440
441 expr.type()=string_typet();
442}
443
445{
446 if(expr.operands().size()!=2)
447 {
449 error() << "operator '" << expr.id() << "' expects two operands" << eom;
450 throw 0;
451 }
452
453 make_type_compatible(to_binary_expr(expr).op0(), jsil_kind(), true);
454 make_type_compatible(to_binary_expr(expr).op1(), jsil_kind(), true);
455
456 expr.type()=bool_typet();
457}
458
460{
461 if(expr.operands().size()!=2)
462 {
464 error() << "operator '" << expr.id() << "' expects two operands" << eom;
465 throw 0;
466 }
467
468 make_type_compatible(to_binary_expr(expr).op0(), bool_typet(), true);
469 make_type_compatible(to_binary_expr(expr).op1(), bool_typet(), true);
470
471 expr.type()=bool_typet();
472}
473
475{
476 if(expr.operands().size()!=2)
477 {
479 error() << "operator '" << expr.id() << "' expects two operands" << eom;
480 throw 0;
481 }
482
485
486 expr.type()=floatbv_typet();
487}
488
490{
491 if(expr.operands().size()!=2)
492 {
494 error() << "operator '" << expr.id() << "' expects two operands" << eom;
495 throw 0;
496 }
497
498 // operands can be of any types
499
500 expr.type()=bool_typet();
501}
502
504{
505 if(expr.operands().size()!=2)
506 {
508 error() << "operator '" << expr.id() << "' expects two operands" << eom;
509 throw 0;
510 }
511
514
515 expr.type()=bool_typet();
516}
517
519{
520 if(expr.operands().size()!=1)
521 {
523 error() << "operator '" << expr.id() << "' expects one operand" << eom;
524 throw 0;
525 }
526
527 make_type_compatible(to_unary_expr(expr).op(), bool_typet(), true);
528
529 expr.type()=bool_typet();
530}
531
533{
534 if(expr.operands().size()!=1)
535 {
537 error() << "operator '" << expr.id() << "' expects one operand" << eom;
538 throw 0;
539 }
540
542
543 expr.type()=floatbv_typet();
544}
545
547{
548 if(expr.operands().size()!=1)
549 {
551 error() << "operator '" << expr.id() << "' expects one operand" << eom;
552 throw 0;
553 }
554
556}
557
559{
560 irep_idt identifier=symbol_expr.get_identifier();
561
562 // if this is a built-in identifier, check if it exists in the
563 // symbol table and retrieve it's type
564 // TODO: add a flag for not needing to prefix internal symbols
565 // that do not start with hash
566 if(has_prefix(id2string(identifier), "#") ||
567 identifier=="eval" ||
568 identifier=="nan")
569 {
570 symbol_tablet::symbolst::const_iterator s_it=
571 symbol_table.symbols.find(identifier);
572
573 if(s_it==symbol_table.symbols.end())
574 {
575 error() << "unexpected internal symbol: " << identifier << eom;
576 throw 0;
577 }
578 else
579 {
580 // symbol already exists
581 const symbolt &symbol=s_it->second;
582
583 // type the expression
584 symbol_expr.type()=symbol.type;
585 }
586 }
587 else
588 {
589 // if this is a variable, we need to check if we already
590 // prefixed it and add to the symbol table if it is not there already
591 irep_idt identifier_base = identifier;
592 if(!has_prefix(id2string(identifier), id2string(proc_name)))
593 {
594 identifier = add_prefix(identifier);
595 symbol_expr.set_identifier(identifier);
596 }
597
598 symbol_tablet::symbolst::const_iterator s_it=
599 symbol_table.symbols.find(identifier);
600
601 if(s_it==symbol_table.symbols.end())
602 {
603 // create new symbol
604 symbolt new_symbol;
605 new_symbol.name=identifier;
606 new_symbol.type=symbol_expr.type();
607 new_symbol.base_name=identifier_base;
608 new_symbol.mode="jsil";
609 new_symbol.is_type=false;
610 new_symbol.is_lvalue=new_symbol.type.id()!=ID_code;
611
612 // mark as already typechecked
613 new_symbol.is_extern=true;
614
615 if(symbol_table.add(new_symbol))
616 {
617 error() << "failed to add symbol '" << new_symbol.name
618 << "' in the symbol table" << eom;
619 throw 0;
620 }
621 }
622 else
623 {
624 // symbol already exists
625 assert(!s_it->second.is_type);
626
627 const symbolt &symbol=s_it->second;
628
629 // type the expression
630 symbol_expr.type()=symbol.type;
631 }
632 }
633}
634
636{
637 const irep_idt &statement=code.get_statement();
638
639 if(statement==ID_function_call)
641 else if(statement==ID_return)
643 else if(statement==ID_expression)
644 {
645 if(code.operands().size()!=1)
646 {
648 error() << "expression statement expected to have one operand"
649 << eom;
650 throw 0;
651 }
652
653 typecheck_expr(code.op0());
654 }
655 else if(statement==ID_label)
656 {
657 typecheck_code(to_code_label(code).code());
658 // TODO: produce defined label set
659 }
660 else if(statement==ID_block)
661 typecheck_block(code);
662 else if(statement==ID_ifthenelse)
664 else if(statement==ID_goto)
665 {
666 // TODO: produce used label set
667 }
668 else if(statement==ID_assign)
670 else if(statement==ID_try_catch)
672 else if(statement==ID_skip)
673 {
674 }
675 else
676 {
678 error() << "unexpected statement: " << statement << eom;
679 throw 0;
680 }
681}
682
684{
685 if(code.has_return_value())
687}
688
690{
691 Forall_operands(it, code)
693}
694
696{
697 // A special case of try catch with one catch clause
698 if(code.operands().size()!=3)
699 {
701 error() << "try_catch expected to have three operands" << eom;
702 throw 0;
703 }
704
705 // function call
707
708 // catch decl is not used, but is required by goto-programs
709
711}
712
715{
716 if(call.operands().size()!=3)
717 {
719 error() << "function call expected to have three operands" << eom;
720 throw 0;
721 }
722
723 exprt &lhs=call.lhs();
724 typecheck_expr(lhs);
725
726 exprt &f=call.function();
728
729 for(auto &arg : call.arguments())
730 typecheck_expr(arg);
731
732 // Look for a function declaration symbol in the symbol table
733 if(f.id()==ID_symbol)
734 {
736
737 if(const auto maybe_symbol=symbol_table.lookup(id))
738 {
739 const symbolt &s=*maybe_symbol;
740
741 if(s.type.id()==ID_code)
742 {
744
745 for(std::size_t i=0; i<codet.parameters().size(); i++)
746 {
747 if(i>=call.arguments().size())
748 break;
749
750 const typet &param_type=codet.parameters()[i].type();
751
752 if(!param_type.id().empty() && param_type.is_not_nil())
753 {
754 // check argument's type if parameter's type is given
755 make_type_compatible(call.arguments()[i], param_type, true);
756 }
757 }
758
759 // if there are too few arguments, add undefined
760 if(codet.parameters().size()>call.arguments().size())
761 {
762 for(std::size_t i=call.arguments().size();
763 i<codet.parameters().size();
764 ++i)
765 call.arguments().push_back(
766 exprt("undefined", jsil_undefined_type()));
767 }
768
769 // if there are too many arguments, remove
770 while(codet.parameters().size()<call.arguments().size())
771 call.arguments().pop_back();
772
773 // check return type if exists
774 if(!codet.return_type().id().empty() &&
775 codet.return_type().is_not_nil())
776 make_type_compatible(lhs, codet.return_type(), true);
777 else make_type_compatible(lhs, jsil_any_type(), true);
778 }
779 else
780 {
781 // TODO: a symbol can be a variable evaluating to a string
782 // which corresponds to a function identifier
784 }
785 }
786 else
787 {
788 // Should be function, declaration not found yet
789 symbolt new_symbol;
790 new_symbol.name=id;
791 new_symbol.type = code_typet({}, typet());
792 new_symbol.mode="jsil";
793 new_symbol.is_type=false;
794 new_symbol.value=exprt("no-body-just-yet");
795
797
798 if(symbol_table.add(new_symbol))
799 {
800 error().source_location=new_symbol.location;
801 error() << "failed to add expression symbol to symbol table"
802 << eom;
803 throw 0;
804 }
805 }
806 }
807 else
808 {
809 // TODO: this might be a string literal
810 // which corresponds to a function identifier
812 }
813}
814
816{
817 exprt &cond=code.cond();
818 typecheck_expr(cond);
819 make_type_compatible(cond, bool_typet(), true);
820
822
823 if(!code.else_case().is_nil())
825}
826
828{
829 typecheck_expr(code.lhs());
830 typecheck_expr(code.rhs());
831
832 make_type_compatible(code.lhs(), code.rhs().type(), false);
833}
834
839{
840 assert(!symbol.is_type);
841
842 // Using is_extern to check if symbol was already typechecked
843 if(symbol.is_extern)
844 return;
845 if(symbol.value.id()!="no-body-just-yet")
846 symbol.is_extern=true;
847
848 proc_name=symbol.name;
849 typecheck_type(symbol.type);
850
851 if(symbol.value.id()==ID_code)
853 else if(symbol.name=="eval")
854 {
855 // No code for eval. Do nothing
856 }
857 else if(symbol.value.id()=="no-body-just-yet")
858 {
859 // Do nothing
860 }
861 else
862 {
864 error() << "non-type symbol value expected code, but got "
865 << symbol.value.pretty() << eom;
866 throw 0;
867 }
868}
869
871{
872 // The hash table iterators are not stable,
873 // and we might add new symbols.
874
875 std::vector<irep_idt> identifiers;
876 identifiers.reserve(symbol_table.symbols.size());
877 for(const auto &symbol_pair : symbol_table.symbols)
878 {
879 identifiers.push_back(symbol_pair.first);
880 }
881
882 // We first check all type symbols,
883 // recursively doing base classes first.
884 for(const irep_idt &id : identifiers)
885 {
887 if(symbol.is_type)
888 typecheck_type_symbol(symbol);
889 }
890
891 // We now check all non-type symbols
892 for(const irep_idt &id : identifiers)
893 {
895 if(!symbol.is_type)
897 }
898}
899
901 symbol_tablet &symbol_table,
902 message_handlert &message_handler)
903{
904 jsil_typecheckt jsil_typecheck(symbol_table, message_handler);
905 return jsil_typecheck.typecheck_main();
906}
907
909 exprt &expr,
910 message_handlert &message_handler,
911 const namespacet &)
912{
913 const unsigned errors_before=
914 message_handler.get_message_count(messaget::M_ERROR);
915
916 symbol_tablet symbol_table;
917
919 symbol_table,
920 message_handler);
921
922 try
923 {
924 jsil_typecheck.typecheck_expr(expr);
925 }
926
927 catch(int)
928 {
929 jsil_typecheck.error();
930 }
931
932 catch(const char *e)
933 {
934 jsil_typecheck.error() << e << messaget::eom;
935 }
936
937 catch(const std::string &e)
938 {
939 jsil_typecheck.error() << e << messaget::eom;
940 }
941
942 return message_handler.get_message_count(messaget::M_ERROR)!=errors_before;
943}
Pre-defined bitvector types.
The Boolean type.
Definition: std_types.h:36
A codet representing an assignment in the program.
codet representation of a "return from a function" statement.
Definition: std_code.h:893
const exprt & return_value() const
Definition: std_code.h:903
bool has_return_value() const
Definition: std_code.h:913
codet representation of a function call statement.
codet representation of an if-then-else statement.
Definition: std_code.h:460
const exprt & cond() const
Definition: std_code.h:478
const codet & else_case() const
Definition: std_code.h:498
const codet & then_case() const
Definition: std_code.h:488
codet representation of a try/catch block.
Definition: std_code.h:1986
codet & try_code()
Definition: std_code.h:1994
codet & get_catch_code(unsigned i)
Definition: std_code.h:2016
Base type of functions.
Definition: std_types.h:539
const parameterst & parameters() const
Definition: std_types.h:655
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
exprt & op0()
Definition: expr.h:99
const irep_idt & get_statement() const
Definition: std_code_base.h:65
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
const source_locationt & source_location() const
Definition: expr.h:230
Fixed-width bit-vector with IEEE floating-point interpretation.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:372
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
bool is_not_nil() const
Definition: irep.h:380
const irep_idt & id() const
Definition: irep.h:396
irept & add(const irep_idt &name)
Definition: irep.cpp:116
bool is_nil() const
Definition: irep.h:376
void typecheck_expr_side_effect_throw(side_effect_expr_throwt &expr)
void typecheck_expr_binary_arith(exprt &expr)
void typecheck_expr_constant(exprt &expr)
void typecheck_expr_has_field(exprt &expr)
void typecheck_expr_main(exprt &expr)
void typecheck_type_symbol(symbolt &)
void typecheck_function_call(code_function_callt &function_call)
virtual void typecheck_expr(exprt &expr)
void typecheck_expr_unary_boolean(exprt &expr)
void typecheck_try_catch(code_try_catcht &code)
void typecheck_assign(code_assignt &code)
symbol_table_baset & symbol_table
void typecheck_expr_index(exprt &expr)
void typecheck_expr_proto_field(exprt &expr)
void typecheck_ifthenelse(code_ifthenelset &code)
void typecheck_expr_subtype(exprt &expr)
void typecheck_expr_ref(exprt &expr)
const namespacet ns
irep_idt add_prefix(const irep_idt &ds)
Prefix parameters and variables with a procedure name.
void typecheck_expr_binary_boolean(exprt &expr)
void typecheck_expr_concatenation(exprt &expr)
virtual void typecheck()
irep_idt proc_name
void typecheck_expr_field(exprt &expr)
void typecheck_expr_unary_string(exprt &expr)
void typecheck_code(codet &code)
virtual std::string to_string(const exprt &expr)
void make_type_compatible(exprt &expr, const typet &type, bool must)
void typecheck_exp_binary_equal(exprt &expr)
void typecheck_expr_operands(exprt &expr)
void typecheck_expr_base(exprt &expr)
void typecheck_expr_delete(exprt &expr)
void typecheck_expr_proto_obj(exprt &expr)
void typecheck_block(codet &code)
void typecheck_expr_unary_num(exprt &expr)
void typecheck_symbol_expr(symbol_exprt &symbol_expr)
void typecheck_type(typet &type)
void typecheck_non_type_symbol(symbolt &symbol)
typechecking procedure declaration; any other symbols should have been typechecked during typecheckin...
void update_expr_type(exprt &expr, const typet &type)
void typecheck_return(code_frontend_returnt &)
void typecheck_expr_binary_compare(exprt &expr)
std::size_t get_message_count(unsigned level) const
Definition: message.h:56
source_locationt source_location
Definition: message.h:247
mstreamt & error() const
Definition: message.h:399
@ M_ERROR
Definition: message.h:170
static eomt eom
Definition: message.h:297
exprt & op2()
Definition: std_expr.h:856
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
Definition: symbol.h:171
A side_effect_exprt representation of a side effect that throws an exception.
Definition: std_code.h:1757
String type.
Definition: std_types.h:901
Expression to hold a symbol (variable)
Definition: std_expr.h:80
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:104
const irep_idt & get_identifier() const
Definition: std_expr.h:109
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_extern
Definition: symbol.h:66
bool is_type
Definition: symbol.h:61
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
bool is_lvalue
Definition: symbol.h:66
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
The type of an expression, extends irept.
Definition: type.h:29
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
std::string type2jsil(const typet &type, const namespacet &ns)
Definition: expr2jsil.cpp:31
std::string expr2jsil(const exprt &expr, const namespacet &ns)
Definition: expr2jsil.cpp:24
Jsil Language.
#define Forall_operands(it, expr)
Definition: expr.h:25
const code_function_callt & to_code_function_call(const codet &code)
const code_assignt & to_code_assign(const codet &code)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
bool jsil_typecheck(symbol_tablet &symbol_table, message_handlert &message_handler)
Jsil Language.
typet jsil_value_or_empty_type()
Definition: jsil_types.cpp:24
typet jsil_empty_type()
Definition: jsil_types.cpp:95
typet jsil_undefined_type()
Definition: jsil_types.cpp:85
typet jsil_null_type()
Definition: jsil_types.cpp:80
typet jsil_variable_reference_type()
Definition: jsil_types.cpp:59
bool jsil_is_subtype(const typet &type1, const typet &type2)
Definition: jsil_types.cpp:100
typet jsil_kind()
Definition: jsil_types.cpp:90
typet jsil_user_object_type()
Definition: jsil_types.cpp:70
typet jsil_union(const typet &type1, const typet &type2)
Definition: jsil_types.cpp:121
bool jsil_incompatible_types(const typet &type1, const typet &type2)
Definition: jsil_types.cpp:115
typet jsil_any_type()
Definition: jsil_types.cpp:18
typet jsil_reference_type()
Definition: jsil_types.cpp:48
typet jsil_member_reference_type()
Definition: jsil_types.cpp:54
typet jsil_value_or_reference_type()
Definition: jsil_types.cpp:29
typet jsil_value_type()
Definition: jsil_types.cpp:34
typet jsil_object_type()
Definition: jsil_types.cpp:64
Jsil Language.
bool is_jsil_spec_code_type(const typet &type)
Definition: jsil_types.h:77
bool is_jsil_builtin_code_type(const typet &type)
Definition: jsil_types.h:54
const code_frontend_returnt & to_code_frontend_return(const codet &code)
Definition: std_code.h:943
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1004
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:530
const code_try_catcht & to_code_try_catch(const codet &code)
Definition: std_code.h:2050
side_effect_expr_throwt & to_side_effect_expr_throw(exprt &expr)
Definition: std_code.h:1778
const codet & to_code(const exprt &expr)
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:899
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
Author: Diffblue Ltd.