CBMC
Loading...
Searching...
No Matches
std_code.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Data structures representing statements in a program
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9
10#ifndef CPROVER_UTIL_STD_CODE_H
11#define CPROVER_UTIL_STD_CODE_H
12
13#include <list>
14
15#include "std_code_base.h"
16#include "std_expr.h"
17
24{
25public:
27 {
28 operands().resize(2);
29 }
30
32 : codet(ID_assign, {std::move(lhs), std::move(rhs)})
33 {
34 }
35
37 : codet(ID_assign, {std::move(lhs), std::move(rhs)}, std::move(loc))
38 {
39 }
40
42 {
43 return op0();
44 }
45
47 {
48 return op1();
49 }
50
51 const exprt &lhs() const
52 {
53 return op0();
54 }
55
56 const exprt &rhs() const
57 {
58 return op1();
59 }
60
61 static void check(
62 const codet &code,
64 {
66 vm, code.operands().size() == 2, "assignment must have two operands");
67 }
68
69 static void validate(
70 const codet &code,
71 const namespacet &,
73 {
74 check(code, vm);
75
77 vm,
78 code.op0().type() == code.op1().type(),
79 "lhs and rhs of assignment must have same type");
80 }
81
82 static void validate_full(
83 const codet &code,
84 const namespacet &ns,
86 {
87 for(const exprt &op : code.operands())
88 {
89 validate_full_expr(op, ns, vm);
90 }
91
92 validate(code, ns, vm);
93 }
94
95protected:
96 using codet::op0;
97 using codet::op1;
98 using codet::op2;
99 using codet::op3;
100};
101
102template <>
104{
106}
107
112
114{
117 return static_cast<const code_frontend_assignt &>(code);
118}
119
121{
124 return static_cast<code_frontend_assignt &>(code);
125}
126
129class code_blockt:public codet
130{
131public:
133 {
134 }
135
136 typedef std::vector<codet> code_operandst;
137
139 {
140 return (code_operandst &)get_sub();
141 }
142
144 {
145 return (const code_operandst &)get_sub();
146 }
147
148 static code_blockt from_list(const std::list<codet> &_list)
149 {
150 code_blockt result;
151 auto &s=result.statements();
152 s.reserve(_list.size());
153 for(const auto &c : _list)
154 s.push_back(c);
155 return result;
156 }
157
158 explicit code_blockt(const std::vector<codet> &_statements)
159 : codet(ID_block, (const std::vector<exprt> &)_statements)
160 {
161 }
162
163 explicit code_blockt(std::vector<codet> &&_statements)
164 : codet(ID_block, std::move((std::vector<exprt> &&) _statements))
165 {
166 }
167
168 void add(const codet &code)
169 {
170 add_to_operands(code);
171 }
172
173 void add(codet &&code)
174 {
175 add_to_operands(std::move(code));
176 }
177
178 void add(codet code, source_locationt loc)
179 {
180 code.add_source_location().swap(loc);
181 add(std::move(code));
182 }
183
184 void append(const code_blockt &extra_block);
185
186 // This is the closing '}' or 'END' at the end of a block
188 {
189 return static_cast<const source_locationt &>(find(ID_C_end_location));
190 }
191
193};
194
195template<> inline bool can_cast_expr<code_blockt>(const exprt &base)
196{
198}
199
200// to_code_block has no validation other than checking the statement(), so no
201// validate_expr is provided for code_blockt
202
203inline const code_blockt &to_code_block(const codet &code)
204{
206 return static_cast<const code_blockt &>(code);
207}
208
210{
212 return static_cast<code_blockt &>(code);
213}
214
216class code_assumet : public codet
217{
218public:
219 explicit code_assumet(exprt expr) : codet(ID_assume, {std::move(expr)})
220 {
221 }
222
223 const exprt &assumption() const
224 {
225 return op0();
226 }
227
229 {
230 return op0();
231 }
232
233protected:
234 using codet::op0;
235 using codet::op1;
236 using codet::op2;
237 using codet::op3;
238};
239
240template <>
241inline bool can_cast_expr<code_assumet>(const exprt &base)
242{
244}
245
246inline void validate_expr(const code_assumet &x)
247{
248 validate_operands(x, 1, "assume must have one operand");
249}
250
251inline const code_assumet &to_code_assume(const codet &code)
252{
254 const code_assumet &ret = static_cast<const code_assumet &>(code);
256 return ret;
257}
258
260{
262 code_assumet &ret = static_cast<code_assumet &>(code);
264 return ret;
265}
266
269class code_assertt : public codet
270{
271public:
272 explicit code_assertt(exprt expr) : codet(ID_assert, {std::move(expr)})
273 {
274 }
275
276 const exprt &assertion() const
277 {
278 return op0();
279 }
280
282 {
283 return op0();
284 }
285
286protected:
287 using codet::op0;
288 using codet::op1;
289 using codet::op2;
290 using codet::op3;
291};
292
293template <>
294inline bool can_cast_expr<code_assertt>(const exprt &base)
295{
297}
298
299inline void validate_expr(const code_assertt &x)
300{
301 validate_operands(x, 1, "assert must have one operand");
302}
303
304inline const code_assertt &to_code_assert(const codet &code)
305{
307 const code_assertt &ret = static_cast<const code_assertt &>(code);
309 return ret;
310}
311
313{
315 code_assertt &ret = static_cast<code_assertt &>(code);
317 return ret;
318}
319
321class code_skipt:public codet
322{
323public:
325 {
326 }
327
328protected:
329 using codet::op0;
330 using codet::op1;
331 using codet::op2;
332 using codet::op3;
333};
334
335template<> inline bool can_cast_expr<code_skipt>(const exprt &base)
336{
338}
339
340// there is no to_code_skip, so no validate_expr is provided for code_skipt
341
347{
348public:
350 : codet(ID_decl, {std::move(symbol)})
351 {
352 }
353
355 {
356 return static_cast<symbol_exprt &>(op0());
357 }
358
359 const symbol_exprt &symbol() const
360 {
361 return static_cast<const symbol_exprt &>(op0());
362 }
363
365 {
366 return symbol().get_identifier();
367 }
368
373 std::optional<exprt> initial_value() const
374 {
375 if(operands().size() < 2)
376 return {};
377 return {op1()};
378 }
379
384 void set_initial_value(std::optional<exprt> initial_value)
385 {
386 if(!initial_value)
387 {
388 operands().resize(1);
389 }
390 else if(operands().size() < 2)
391 {
392 PRECONDITION(operands().size() == 1);
393 add_to_operands(std::move(*initial_value));
394 }
395 else
396 {
397 op1() = std::move(*initial_value);
398 }
399 }
400
401 static void check(
402 const codet &code,
404 {
405 // will be size()==1 in the future
407 vm,
408 code.operands().size() >= 1,
409 "declaration must have one or more operands");
411 vm,
412 code.op0().id() == ID_symbol,
413 "declaring a non-symbol: " +
414 id2string(to_symbol_expr(code.op0()).get_identifier()));
415 }
416};
417
418template <>
420{
422}
423
428
430{
433 return static_cast<const code_frontend_declt &>(code);
434}
435
437{
440 return static_cast<code_frontend_declt &>(code);
441}
442
456 const exprt &condition, const source_locationt &source_location);
457
460{
461public:
464 : codet(
466 {std::move(condition), std::move(then_code), std::move(else_code)})
467 {
468 }
469
472 : codet(
474 {std::move(condition), std::move(then_code), nil_exprt()})
475 {
476 }
477
478 const exprt &cond() const
479 {
480 return op0();
481 }
482
484 {
485 return op0();
486 }
487
488 const codet &then_case() const
489 {
490 return static_cast<const codet &>(op1());
491 }
492
493 bool has_else_case() const
494 {
495 return op2().is_not_nil();
496 }
497
498 const codet &else_case() const
499 {
500 return static_cast<const codet &>(op2());
501 }
502
504 {
505 return static_cast<codet &>(op1());
506 }
507
509 {
510 return static_cast<codet &>(op2());
511 }
512
513protected:
514 using codet::op0;
515 using codet::op1;
516 using codet::op2;
517 using codet::op3;
518};
519
520template<> inline bool can_cast_expr<code_ifthenelset>(const exprt &base)
521{
523}
524
526{
527 validate_operands(x, 3, "if-then-else must have three operands");
528}
529
530inline const code_ifthenelset &to_code_ifthenelse(const codet &code)
531{
533 const code_ifthenelset &ret = static_cast<const code_ifthenelset &>(code);
535 return ret;
536}
537
539{
541 code_ifthenelset &ret = static_cast<code_ifthenelset &>(code);
543 return ret;
544}
545
547class code_switcht:public codet
548{
549public:
551 : codet(ID_switch, {std::move(_value), std::move(_body)})
552 {
553 }
554
555 const exprt &value() const
556 {
557 return op0();
558 }
559
561 {
562 return op0();
563 }
564
565 const codet &body() const
566 {
567 return to_code(op1());
568 }
569
571 {
572 return static_cast<codet &>(op1());
573 }
574
575protected:
576 using codet::op0;
577 using codet::op1;
578 using codet::op2;
579 using codet::op3;
580};
581
582template<> inline bool can_cast_expr<code_switcht>(const exprt &base)
583{
585}
586
587inline void validate_expr(const code_switcht &x)
588{
589 validate_operands(x, 2, "switch must have two operands");
590}
591
592inline const code_switcht &to_code_switch(const codet &code)
593{
595 const code_switcht &ret = static_cast<const code_switcht &>(code);
597 return ret;
598}
599
601{
603 code_switcht &ret = static_cast<code_switcht &>(code);
605 return ret;
606}
607
609class code_whilet:public codet
610{
611public:
613 : codet(ID_while, {std::move(_cond), std::move(_body)})
614 {
615 }
616
617 const exprt &cond() const
618 {
619 return op0();
620 }
621
623 {
624 return op0();
625 }
626
627 const codet &body() const
628 {
629 return to_code(op1());
630 }
631
633 {
634 return static_cast<codet &>(op1());
635 }
636
637protected:
638 using codet::op0;
639 using codet::op1;
640 using codet::op2;
641 using codet::op3;
642};
643
644template<> inline bool can_cast_expr<code_whilet>(const exprt &base)
645{
647}
648
649inline void validate_expr(const code_whilet &x)
650{
651 validate_operands(x, 2, "while must have two operands");
652}
653
654inline const code_whilet &to_code_while(const codet &code)
655{
657 const code_whilet &ret = static_cast<const code_whilet &>(code);
659 return ret;
660}
661
663{
665 code_whilet &ret = static_cast<code_whilet &>(code);
667 return ret;
668}
669
672{
673public:
675 : codet(ID_dowhile, {std::move(_cond), std::move(_body)})
676 {
677 }
678
679 const exprt &cond() const
680 {
681 return op0();
682 }
683
685 {
686 return op0();
687 }
688
689 const codet &body() const
690 {
691 return to_code(op1());
692 }
693
695 {
696 return static_cast<codet &>(op1());
697 }
698
699protected:
700 using codet::op0;
701 using codet::op1;
702 using codet::op2;
703 using codet::op3;
704};
705
706template<> inline bool can_cast_expr<code_dowhilet>(const exprt &base)
707{
709}
710
711inline void validate_expr(const code_dowhilet &x)
712{
713 validate_operands(x, 2, "do-while must have two operands");
714}
715
716inline const code_dowhilet &to_code_dowhile(const codet &code)
717{
719 const code_dowhilet &ret = static_cast<const code_dowhilet &>(code);
721 return ret;
722}
723
725{
727 code_dowhilet &ret = static_cast<code_dowhilet &>(code);
729 return ret;
730}
731
733class code_fort:public codet
734{
735public:
739 : codet(
740 ID_for,
741 {std::move(_init),
742 std::move(_cond),
743 std::move(_iter),
744 std::move(_body)})
745 {
746 }
747
748 // nil or a statement
749 const exprt &init() const
750 {
751 return op0();
752 }
753
755 {
756 return op0();
757 }
758
759 const exprt &cond() const
760 {
761 return op1();
762 }
763
765 {
766 return op1();
767 }
768
769 const exprt &iter() const
770 {
771 return op2();
772 }
773
775 {
776 return op2();
777 }
778
779 const codet &body() const
780 {
781 return to_code(op3());
782 }
783
785 {
786 return static_cast<codet &>(op3());
787 }
788
803 codet body,
804 source_locationt location);
805
806protected:
807 using codet::op0;
808 using codet::op1;
809 using codet::op2;
810 using codet::op3;
811};
812
813template<> inline bool can_cast_expr<code_fort>(const exprt &base)
814{
816}
817
818inline void validate_expr(const code_fort &x)
819{
820 validate_operands(x, 4, "for must have four operands");
821}
822
823inline const code_fort &to_code_for(const codet &code)
824{
826 const code_fort &ret = static_cast<const code_fort &>(code);
828 return ret;
829}
830
832{
834 code_fort &ret = static_cast<code_fort &>(code);
836 return ret;
837}
838
840class code_gotot:public codet
841{
842public:
843 explicit code_gotot(const irep_idt &label):codet(ID_goto)
844 {
845 set_destination(label);
846 }
847
848 void set_destination(const irep_idt &label)
849 {
850 set(ID_destination, label);
851 }
852
854 {
855 return get(ID_destination);
856 }
857
858protected:
859 using codet::op0;
860 using codet::op1;
861 using codet::op2;
862 using codet::op3;
863};
864
865template<> inline bool can_cast_expr<code_gotot>(const exprt &base)
866{
868}
869
870inline void validate_expr(const code_gotot &x)
871{
872 validate_operands(x, 0, "goto must not have operands");
873}
874
875inline const code_gotot &to_code_goto(const codet &code)
876{
878 const code_gotot &ret = static_cast<const code_gotot &>(code);
880 return ret;
881}
882
884{
886 code_gotot &ret = static_cast<code_gotot &>(code);
888 return ret;
889}
890
893{
894public:
898
900 {
901 }
902
903 const exprt &return_value() const
904 {
905 return op0();
906 }
907
909 {
910 return op0();
911 }
912
913 bool has_return_value() const
914 {
915 return return_value().is_not_nil();
916 }
917
918 static void check(
919 const codet &code,
921 {
922 DATA_CHECK(vm, code.operands().size() == 1, "return must have one operand");
923 }
924
925protected:
926 using codet::op0;
927 using codet::op1;
928 using codet::op2;
929 using codet::op3;
930};
931
932template <>
934{
936}
937
942
944{
947 return static_cast<const code_frontend_returnt &>(code);
948}
949
951{
954 return static_cast<code_frontend_returnt &>(code);
955}
956
958class code_labelt:public codet
959{
960public:
962 : codet(ID_label, {std::move(_code)})
963 {
965 }
966
967 const irep_idt &get_label() const
968 {
969 return get(ID_label);
970 }
971
972 void set_label(const irep_idt &label)
973 {
974 set(ID_label, label);
975 }
976
978 {
979 return static_cast<codet &>(op0());
980 }
981
982 const codet &code() const
983 {
984 return static_cast<const codet &>(op0());
985 }
986
987protected:
988 using codet::op0;
989 using codet::op1;
990 using codet::op2;
991 using codet::op3;
992};
993
994template<> inline bool can_cast_expr<code_labelt>(const exprt &base)
995{
997}
998
999inline void validate_expr(const code_labelt &x)
1000{
1001 validate_operands(x, 1, "label must have one operand");
1002}
1003
1004inline const code_labelt &to_code_label(const codet &code)
1005{
1007 const code_labelt &ret = static_cast<const code_labelt &>(code);
1009 return ret;
1010}
1011
1013{
1015 code_labelt &ret = static_cast<code_labelt &>(code);
1017 return ret;
1018}
1019
1023{
1024public:
1026 : codet(ID_switch_case, {std::move(_case_op), std::move(_code)})
1027 {
1028 }
1029
1030 bool is_default() const
1031 {
1032 return get_bool(ID_default);
1033 }
1034
1036 {
1037 return set(ID_default, true);
1038 }
1039
1040 const exprt &case_op() const
1041 {
1042 return op0();
1043 }
1044
1046 {
1047 return op0();
1048 }
1049
1051 {
1052 return static_cast<codet &>(op1());
1053 }
1054
1055 const codet &code() const
1056 {
1057 return static_cast<const codet &>(op1());
1058 }
1059
1060protected:
1061 using codet::op0;
1062 using codet::op1;
1063 using codet::op2;
1064 using codet::op3;
1065};
1066
1067template<> inline bool can_cast_expr<code_switch_caset>(const exprt &base)
1068{
1070}
1071
1073{
1074 validate_operands(x, 2, "switch-case must have two operands");
1075}
1076
1078{
1080 const code_switch_caset &ret = static_cast<const code_switch_caset &>(code);
1082 return ret;
1083}
1084
1086{
1088 code_switch_caset &ret = static_cast<code_switch_caset &>(code);
1090 return ret;
1091}
1092
1097{
1098public:
1100 : codet(
1102 {std::move(_lower), std::move(_upper), std::move(_code)})
1103 {
1104 }
1105
1107 const exprt &lower() const
1108 {
1109 return op0();
1110 }
1111
1114 {
1115 return op0();
1116 }
1117
1119 const exprt &upper() const
1120 {
1121 return op1();
1122 }
1123
1126 {
1127 return op1();
1128 }
1129
1132 {
1133 return static_cast<codet &>(op2());
1134 }
1135
1137 const codet &code() const
1138 {
1139 return static_cast<const codet &>(op2());
1140 }
1141
1142protected:
1143 using codet::op0;
1144 using codet::op1;
1145 using codet::op2;
1146 using codet::op3;
1147};
1148
1149template <>
1154
1156{
1157 validate_operands(x, 3, "gcc-switch-case-range must have three operands");
1158}
1159
1160inline const code_gcc_switch_case_ranget &
1162{
1165 static_cast<const code_gcc_switch_case_ranget &>(code);
1167 return ret;
1168}
1169
1178
1181class code_breakt:public codet
1182{
1183public:
1185 {
1186 }
1187
1188protected:
1189 using codet::op0;
1190 using codet::op1;
1191 using codet::op2;
1192 using codet::op3;
1193};
1194
1195template<> inline bool can_cast_expr<code_breakt>(const exprt &base)
1196{
1198}
1199
1200// to_code_break only checks the code statement, so no validate_expr is
1201// provided for code_breakt
1202
1203inline const code_breakt &to_code_break(const codet &code)
1204{
1206 return static_cast<const code_breakt &>(code);
1207}
1208
1210{
1212 return static_cast<code_breakt &>(code);
1213}
1214
1218{
1219public:
1223
1224protected:
1225 using codet::op0;
1226 using codet::op1;
1227 using codet::op2;
1228 using codet::op3;
1229};
1230
1231template<> inline bool can_cast_expr<code_continuet>(const exprt &base)
1232{
1234}
1235
1236// to_code_continue only checks the code statement, so no validate_expr is
1237// provided for code_continuet
1238
1239inline const code_continuet &to_code_continue(const codet &code)
1240{
1242 return static_cast<const code_continuet &>(code);
1243}
1244
1246{
1248 return static_cast<code_continuet &>(code);
1249}
1250
1252class code_asmt:public codet
1253{
1254public:
1256 {
1257 }
1258
1259 explicit code_asmt(exprt expr) : codet(ID_asm, {std::move(expr)})
1260 {
1261 }
1262
1263 const irep_idt &get_flavor() const
1264 {
1265 return get(ID_flavor);
1266 }
1267
1268 void set_flavor(const irep_idt &f)
1269 {
1270 set(ID_flavor, f);
1271 }
1272};
1273
1274template<> inline bool can_cast_expr<code_asmt>(const exprt &base)
1275{
1276 return detail::can_cast_code_impl(base, ID_asm);
1277}
1278
1279// to_code_asm only checks the code statement, so no validate_expr is
1280// provided for code_asmt
1281
1283{
1285 return static_cast<code_asmt &>(code);
1286}
1287
1288inline const code_asmt &to_code_asm(const codet &code)
1289{
1291 return static_cast<const code_asmt &>(code);
1292}
1293
1297{
1298public:
1300 {
1302 operands().resize(5);
1303 }
1304
1306 {
1307 return op0();
1308 }
1309
1310 const exprt &asm_text() const
1311 {
1312 return op0();
1313 }
1314
1316 {
1317 return op1();
1318 }
1319
1320 const exprt &outputs() const
1321 {
1322 return op1();
1323 }
1324
1326 {
1327 return op2();
1328 }
1329
1330 const exprt &inputs() const
1331 {
1332 return op2();
1333 }
1334
1336 {
1337 return op3();
1338 }
1339
1340 const exprt &clobbers() const
1341 {
1342 return op3();
1343 }
1344
1346 {
1347 return operands()[4];
1348 }
1349
1350 const exprt &labels() const
1351 {
1352 return operands()[4];
1353 }
1354
1355protected:
1356 using code_asmt::op0;
1357 using code_asmt::op1;
1358 using code_asmt::op2;
1359 using code_asmt::op3;
1360};
1361
1362template <>
1363inline bool can_cast_expr<code_asm_gcct>(const exprt &base)
1364{
1365 return detail::can_cast_code_impl(base, ID_asm);
1366}
1367
1368inline void validate_expr(const code_asm_gcct &x)
1369{
1370 validate_operands(x, 5, "code_asm_gcc must have five operands");
1371}
1372
1374{
1376 PRECONDITION(to_code_asm(code).get_flavor() == ID_gcc);
1377 code_asm_gcct &ret = static_cast<code_asm_gcct &>(code);
1379 return ret;
1380}
1381
1382inline const code_asm_gcct &to_code_asm_gcc(const codet &code)
1383{
1385 PRECONDITION(to_code_asm(code).get_flavor() == ID_gcc);
1386 const code_asm_gcct &ret = static_cast<const code_asm_gcct &>(code);
1388 return ret;
1389}
1390
1394{
1395public:
1397 : codet(ID_expression, {std::move(expr)})
1398 {
1399 }
1400
1401 const exprt &expression() const
1402 {
1403 return op0();
1404 }
1405
1407 {
1408 return op0();
1409 }
1410
1411protected:
1412 using codet::op0;
1413 using codet::op1;
1414 using codet::op2;
1415 using codet::op3;
1416};
1417
1418template<> inline bool can_cast_expr<code_expressiont>(const exprt &base)
1419{
1421}
1422
1424{
1425 validate_operands(x, 1, "expression statement must have one operand");
1426}
1427
1429{
1431 code_expressiont &ret = static_cast<code_expressiont &>(code);
1433 return ret;
1434}
1435
1437{
1439 const code_expressiont &ret = static_cast<const code_expressiont &>(code);
1441 return ret;
1442}
1443
1450{
1451public:
1453 const irep_idt &statement,
1455 typet _type,
1456 source_locationt loc)
1457 : exprt(ID_side_effect, std::move(_type), std::move(loc))
1458 {
1459 set_statement(statement);
1460 operands() = std::move(_operands);
1461 }
1462
1464 const irep_idt &statement,
1465 typet _type,
1466 source_locationt loc)
1467 : exprt(ID_side_effect, std::move(_type), std::move(loc))
1468 {
1469 set_statement(statement);
1470 }
1471
1473 {
1474 return get(ID_statement);
1475 }
1476
1477 void set_statement(const irep_idt &statement)
1478 {
1479 return set(ID_statement, statement);
1480 }
1481};
1482
1483namespace detail // NOLINT
1484{
1485
1486template<typename Tag>
1487inline bool can_cast_side_effect_expr_impl(const exprt &expr, const Tag &tag)
1488{
1489 if(const auto ptr = expr_try_dynamic_cast<side_effect_exprt>(expr))
1490 {
1491 return ptr->get_statement() == tag;
1492 }
1493 return false;
1494}
1495
1496} // namespace detail
1497
1498template<> inline bool can_cast_expr<side_effect_exprt>(const exprt &base)
1499{
1500 return base.id()==ID_side_effect;
1501}
1502
1503// to_side_effect_expr only checks the id, so no validate_expr is provided for
1504// side_effect_exprt
1505
1507{
1508 PRECONDITION(expr.id() == ID_side_effect);
1509 return static_cast<side_effect_exprt &>(expr);
1510}
1511
1513{
1514 PRECONDITION(expr.id() == ID_side_effect);
1515 return static_cast<const side_effect_exprt &>(expr);
1516}
1517
1520{
1521public:
1523 : side_effect_exprt(ID_nondet, std::move(_type), std::move(loc))
1524 {
1525 set_nullable(true);
1526 }
1527
1529 {
1531 }
1532
1533 bool get_nullable() const
1534 {
1536 }
1537};
1538
1539template<>
1544
1545// to_side_effect_expr_nondet only checks the id, so no validate_expr is
1546// provided for side_effect_expr_nondett
1547
1554
1556 const exprt &expr)
1557{
1560 return static_cast<const side_effect_expr_nondett &>(side_effect_expr_nondet);
1561}
1562
1565{
1566public:
1570 const exprt &_lhs,
1571 const exprt &_rhs,
1572 const source_locationt &loc)
1573 : side_effect_exprt(ID_assign, {_lhs, _rhs}, _lhs.type(), loc)
1574 {
1575 }
1576
1579 exprt _lhs,
1580 exprt _rhs,
1581 typet _type,
1582 source_locationt loc)
1584 ID_assign,
1585 {std::move(_lhs), std::move(_rhs)},
1586 std::move(_type),
1587 std::move(loc))
1588 {
1589 }
1590
1592 {
1593 return op0();
1594 }
1595
1596 const exprt &lhs() const
1597 {
1598 return op0();
1599 }
1600
1602 {
1603 return op1();
1604 }
1605
1606 const exprt &rhs() const
1607 {
1608 return op1();
1609 }
1610};
1611
1612template <>
1617
1624
1625inline const side_effect_expr_assignt &
1627{
1628 const auto &side_effect_expr_assign = to_side_effect_expr(expr);
1630 return static_cast<const side_effect_expr_assignt &>(side_effect_expr_assign);
1631}
1632
1635{
1636public:
1639 codet _code,
1640 typet _type,
1641 source_locationt loc)
1644 {std::move(_code)},
1645 std::move(_type),
1646 std::move(loc))
1647 {
1648 }
1649
1651 {
1652 return to_code(op0());
1653 }
1654
1655 const codet &statement() const
1656 {
1657 return to_code(op0());
1658 }
1659};
1660
1661template <>
1667
1678
1689
1692{
1693public:
1697 typet _type,
1698 source_locationt loc)
1701 {std::move(_function),
1703 std::move(_type),
1704 std::move(loc))
1705 {
1706 }
1707
1709 {
1710 return op0();
1711 }
1712
1713 const exprt &function() const
1714 {
1715 return op0();
1716 }
1717
1719 {
1720 return op1().operands();
1721 }
1722
1724 {
1725 return op1().operands();
1726 }
1727};
1728
1729template<>
1734
1735// to_side_effect_expr_function_call only checks the id, so no validate_expr is
1736// provided for side_effect_expr_function_callt
1737
1740{
1741 PRECONDITION(expr.id() == ID_side_effect);
1743 return static_cast<side_effect_expr_function_callt &>(expr);
1744}
1745
1748{
1749 PRECONDITION(expr.id() == ID_side_effect);
1751 return static_cast<const side_effect_expr_function_callt &>(expr);
1752}
1753
1757{
1758public:
1760 irept exception_list,
1761 typet type,
1762 source_locationt loc)
1763 : side_effect_exprt(ID_throw, std::move(type), std::move(loc))
1764 {
1765 set(ID_exception_list, std::move(exception_list));
1766 }
1767};
1768
1769template<>
1774
1775// to_side_effect_expr_throw only checks the id, so no validate_expr is
1776// provided for side_effect_expr_throwt
1777
1779{
1780 PRECONDITION(expr.id() == ID_side_effect);
1782 return static_cast<side_effect_expr_throwt &>(expr);
1783}
1784
1786 const exprt &expr)
1787{
1788 PRECONDITION(expr.id() == ID_side_effect);
1790 return static_cast<const side_effect_expr_throwt &>(expr);
1791}
1792
1805{
1806public:
1811
1813 {
1814 public:
1816 {
1817 }
1818
1819 explicit exception_list_entryt(const irep_idt &tag)
1820 {
1821 set(ID_tag, tag);
1822 }
1823
1824 exception_list_entryt(const irep_idt &tag, const irep_idt &label)
1825 {
1826 set(ID_tag, tag);
1827 set(ID_label, label);
1828 }
1829
1830 void set_tag(const irep_idt &tag)
1831 {
1832 set(ID_tag, tag);
1833 }
1834
1835 const irep_idt &get_tag() const {
1836 return get(ID_tag);
1837 }
1838
1839 void set_label(const irep_idt &label)
1840 {
1841 set(ID_label, label);
1842 }
1843
1844 const irep_idt &get_label() const {
1845 return get(ID_label);
1846 }
1847 };
1848
1849 typedef std::vector<exception_list_entryt> exception_listt;
1850
1852 const irep_idt &tag,
1853 const irep_idt &label):
1855 {
1857 exception_list().push_back(exception_list_entryt(tag, label));
1858 }
1859
1863
1865 return (const exception_listt &)find(ID_exception_list).get_sub();
1866 }
1867
1868protected:
1869 using codet::op0;
1870 using codet::op1;
1871 using codet::op2;
1872 using codet::op3;
1873};
1874
1875template<> inline bool can_cast_expr<code_push_catcht>(const exprt &base)
1876{
1878}
1879
1880// to_code_push_catch only checks the code statement, so no validate_expr is
1881// provided for code_push_catcht
1882
1884{
1886 return static_cast<code_push_catcht &>(code);
1887}
1888
1889static inline const code_push_catcht &to_code_push_catch(const codet &code)
1890{
1892 return static_cast<const code_push_catcht &>(code);
1893}
1894
1899{
1900public:
1904
1905protected:
1906 using codet::op0;
1907 using codet::op1;
1908 using codet::op2;
1909 using codet::op3;
1910};
1911
1912template<> inline bool can_cast_expr<code_pop_catcht>(const exprt &base)
1913{
1915}
1916
1917// to_code_pop_catch only checks the code statement, so no validate_expr is
1918// provided for code_pop_catcht
1919
1921{
1923 return static_cast<code_pop_catcht &>(code);
1924}
1925
1926static inline const code_pop_catcht &to_code_pop_catch(const codet &code)
1927{
1929 return static_cast<const code_pop_catcht &>(code);
1930}
1931
1936{
1937 public:
1939 {
1940 operands().resize(1);
1941 }
1942
1945 {
1946 }
1947
1948 const exprt &catch_expr() const
1949 {
1950 return op0();
1951 }
1953 {
1954 return op0();
1955 }
1956
1957protected:
1958 using codet::op0;
1959 using codet::op1;
1960 using codet::op2;
1961 using codet::op3;
1962};
1963
1964template<> inline bool can_cast_expr<code_landingpadt>(const exprt &base)
1965{
1967}
1968
1969// to_code_landingpad only checks the code statement, so no validate_expr is
1970// provided for code_landingpadt
1971
1973{
1975 return static_cast<code_landingpadt &>(code);
1976}
1977
1978static inline const code_landingpadt &to_code_landingpad(const codet &code)
1979{
1981 return static_cast<const code_landingpadt &>(code);
1982}
1983
1986{
1987public:
1990 : codet(ID_try_catch, {std::move(_try_code)})
1991 {
1992 }
1993
1995 {
1996 return static_cast<codet &>(op0());
1997 }
1998
1999 const codet &try_code() const
2000 {
2001 return static_cast<const codet &>(op0());
2002 }
2003
2005 {
2006 PRECONDITION((2 * i + 2) < operands().size());
2007 return to_code_frontend_decl(to_code(operands()[2 * i + 1]));
2008 }
2009
2010 const code_frontend_declt &get_catch_decl(unsigned i) const
2011 {
2012 PRECONDITION((2 * i + 2) < operands().size());
2013 return to_code_frontend_decl(to_code(operands()[2 * i + 1]));
2014 }
2015
2017 {
2018 PRECONDITION((2 * i + 2) < operands().size());
2019 return to_code(operands()[2*i+2]);
2020 }
2021
2022 const codet &get_catch_code(unsigned i) const
2023 {
2024 PRECONDITION((2 * i + 2) < operands().size());
2025 return to_code(operands()[2*i+2]);
2026 }
2027
2029 {
2030 add_to_operands(std::move(to_catch), std::move(code_catch));
2031 }
2032
2033protected:
2034 using codet::op0;
2035 using codet::op1;
2036 using codet::op2;
2037 using codet::op3;
2038};
2039
2040template<> inline bool can_cast_expr<code_try_catcht>(const exprt &base)
2041{
2043}
2044
2046{
2047 validate_operands(x, 3, "try-catch must have three or more operands", true);
2048}
2049
2050inline const code_try_catcht &to_code_try_catch(const codet &code)
2051{
2053 const code_try_catcht &ret = static_cast<const code_try_catcht &>(code);
2055 return ret;
2056}
2057
2059{
2061 code_try_catcht &ret = static_cast<code_try_catcht &>(code);
2063 return ret;
2064}
2065
2070{
2071public:
2073 const std::vector<irep_idt> &parameter_identifiers,
2075 : codet(ID_function_body, {std::move(_block)})
2076 {
2077 set_parameter_identifiers(parameter_identifiers);
2078 }
2079
2081 {
2082 return to_code_block(to_code(op0()));
2083 }
2084
2085 const code_blockt &block() const
2086 {
2087 return to_code_block(to_code(op0()));
2088 }
2089
2090 std::vector<irep_idt> get_parameter_identifiers() const;
2091 void set_parameter_identifiers(const std::vector<irep_idt> &);
2092
2093protected:
2094 using codet::op0;
2095 using codet::op1;
2096 using codet::op2;
2097 using codet::op3;
2098};
2099
2101{
2104 code.operands().size() == 1, "code_function_body must have one operand");
2105 return static_cast<const code_function_bodyt &>(code);
2106}
2107
2109{
2112 code.operands().size() == 1, "code_function_body must have one operand");
2113 return static_cast<code_function_bodyt &>(code);
2114}
2115
2116#endif // CPROVER_UTIL_STD_CODE_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
codet representation of an inline assembler statement, for the gcc flavor.
Definition std_code.h:1297
const exprt & asm_text() const
Definition std_code.h:1310
const exprt & labels() const
Definition std_code.h:1350
exprt & asm_text()
Definition std_code.h:1305
exprt & outputs()
Definition std_code.h:1315
const exprt & outputs() const
Definition std_code.h:1320
const exprt & inputs() const
Definition std_code.h:1330
exprt & clobbers()
Definition std_code.h:1335
exprt & inputs()
Definition std_code.h:1325
exprt & labels()
Definition std_code.h:1345
const exprt & clobbers() const
Definition std_code.h:1340
codet representation of an inline assembler statement.
Definition std_code.h:1253
code_asmt(exprt expr)
Definition std_code.h:1259
const irep_idt & get_flavor() const
Definition std_code.h:1263
void set_flavor(const irep_idt &f)
Definition std_code.h:1268
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition std_code.h:270
const exprt & assertion() const
Definition std_code.h:276
code_assertt(exprt expr)
Definition std_code.h:272
exprt & assertion()
Definition std_code.h:281
An assumption, which must hold in subsequent code.
Definition std_code.h:217
code_assumet(exprt expr)
Definition std_code.h:219
exprt & assumption()
Definition std_code.h:228
const exprt & assumption() const
Definition std_code.h:223
A codet representing sequential composition of program statements.
Definition std_code.h:130
static code_blockt from_list(const std::list< codet > &_list)
Definition std_code.h:148
code_operandst & statements()
Definition std_code.h:138
source_locationt end_location() const
Definition std_code.h:187
void add(codet code, source_locationt loc)
Definition std_code.h:178
void add(codet &&code)
Definition std_code.h:173
code_blockt(std::vector< codet > &&_statements)
Definition std_code.h:163
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition std_code.cpp:86
code_blockt(const std::vector< codet > &_statements)
Definition std_code.h:158
void add(const codet &code)
Definition std_code.h:168
const code_operandst & statements() const
Definition std_code.h:143
std::vector< codet > code_operandst
Definition std_code.h:136
codet & find_last_statement()
Definition std_code.cpp:96
codet representation of a break statement (within a for or while loop).
Definition std_code.h:1182
codet representation of a continue statement (within a for or while loop).
Definition std_code.h:1218
codet representation of a do while statement.
Definition std_code.h:672
code_dowhilet(exprt _cond, codet _body)
Definition std_code.h:674
exprt & cond()
Definition std_code.h:684
const codet & body() const
Definition std_code.h:689
const exprt & cond() const
Definition std_code.h:679
codet & body()
Definition std_code.h:694
codet representation of an expression statement.
Definition std_code.h:1394
code_expressiont(exprt expr)
Definition std_code.h:1396
exprt & expression()
Definition std_code.h:1406
const exprt & expression() const
Definition std_code.h:1401
codet representation of a for statement.
Definition std_code.h:734
exprt & init()
Definition std_code.h:754
exprt & iter()
Definition std_code.h:774
const exprt & cond() const
Definition std_code.h:759
code_fort(exprt _init, exprt _cond, exprt _iter, codet _body)
A statement describing a for loop with initializer _init, loop condition _cond, increment _iter,...
Definition std_code.h:738
codet & body()
Definition std_code.h:784
static code_fort from_index_bounds(exprt start_index, exprt end_index, symbol_exprt loop_index, codet body, source_locationt location)
Produce a code_fort representing:
Definition std_code.cpp:155
const exprt & iter() const
Definition std_code.h:769
const codet & body() const
Definition std_code.h:779
exprt & cond()
Definition std_code.h:764
const exprt & init() const
Definition std_code.h:749
A codet representing an assignment in the program.
Definition std_code.h:24
static void validate(const codet &code, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition std_code.h:69
static void validate_full(const codet &code, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition std_code.h:82
code_frontend_assignt(exprt lhs, exprt rhs)
Definition std_code.h:31
const exprt & lhs() const
Definition std_code.h:51
const exprt & rhs() const
Definition std_code.h:56
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
Definition std_code.h:61
code_frontend_assignt(exprt lhs, exprt rhs, source_locationt loc)
Definition std_code.h:36
A codet representing the declaration of a local variable.
Definition std_code.h:347
code_frontend_declt(symbol_exprt symbol)
Definition std_code.h:349
symbol_exprt & symbol()
Definition std_code.h:354
const symbol_exprt & symbol() const
Definition std_code.h:359
void set_initial_value(std::optional< exprt > initial_value)
Sets the value to which this declaration initializes the declared variable.
Definition std_code.h:384
std::optional< exprt > initial_value() const
Returns the initial value to which the declared variable is initialized, or empty in the case where n...
Definition std_code.h:373
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
Definition std_code.h:401
const irep_idt & get_identifier() const
Definition std_code.h:364
codet representation of a "return from a function" statement.
Definition std_code.h:893
const exprt & return_value() const
Definition std_code.h:903
exprt & return_value()
Definition std_code.h:908
bool has_return_value() const
Definition std_code.h:913
code_frontend_returnt(exprt _op)
Definition std_code.h:899
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
Definition std_code.h:918
This class is used to interface between a language frontend and goto-convert – it communicates the id...
Definition std_code.h:2070
code_function_bodyt(const std::vector< irep_idt > &parameter_identifiers, code_blockt _block)
Definition std_code.h:2072
std::vector< irep_idt > get_parameter_identifiers() const
Definition std_code.cpp:133
code_blockt & block()
Definition std_code.h:2080
const code_blockt & block() const
Definition std_code.h:2085
void set_parameter_identifiers(const std::vector< irep_idt > &)
Definition std_code.cpp:143
codet representation of a switch-case, i.e. a case statement within a switch.
Definition std_code.h:1097
const codet & code() const
the statement to be executed when the case applies
Definition std_code.h:1137
const exprt & upper() const
upper bound of range
Definition std_code.h:1119
code_gcc_switch_case_ranget(exprt _lower, exprt _upper, codet _code)
Definition std_code.h:1099
const exprt & lower() const
lower bound of range
Definition std_code.h:1107
exprt & lower()
lower bound of range
Definition std_code.h:1113
exprt & upper()
upper bound of range
Definition std_code.h:1125
codet & code()
the statement to be executed when the case applies
Definition std_code.h:1131
codet representation of a goto statement.
Definition std_code.h:841
const irep_idt & get_destination() const
Definition std_code.h:853
code_gotot(const irep_idt &label)
Definition std_code.h:843
void set_destination(const irep_idt &label)
Definition std_code.h:848
codet representation of an if-then-else statement.
Definition std_code.h:460
code_ifthenelset(exprt condition, codet then_code)
An if condition then then_code statement (no "else" case).
Definition std_code.h:471
const exprt & cond() const
Definition std_code.h:478
codet & then_case()
Definition std_code.h:503
const codet & else_case() const
Definition std_code.h:498
const codet & then_case() const
Definition std_code.h:488
codet & else_case()
Definition std_code.h:508
exprt & cond()
Definition std_code.h:483
code_ifthenelset(exprt condition, codet then_code, codet else_code)
An if condition then then_code else else_code statement.
Definition std_code.h:463
bool has_else_case() const
Definition std_code.h:493
codet representation of a label for branch targets.
Definition std_code.h:959
const irep_idt & get_label() const
Definition std_code.h:967
code_labelt(const irep_idt &_label, codet _code)
Definition std_code.h:961
const codet & code() const
Definition std_code.h:982
codet & code()
Definition std_code.h:977
void set_label(const irep_idt &label)
Definition std_code.h:972
A statement that catches an exception, assigning the exception in flight to an expression (e....
Definition std_code.h:1936
const exprt & catch_expr() const
Definition std_code.h:1948
code_landingpadt(exprt catch_expr)
Definition std_code.h:1943
exprt & catch_expr()
Definition std_code.h:1952
Pops an exception handler from the stack of active handlers (i.e.
Definition std_code.h:1899
void set_tag(const irep_idt &tag)
Definition std_code.h:1830
exception_list_entryt(const irep_idt &tag)
Definition std_code.h:1819
const irep_idt & get_label() const
Definition std_code.h:1844
exception_list_entryt(const irep_idt &tag, const irep_idt &label)
Definition std_code.h:1824
const irep_idt & get_tag() const
Definition std_code.h:1835
void set_label(const irep_idt &label)
Definition std_code.h:1839
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ....
Definition std_code.h:1805
exception_listt & exception_list()
Definition std_code.h:1860
std::vector< exception_list_entryt > exception_listt
Definition std_code.h:1849
const exception_listt & exception_list() const
Definition std_code.h:1864
code_push_catcht(const irep_idt &tag, const irep_idt &label)
Definition std_code.h:1851
A codet representing a skip statement.
Definition std_code.h:322
codet representation of a switch-case, i.e. a case statement within a switch.
Definition std_code.h:1023
exprt & case_op()
Definition std_code.h:1045
const exprt & case_op() const
Definition std_code.h:1040
code_switch_caset(exprt _case_op, codet _code)
Definition std_code.h:1025
const codet & code() const
Definition std_code.h:1055
bool is_default() const
Definition std_code.h:1030
codet representing a switch statement.
Definition std_code.h:548
code_switcht(exprt _value, codet _body)
Definition std_code.h:550
const codet & body() const
Definition std_code.h:565
const exprt & value() const
Definition std_code.h:555
codet & body()
Definition std_code.h:570
exprt & value()
Definition std_code.h:560
codet representation of a try/catch block.
Definition std_code.h:1986
const code_frontend_declt & get_catch_decl(unsigned i) const
Definition std_code.h:2010
const codet & try_code() const
Definition std_code.h:1999
codet & try_code()
Definition std_code.h:1994
code_frontend_declt & get_catch_decl(unsigned i)
Definition std_code.h:2004
code_try_catcht(codet _try_code)
A statement representing try _try_code catch ...
Definition std_code.h:1989
void add_catch(code_frontend_declt &&to_catch, codet &&code_catch)
Definition std_code.h:2028
codet & get_catch_code(unsigned i)
Definition std_code.h:2016
const codet & get_catch_code(unsigned i) const
Definition std_code.h:2022
codet representing a while statement.
Definition std_code.h:610
exprt & cond()
Definition std_code.h:622
code_whilet(exprt _cond, codet _body)
Definition std_code.h:612
const exprt & cond() const
Definition std_code.h:617
const codet & body() const
Definition std_code.h:627
codet & body()
Definition std_code.h:632
Data structure for representing an arbitrary statement in a program.
exprt & op3()
Definition expr.h:142
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
exprt & op2()
Definition expr.h:139
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:38
Base class for all expressions.
Definition expr.h:56
exprt & op3()
Definition expr.h:142
std::vector< exprt > operandst
Definition expr.h:58
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
exprt & op2()
Definition expr.h:139
source_locationt & add_source_location()
Definition expr.h:236
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:170
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:364
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
irept()=default
const irept & find(const irep_idt &name) const
Definition irep.cpp:93
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:412
bool is_not_nil() const
Definition irep.h:372
subt & get_sub()
Definition irep.h:448
void swap(irept &irep)
Definition irep.h:434
const irep_idt & id() const
Definition irep.h:388
irept & add(const irep_idt &name)
Definition irep.cpp:103
A base class for multi-ary expressions Associativity is not specified.
Definition std_expr.h:912
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The NIL expression.
Definition std_expr.h:3208
A side_effect_exprt that performs an assignment.
Definition std_code.h:1565
const exprt & rhs() const
Definition std_code.h:1606
side_effect_expr_assignt(exprt _lhs, exprt _rhs, typet _type, source_locationt loc)
construct an assignment side-effect, given lhs, rhs and the type
Definition std_code.h:1578
const exprt & lhs() const
Definition std_code.h:1596
side_effect_expr_assignt(const exprt &_lhs, const exprt &_rhs, const source_locationt &loc)
construct an assignment side-effect, given lhs and rhs The type is copied from lhs
Definition std_code.h:1569
A side_effect_exprt representation of a function call side effect.
Definition std_code.h:1692
side_effect_expr_function_callt(exprt _function, exprt::operandst _arguments, typet _type, source_locationt loc)
Definition std_code.h:1694
const exprt::operandst & arguments() const
Definition std_code.h:1723
exprt::operandst & arguments()
Definition std_code.h:1718
const exprt & function() const
Definition std_code.h:1713
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
void set_nullable(bool nullable)
Definition std_code.h:1528
bool get_nullable() const
Definition std_code.h:1533
side_effect_expr_nondett(typet _type, source_locationt loc)
Definition std_code.h:1522
A side_effect_exprt that contains a statement.
Definition std_code.h:1635
side_effect_expr_statement_expressiont(codet _code, typet _type, source_locationt loc)
construct an assignment side-effect, given lhs, rhs and the type
Definition std_code.h:1638
A side_effect_exprt representation of a side effect that throws an exception.
Definition std_code.h:1757
side_effect_expr_throwt(irept exception_list, typet type, source_locationt loc)
Definition std_code.h:1759
An expression containing a side effect.
Definition std_code.h:1450
void set_statement(const irep_idt &statement)
Definition std_code.h:1477
const irep_idt & get_statement() const
Definition std_code.h:1472
side_effect_exprt(const irep_idt &statement, operandst _operands, typet _type, source_locationt loc)
Definition std_code.h:1452
side_effect_exprt(const irep_idt &statement, typet _type, source_locationt loc)
Definition std_code.h:1463
Expression to hold a symbol (variable)
Definition std_expr.h:131
const irep_idt & get_identifier() const
Definition std_expr.h:160
The type of an expression, extends irept.
Definition type.h:29
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition expr_cast.h:250
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
bool can_cast_code_impl(const exprt &expr, const Tag &tag)
bool can_cast_side_effect_expr_impl(const exprt &expr, const Tag &tag)
Definition std_code.h:1487
STL namespace.
#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
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition std_code.h:1506
code_blockt create_fatal_assertion(const exprt &condition, const source_locationt &source_location)
Create a fatal assertion, which checks a condition and then halts if it does not hold.
Definition std_code.cpp:120
bool can_cast_expr< side_effect_expr_throwt >(const exprt &base)
Definition std_code.h:1770
bool can_cast_expr< code_ifthenelset >(const exprt &base)
Definition std_code.h:520
bool can_cast_expr< code_switcht >(const exprt &base)
Definition std_code.h:582
const code_breakt & to_code_break(const codet &code)
Definition std_code.h:1203
const code_switch_caset & to_code_switch_case(const codet &code)
Definition std_code.h:1077
bool can_cast_expr< code_switch_caset >(const exprt &base)
Definition std_code.h:1067
bool can_cast_expr< code_asmt >(const exprt &base)
Definition std_code.h:1274
const code_function_bodyt & to_code_function_body(const codet &code)
Definition std_code.h:2100
bool can_cast_expr< code_expressiont >(const exprt &base)
Definition std_code.h:1418
bool can_cast_expr< code_landingpadt >(const exprt &base)
Definition std_code.h:1964
bool can_cast_expr< code_frontend_assignt >(const exprt &base)
Definition std_code.h:103
const code_gotot & to_code_goto(const codet &code)
Definition std_code.h:875
const code_assertt & to_code_assert(const codet &code)
Definition std_code.h:304
bool can_cast_expr< code_blockt >(const exprt &base)
Definition std_code.h:195
bool can_cast_expr< code_breakt >(const exprt &base)
Definition std_code.h:1195
bool can_cast_expr< side_effect_expr_nondett >(const exprt &base)
Definition std_code.h:1540
bool can_cast_expr< code_dowhilet >(const exprt &base)
Definition std_code.h:706
static code_push_catcht & to_code_push_catch(codet &code)
Definition std_code.h:1883
side_effect_expr_statement_expressiont & to_side_effect_expr_statement_expression(exprt &expr)
Definition std_code.h:1669
bool can_cast_expr< code_try_catcht >(const exprt &base)
Definition std_code.h:2040
bool can_cast_expr< code_frontend_returnt >(const exprt &base)
Definition std_code.h:933
code_asm_gcct & to_code_asm_gcc(codet &code)
Definition std_code.h:1373
static code_landingpadt & to_code_landingpad(codet &code)
Definition std_code.h:1972
const code_frontend_returnt & to_code_frontend_return(const codet &code)
Definition std_code.h:943
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition std_code.h:1739
const code_dowhilet & to_code_dowhile(const codet &code)
Definition std_code.h:716
static code_pop_catcht & to_code_pop_catch(codet &code)
Definition std_code.h:1920
side_effect_expr_nondett & to_side_effect_expr_nondet(exprt &expr)
Definition std_code.h:1548
const code_assumet & to_code_assume(const codet &code)
Definition std_code.h:251
bool can_cast_expr< code_assertt >(const exprt &base)
Definition std_code.h:294
const code_whilet & to_code_while(const codet &code)
Definition std_code.h:654
bool can_cast_expr< code_skipt >(const exprt &base)
Definition std_code.h:335
bool can_cast_expr< side_effect_expr_assignt >(const exprt &base)
Definition std_code.h:1613
bool can_cast_expr< code_asm_gcct >(const exprt &base)
Definition std_code.h:1363
bool can_cast_expr< code_frontend_declt >(const exprt &base)
Definition std_code.h:419
bool can_cast_expr< code_gotot >(const exprt &base)
Definition std_code.h:865
bool can_cast_expr< side_effect_expr_statement_expressiont >(const exprt &base)
Definition std_code.h:1663
const code_labelt & to_code_label(const codet &code)
Definition std_code.h:1004
bool can_cast_expr< side_effect_expr_function_callt >(const exprt &base)
Definition std_code.h:1730
const code_blockt & to_code_block(const codet &code)
Definition std_code.h:203
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition std_code.h:530
const code_gcc_switch_case_ranget & to_code_gcc_switch_case_range(const codet &code)
Definition std_code.h:1161
void validate_expr(const code_frontend_assignt &x)
Definition std_code.h:108
bool can_cast_expr< code_whilet >(const exprt &base)
Definition std_code.h:644
bool can_cast_expr< code_continuet >(const exprt &base)
Definition std_code.h:1231
const code_frontend_assignt & to_code_frontend_assign(const codet &code)
Definition std_code.h:113
bool can_cast_expr< side_effect_exprt >(const exprt &base)
Definition std_code.h:1498
code_asmt & to_code_asm(codet &code)
Definition std_code.h:1282
bool can_cast_expr< code_push_catcht >(const exprt &base)
Definition std_code.h:1875
side_effect_expr_assignt & to_side_effect_expr_assign(exprt &expr)
Definition std_code.h:1618
const code_fort & to_code_for(const codet &code)
Definition std_code.h:823
bool can_cast_expr< code_fort >(const exprt &base)
Definition std_code.h:813
const code_switcht & to_code_switch(const codet &code)
Definition std_code.h:592
const code_try_catcht & to_code_try_catch(const codet &code)
Definition std_code.h:2050
bool can_cast_expr< code_gcc_switch_case_ranget >(const exprt &base)
Definition std_code.h:1150
const code_frontend_declt & to_code_frontend_decl(const codet &code)
Definition std_code.h:429
code_expressiont & to_code_expression(codet &code)
Definition std_code.h:1428
bool can_cast_expr< code_labelt >(const exprt &base)
Definition std_code.h:994
bool can_cast_expr< code_pop_catcht >(const exprt &base)
Definition std_code.h:1912
side_effect_expr_throwt & to_side_effect_expr_throw(exprt &expr)
Definition std_code.h:1778
const code_continuet & to_code_continue(const codet &code)
Definition std_code.h:1239
bool can_cast_expr< code_assumet >(const exprt &base)
Definition std_code.h:241
const codet & to_code(const exprt &expr)
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition validate.h:22
void validate_full_expr(const exprt &expr, const namespacet &ns, const validation_modet vm)
Check that the given expression is well-formed (full check, including checks of all subexpressions an...
validation_modet