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
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.is_constant())
166 {
167 }
168 else
169 {
171 expr.type().is_nil() || expr.type().id().empty(),
172 "expressions are expected not to have type set just yet");
173
174 if(expr.id()==ID_null ||
175 expr.id()=="undefined" ||
176 expr.id()==ID_empty)
178 else if(expr.id()=="null_type" ||
179 expr.id()=="undefined_type" ||
180 expr.id()==ID_boolean ||
181 expr.id()==ID_string ||
182 expr.id()=="number" ||
183 expr.id()=="builtin_object" ||
184 expr.id()=="user_object" ||
185 expr.id()=="object" ||
186 expr.id()==ID_pointer ||
187 expr.id()==ID_member ||
188 expr.id()=="variable")
189 expr.type()=jsil_kind();
190 else if(expr.id()=="proto" ||
191 expr.id()=="fid" ||
192 expr.id()=="scope" ||
193 expr.id()=="constructid" ||
194 expr.id()=="primvalue" ||
195 expr.id()=="targetfunction" ||
196 expr.id()==ID_class)
197 {
198 // TODO: have a special type for builtin fields
199 expr.type()=string_typet();
200 }
201 else if(expr.id()==ID_not)
203 else if(expr.id()=="string_to_num")
205 else if(expr.id()==ID_unary_minus ||
206 expr.id()=="num_to_int32" ||
207 expr.id()=="num_to_uint32" ||
208 expr.id()==ID_bitnot)
209 {
211 expr.type()=floatbv_typet();
212 }
213 else if(expr.id()=="num_to_string")
214 {
216 expr.type()=string_typet();
217 }
218 else if(expr.id()==ID_equal)
220 else if(expr.id()==ID_lt ||
221 expr.id()==ID_le)
223 else if(expr.id()==ID_plus ||
224 expr.id()==ID_minus ||
225 expr.id()==ID_mult ||
226 expr.id()==ID_div ||
227 expr.id()==ID_mod ||
228 expr.id()==ID_bitand ||
229 expr.id()==ID_bitor ||
230 expr.id()==ID_bitxor ||
231 expr.id()==ID_shl ||
232 expr.id()==ID_shr ||
233 expr.id()==ID_lshr)
235 else if(expr.id()==ID_and ||
236 expr.id()==ID_or)
238 else if(expr.id()=="subtype_of")
240 else if(expr.id()==ID_concatenation)
242 else if(expr.id()=="ref")
243 typecheck_expr_ref(expr);
244 else if(expr.id()=="field")
246 else if(expr.id()==ID_base)
248 else if(expr.id()==ID_typeof)
249 expr.type()=jsil_kind();
250 else if(expr.id()=="new")
252 else if(expr.id()=="hasField")
254 else if(expr.id()==ID_index)
256 else if(expr.id()=="delete")
258 else if(expr.id()=="protoField")
260 else if(expr.id()=="protoObj")
262 else if(expr.id()==ID_side_effect)
264 else
265 {
267 error() << "unexpected expression: " << expr.pretty() << eom;
268 throw 0;
269 }
270 }
271}
272
275{
276 irept &excep_list=expr.add(ID_exception_list);
277 PRECONDITION(excep_list.id() == ID_symbol);
278 symbol_exprt &s=static_cast<symbol_exprt &>(excep_list);
280}
281
283{
284 if(expr.id()==ID_null)
285 expr.type()=jsil_null_type();
286 else if(expr.id()=="undefined")
287 expr.type()=jsil_undefined_type();
288 else if(expr.id()==ID_empty)
289 expr.type()=jsil_empty_type();
290}
291
293{
294 if(expr.operands().size()!=2)
295 {
297 error() << "operator '" << expr.id() << "' expects two operands" << eom;
298 throw 0;
299 }
300
303
305}
306
308{
309 if(expr.operands().size()!=2)
310 {
312 error() << "operator '" << expr.id() << "' expects two operands";
313 throw 0;
314 }
315
318
319 expr.type()=bool_typet();
320}
321
323{
324 if(expr.operands().size()!=2)
325 {
327 error() << "operator '" << expr.id() << "' expects two operands" << eom;
328 throw 0;
329 }
330
333
334 expr.type()=bool_typet();
335}
336
338{
339 if(expr.operands().size()!=2)
340 {
342 error() << "operator '" << expr.id() << "' expects two operands" << eom;
343 throw 0;
344 }
345
348
349 // special case for function identifiers
350 if(
351 to_binary_expr(expr).op1().id() == "fid" ||
352 to_binary_expr(expr).op1().id() == "constructid")
353 expr.type() = code_typet({}, typet());
354 else
355 expr.type()=jsil_value_type();
356}
357
359{
360 if(expr.operands().size()!=2)
361 {
363 error() << "operator '" << expr.id() << "' expects two operands" << eom;
364 throw 0;
365 }
366
369
370 expr.type()=bool_typet();
371}
372
374{
375 if(expr.operands().size()!=1)
376 {
378 error() << "operator '" << expr.id() << "' expects single operand" << eom;
379 throw 0;
380 }
381
383
384 expr.type()=string_typet();
385}
386
388{
389 if(expr.operands().size()!=1)
390 {
392 error() << "operator '" << expr.id() << "' expects single operand" << eom;
393 throw 0;
394 }
395
397
398 expr.type()=jsil_value_type();
399}
400
402{
403 if(expr.operands().size()!=3)
404 {
406 error() << "operator '" << expr.id() << "' expects three operands" << eom;
407 throw 0;
408 }
409
412
413 exprt &operand3 = to_multi_ary_expr(expr).op2();
414 make_type_compatible(operand3, jsil_kind(), true);
415
416 if(operand3.id()==ID_member)
418 else if(operand3.id()=="variable")
420 else
421 {
423 error() << "operator '" << expr.id()
424 << "' expects reference type in the third parameter. Got:"
425 << operand3.pretty() << eom;
426 throw 0;
427 }
428}
429
431{
432 if(expr.operands().size()!=2)
433 {
435 error() << "operator '" << expr.id() << "' expects two operands" << eom;
436 throw 0;
437 }
438
441
442 expr.type()=string_typet();
443}
444
446{
447 if(expr.operands().size()!=2)
448 {
450 error() << "operator '" << expr.id() << "' expects two operands" << eom;
451 throw 0;
452 }
453
454 make_type_compatible(to_binary_expr(expr).op0(), jsil_kind(), true);
455 make_type_compatible(to_binary_expr(expr).op1(), jsil_kind(), true);
456
457 expr.type()=bool_typet();
458}
459
461{
462 if(expr.operands().size()!=2)
463 {
465 error() << "operator '" << expr.id() << "' expects two operands" << eom;
466 throw 0;
467 }
468
469 make_type_compatible(to_binary_expr(expr).op0(), bool_typet(), true);
470 make_type_compatible(to_binary_expr(expr).op1(), bool_typet(), true);
471
472 expr.type()=bool_typet();
473}
474
476{
477 if(expr.operands().size()!=2)
478 {
480 error() << "operator '" << expr.id() << "' expects two operands" << eom;
481 throw 0;
482 }
483
486
487 expr.type()=floatbv_typet();
488}
489
491{
492 if(expr.operands().size()!=2)
493 {
495 error() << "operator '" << expr.id() << "' expects two operands" << eom;
496 throw 0;
497 }
498
499 // operands can be of any types
500
501 expr.type()=bool_typet();
502}
503
505{
506 if(expr.operands().size()!=2)
507 {
509 error() << "operator '" << expr.id() << "' expects two operands" << eom;
510 throw 0;
511 }
512
515
516 expr.type()=bool_typet();
517}
518
520{
521 if(expr.operands().size()!=1)
522 {
524 error() << "operator '" << expr.id() << "' expects one operand" << eom;
525 throw 0;
526 }
527
528 make_type_compatible(to_unary_expr(expr).op(), bool_typet(), true);
529
530 expr.type()=bool_typet();
531}
532
534{
535 if(expr.operands().size()!=1)
536 {
538 error() << "operator '" << expr.id() << "' expects one operand" << eom;
539 throw 0;
540 }
541
543
544 expr.type()=floatbv_typet();
545}
546
548{
549 if(expr.operands().size()!=1)
550 {
552 error() << "operator '" << expr.id() << "' expects one operand" << eom;
553 throw 0;
554 }
555
557}
558
560{
561 irep_idt identifier=symbol_expr.get_identifier();
562
563 // if this is a built-in identifier, check if it exists in the
564 // symbol table and retrieve it's type
565 // TODO: add a flag for not needing to prefix internal symbols
566 // that do not start with hash
567 if(has_prefix(id2string(identifier), "#") ||
568 identifier=="eval" ||
569 identifier=="nan")
570 {
571 symbol_table_baset::symbolst::const_iterator s_it =
572 symbol_table.symbols.find(identifier);
573
574 if(s_it==symbol_table.symbols.end())
575 {
576 error() << "unexpected internal symbol: " << identifier << eom;
577 throw 0;
578 }
579 else
580 {
581 // symbol already exists
582 const symbolt &symbol=s_it->second;
583
584 // type the expression
585 symbol_expr.type()=symbol.type;
586 }
587 }
588 else
589 {
590 // if this is a variable, we need to check if we already
591 // prefixed it and add to the symbol table if it is not there already
592 irep_idt identifier_base = identifier;
593 if(!has_prefix(id2string(identifier), id2string(proc_name)))
594 {
595 identifier = add_prefix(identifier);
596 symbol_expr.set_identifier(identifier);
597 }
598
599 symbol_table_baset::symbolst::const_iterator s_it =
600 symbol_table.symbols.find(identifier);
601
602 if(s_it==symbol_table.symbols.end())
603 {
604 // create new symbol
605 symbolt new_symbol{identifier, symbol_expr.type(), "jsil"};
606 new_symbol.base_name=identifier_base;
607 new_symbol.is_lvalue=new_symbol.type.id()!=ID_code;
608
609 // mark as already typechecked
610 new_symbol.is_extern=true;
611
612 if(symbol_table.add(new_symbol))
613 {
614 error() << "failed to add symbol '" << new_symbol.name
615 << "' in the symbol table" << eom;
616 throw 0;
617 }
618 }
619 else
620 {
621 // symbol already exists
622 DATA_INVARIANT(!s_it->second.is_type, "non-type symbol expected");
623
624 const symbolt &symbol=s_it->second;
625
626 // type the expression
627 symbol_expr.type()=symbol.type;
628 }
629 }
630}
631
633{
634 const irep_idt &statement=code.get_statement();
635
636 if(statement==ID_function_call)
638 else if(statement==ID_return)
640 else if(statement==ID_expression)
641 {
642 if(code.operands().size()!=1)
643 {
645 error() << "expression statement expected to have one operand"
646 << eom;
647 throw 0;
648 }
649
650 typecheck_expr(code.op0());
651 }
652 else if(statement==ID_label)
653 {
654 typecheck_code(to_code_label(code).code());
655 // TODO: produce defined label set
656 }
657 else if(statement==ID_block)
658 typecheck_block(code);
659 else if(statement==ID_ifthenelse)
661 else if(statement==ID_goto)
662 {
663 // TODO: produce used label set
664 }
665 else if(statement==ID_assign)
667 else if(statement==ID_try_catch)
669 else if(statement==ID_skip)
670 {
671 }
672 else
673 {
675 error() << "unexpected statement: " << statement << eom;
676 throw 0;
677 }
678}
679
685
687{
688 Forall_operands(it, code)
690}
691
693{
694 // A special case of try catch with one catch clause
695 if(code.operands().size()!=3)
696 {
698 error() << "try_catch expected to have three operands" << eom;
699 throw 0;
700 }
701
702 // function call
704
705 // catch decl is not used, but is required by goto-programs
706
708}
709
712{
713 if(call.operands().size()!=3)
714 {
716 error() << "function call expected to have three operands" << eom;
717 throw 0;
718 }
719
720 exprt &lhs=call.lhs();
721 typecheck_expr(lhs);
722
723 exprt &f=call.function();
725
726 for(auto &arg : call.arguments())
727 typecheck_expr(arg);
728
729 // Look for a function declaration symbol in the symbol table
730 if(f.id()==ID_symbol)
731 {
733
734 if(const auto maybe_symbol=symbol_table.lookup(id))
735 {
736 const symbolt &s=*maybe_symbol;
737
738 if(s.type.id()==ID_code)
739 {
741
742 for(std::size_t i=0; i<codet.parameters().size(); i++)
743 {
744 if(i>=call.arguments().size())
745 break;
746
747 const typet &param_type=codet.parameters()[i].type();
748
749 if(!param_type.id().empty() && param_type.is_not_nil())
750 {
751 // check argument's type if parameter's type is given
752 make_type_compatible(call.arguments()[i], param_type, true);
753 }
754 }
755
756 // if there are too few arguments, add undefined
757 if(codet.parameters().size()>call.arguments().size())
758 {
759 for(std::size_t i=call.arguments().size();
760 i<codet.parameters().size();
761 ++i)
762 call.arguments().push_back(
763 exprt("undefined", jsil_undefined_type()));
764 }
765
766 // if there are too many arguments, remove
767 while(codet.parameters().size()<call.arguments().size())
768 call.arguments().pop_back();
769
770 // check return type if exists
771 if(!codet.return_type().id().empty() &&
772 codet.return_type().is_not_nil())
773 make_type_compatible(lhs, codet.return_type(), true);
774 else make_type_compatible(lhs, jsil_any_type(), true);
775 }
776 else
777 {
778 // TODO: a symbol can be a variable evaluating to a string
779 // which corresponds to a function identifier
781 }
782 }
783 else
784 {
785 // Should be function, declaration not found yet
786 symbolt new_symbol{id, code_typet({}, typet()), "jsil"};
787 new_symbol.value=exprt("no-body-just-yet");
788
790
791 if(symbol_table.add(new_symbol))
792 {
793 error().source_location=new_symbol.location;
794 error() << "failed to add expression symbol to symbol table"
795 << eom;
796 throw 0;
797 }
798 }
799 }
800 else
801 {
802 // TODO: this might be a string literal
803 // which corresponds to a function identifier
805 }
806}
807
809{
810 exprt &cond=code.cond();
811 typecheck_expr(cond);
812 make_type_compatible(cond, bool_typet(), true);
813
815
816 if(!code.else_case().is_nil())
818}
819
821{
822 typecheck_expr(code.lhs());
823 typecheck_expr(code.rhs());
824
825 make_type_compatible(code.lhs(), code.rhs().type(), false);
826}
827
832{
833 PRECONDITION(!symbol.is_type);
834
835 // Using is_extern to check if symbol was already typechecked
836 if(symbol.is_extern)
837 return;
838 if(symbol.value.id()!="no-body-just-yet")
839 symbol.is_extern=true;
840
841 proc_name=symbol.name;
842 typecheck_type(symbol.type);
843
844 if(symbol.value.id()==ID_code)
846 else if(symbol.name=="eval")
847 {
848 // No code for eval. Do nothing
849 }
850 else if(symbol.value.id()=="no-body-just-yet")
851 {
852 // Do nothing
853 }
854 else
855 {
857 error() << "non-type symbol value expected code, but got "
858 << symbol.value.pretty() << eom;
859 throw 0;
860 }
861}
862
864{
865 // The hash table iterators are not stable,
866 // and we might add new symbols.
867
868 std::vector<irep_idt> identifiers;
869 identifiers.reserve(symbol_table.symbols.size());
870 for(const auto &symbol_pair : symbol_table.symbols)
871 {
872 identifiers.push_back(symbol_pair.first);
873 }
874
875 // We first check all type symbols,
876 // recursively doing base classes first.
877 for(const irep_idt &id : identifiers)
878 {
880 if(symbol.is_type)
881 typecheck_type_symbol(symbol);
882 }
883
884 // We now check all non-type symbols
885 for(const irep_idt &id : identifiers)
886 {
888 if(!symbol.is_type)
890 }
891}
892
894 symbol_table_baset &symbol_table,
895 message_handlert &message_handler)
896{
897 jsil_typecheckt jsil_typecheck(symbol_table, message_handler);
898 return jsil_typecheck.typecheck_main();
899}
900
902 exprt &expr,
903 message_handlert &message_handler,
904 const namespacet &)
905{
906 const unsigned errors_before=
907 message_handler.get_message_count(messaget::M_ERROR);
908
909 symbol_tablet symbol_table;
910
912 symbol_table,
913 message_handler);
914
915 try
916 {
917 jsil_typecheck.typecheck_expr(expr);
918 }
919
920 catch(int)
921 {
922 jsil_typecheck.error();
923 }
924
925 catch(const char *e)
926 {
927 jsil_typecheck.error() << e << messaget::eom;
928 }
929
930 catch(const std::string &e)
931 {
932 jsil_typecheck.error() << e << messaget::eom;
933 }
934
935 return message_handler.get_message_count(messaget::M_ERROR)!=errors_before;
936}
Pre-defined bitvector types.
The Boolean type.
Definition std_types.h:36
A goto_instruction_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
goto_instruction_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.
exprt & op0()
Definition expr.h:125
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
bool empty() const
Definition dstring.h:90
Base class for all expressions.
Definition expr.h:56
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:204
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
const source_locationt & source_location() const
Definition expr.h:223
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:490
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:111
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()
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:889
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:179
A side_effect_exprt representation of a side effect that throws an exception.
Definition std_code.h:1757
String type.
Definition std_types.h:913
Expression to hold a symbol (variable)
Definition std_expr.h:113
void set_identifier(const irep_idt &identifier)
Definition std_expr.h:137
const irep_idt & get_identifier() const
Definition std_expr.h:142
The symbol table base class interface.
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.
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:74
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
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:27
const code_function_callt & to_code_function_call(const goto_instruction_codet &code)
const code_assignt & to_code_assign(const goto_instruction_codet &code)
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
bool jsil_typecheck(symbol_table_baset &symbol_table, message_handlert &message_handler)
Jsil Language.
typet jsil_value_or_empty_type()
typet jsil_empty_type()
typet jsil_undefined_type()
typet jsil_null_type()
typet jsil_variable_reference_type()
bool jsil_is_subtype(const typet &type1, const typet &type2)
typet jsil_kind()
typet jsil_user_object_type()
typet jsil_union(const typet &type1, const typet &type2)
bool jsil_incompatible_types(const typet &type1, const typet &type2)
typet jsil_any_type()
typet jsil_reference_type()
typet jsil_member_reference_type()
typet jsil_value_or_reference_type()
typet jsil_value_type()
typet jsil_object_type()
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
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
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:660
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:361
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition std_expr.h:932
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
Author: Diffblue Ltd.