@@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com
21
21
class codet :public exprt
22
22
{
23
23
public:
24
+ DEPRECATED (" Use codet(statement) instead" )
24
25
codet ():exprt(ID_code, typet(ID_code))
25
26
{
26
27
}
@@ -253,6 +254,7 @@ inline code_assignt &to_code_assign(codet &code)
253
254
class code_declt :public codet
254
255
{
255
256
public:
257
+ DEPRECATED (" Use code_declt(symbol) instead" )
256
258
code_declt ():codet(ID_decl)
257
259
{
258
260
operands ().resize (1 );
@@ -305,6 +307,7 @@ inline code_declt &to_code_decl(codet &code)
305
307
class code_deadt :public codet
306
308
{
307
309
public:
310
+ DEPRECATED (" Use code_deadt(symbol) instead" )
308
311
code_deadt ():codet(ID_dead)
309
312
{
310
313
operands ().resize (1 );
@@ -354,6 +357,7 @@ inline code_deadt &to_code_dead(codet &code)
354
357
class code_assumet :public codet
355
358
{
356
359
public:
360
+ DEPRECATED (" Use code_assumet(expr) instead" )
357
361
code_assumet ():codet(ID_assume)
358
362
{
359
363
operands ().resize (1 );
@@ -400,6 +404,7 @@ inline code_assumet &to_code_assume(codet &code)
400
404
class code_assertt :public codet
401
405
{
402
406
public:
407
+ DEPRECATED (" Use code_assertt(expr) instead" )
403
408
code_assertt ():codet(ID_assert)
404
409
{
405
410
operands ().resize (1 );
@@ -533,11 +538,19 @@ inline code_ifthenelset &to_code_ifthenelse(codet &code)
533
538
class code_switcht :public codet
534
539
{
535
540
public:
541
+ DEPRECATED (" Use code_switcht(value, body) instead" )
536
542
code_switcht ():codet(ID_switch)
537
543
{
538
544
operands ().resize (2 );
539
545
}
540
546
547
+ code_switcht (const exprt &_value, const codet &_body) : codet(ID_switch)
548
+ {
549
+ operands ().resize (2 );
550
+ value () = _value;
551
+ body () = _body;
552
+ }
553
+
541
554
const exprt &value () const
542
555
{
543
556
return op0 ();
@@ -588,11 +601,19 @@ inline code_switcht &to_code_switch(codet &code)
588
601
class code_whilet :public codet
589
602
{
590
603
public:
604
+ DEPRECATED (" Use code_whilet(cond, body) instead" )
591
605
code_whilet ():codet(ID_while)
592
606
{
593
607
operands ().resize (2 );
594
608
}
595
609
610
+ code_whilet (const exprt &_cond, const codet &_body) : codet(ID_while)
611
+ {
612
+ operands ().resize (2 );
613
+ cond () = _cond;
614
+ body () = _body;
615
+ }
616
+
596
617
const exprt &cond () const
597
618
{
598
619
return op0 ();
@@ -643,11 +664,19 @@ inline code_whilet &to_code_while(codet &code)
643
664
class code_dowhilet :public codet
644
665
{
645
666
public:
667
+ DEPRECATED (" Use code_dowhilet(cond, body) instead" )
646
668
code_dowhilet ():codet(ID_dowhile)
647
669
{
648
670
operands ().resize (2 );
649
671
}
650
672
673
+ code_dowhilet (const exprt &_cond, const codet &_body) : codet(ID_dowhile)
674
+ {
675
+ operands ().resize (2 );
676
+ cond () = _cond;
677
+ body () = _body;
678
+ }
679
+
651
680
const exprt &cond () const
652
681
{
653
682
return op0 ();
@@ -774,6 +803,7 @@ inline code_fort &to_code_for(codet &code)
774
803
class code_gotot :public codet
775
804
{
776
805
public:
806
+ DEPRECATED (" Use code_gotot(label) instead" )
777
807
code_gotot ():codet(ID_goto)
778
808
{
779
809
}
@@ -947,6 +977,7 @@ inline code_returnt &to_code_return(codet &code)
947
977
class code_labelt :public codet
948
978
{
949
979
public:
980
+ DEPRECATED (" Use code_labelt(label) instead" )
950
981
code_labelt ():codet(ID_label)
951
982
{
952
983
operands ().resize (1 );
@@ -1014,6 +1045,7 @@ inline code_labelt &to_code_label(codet &code)
1014
1045
class code_switch_caset :public codet
1015
1046
{
1016
1047
public:
1048
+ DEPRECATED (" Use code_switch_caset(case_op, code) instead" )
1017
1049
code_switch_caset ():codet(ID_switch_case)
1018
1050
{
1019
1051
operands ().resize (2 );
@@ -1188,6 +1220,7 @@ inline const code_asmt &to_code_asm(const codet &code)
1188
1220
class code_expressiont :public codet
1189
1221
{
1190
1222
public:
1223
+ DEPRECATED (" Use code_expressiont(expr) instead" )
1191
1224
code_expressiont ():codet(ID_expression)
1192
1225
{
1193
1226
operands ().resize (1 );
@@ -1238,6 +1271,7 @@ inline const code_expressiont &to_code_expression(const codet &code)
1238
1271
class side_effect_exprt :public exprt
1239
1272
{
1240
1273
public:
1274
+ DEPRECATED (" Use side_effect_exprt(statement, type) instead" )
1241
1275
explicit side_effect_exprt (const irep_idt &statement):
1242
1276
exprt(ID_side_effect)
1243
1277
{
@@ -1301,6 +1335,7 @@ inline const side_effect_exprt &to_side_effect_expr(const exprt &expr)
1301
1335
class side_effect_expr_nondett :public side_effect_exprt
1302
1336
{
1303
1337
public:
1338
+ DEPRECATED (" Use side_effect_expr_nondett(statement, type) instead" )
1304
1339
side_effect_expr_nondett ():side_effect_exprt(ID_nondet)
1305
1340
{
1306
1341
set_nullable (true );
@@ -1352,12 +1387,36 @@ inline const side_effect_expr_nondett &to_side_effect_expr_nondet(
1352
1387
class side_effect_expr_function_callt :public side_effect_exprt
1353
1388
{
1354
1389
public:
1390
+ DEPRECATED (" Use side_effect_expr_function_callt(...) instead" )
1355
1391
side_effect_expr_function_callt ():side_effect_exprt(ID_function_call)
1356
1392
{
1357
1393
operands ().resize (2 );
1358
1394
op1 ().id (ID_arguments);
1359
1395
}
1360
1396
1397
+ side_effect_expr_function_callt (
1398
+ const exprt &_function,
1399
+ const exprt::operandst &_arguments)
1400
+ : side_effect_exprt(ID_function_call)
1401
+ {
1402
+ operands ().resize (2 );
1403
+ op1 ().id (ID_arguments);
1404
+ function () = _function;
1405
+ arguments () = _arguments;
1406
+ }
1407
+
1408
+ side_effect_expr_function_callt (
1409
+ const exprt &_function,
1410
+ const exprt::operandst &_arguments,
1411
+ const typet &_type)
1412
+ : side_effect_exprt(ID_function_call, _type)
1413
+ {
1414
+ operands ().resize (2 );
1415
+ op1 ().id (ID_arguments);
1416
+ function () = _function;
1417
+ arguments () = _arguments;
1418
+ }
1419
+
1361
1420
exprt &function ()
1362
1421
{
1363
1422
return op0 ();
@@ -1409,6 +1468,7 @@ inline const side_effect_expr_function_callt
1409
1468
class side_effect_expr_throwt :public side_effect_exprt
1410
1469
{
1411
1470
public:
1471
+ DEPRECATED (" Use side_effect_expr_throwt(exception_list) instead" )
1412
1472
side_effect_expr_throwt ():side_effect_exprt(ID_throw)
1413
1473
{
1414
1474
}
0 commit comments