@@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com
2121class codet :public exprt
2222{
2323public:
24+ // deprecated, will go away
2425 codet ():exprt(ID_code, typet(ID_code))
2526 {
2627 }
@@ -253,6 +254,7 @@ inline code_assignt &to_code_assign(codet &code)
253254class code_declt :public codet
254255{
255256public:
257+ // deprecated, will go away
256258 code_declt ():codet(ID_decl)
257259 {
258260 operands ().resize (1 );
@@ -305,6 +307,7 @@ inline code_declt &to_code_decl(codet &code)
305307class code_deadt :public codet
306308{
307309public:
310+ // deprecated, will go away
308311 code_deadt ():codet(ID_dead)
309312 {
310313 operands ().resize (1 );
@@ -354,6 +357,7 @@ inline code_deadt &to_code_dead(codet &code)
354357class code_assumet :public codet
355358{
356359public:
360+ // deprecated, will go away
357361 code_assumet ():codet(ID_assume)
358362 {
359363 operands ().resize (1 );
@@ -400,6 +404,7 @@ inline code_assumet &to_code_assume(codet &code)
400404class code_assertt :public codet
401405{
402406public:
407+ // deprecated, will go away
403408 code_assertt ():codet(ID_assert)
404409 {
405410 operands ().resize (1 );
@@ -533,11 +538,19 @@ inline code_ifthenelset &to_code_ifthenelse(codet &code)
533538class code_switcht :public codet
534539{
535540public:
541+ // deprecated, will go away
536542 code_switcht ():codet(ID_switch)
537543 {
538544 operands ().resize (2 );
539545 }
540546
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+
541554 const exprt &value () const
542555 {
543556 return op0 ();
@@ -588,11 +601,19 @@ inline code_switcht &to_code_switch(codet &code)
588601class code_whilet :public codet
589602{
590603public:
604+ // deprecated, will go away
591605 code_whilet ():codet(ID_while)
592606 {
593607 operands ().resize (2 );
594608 }
595609
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+
596617 const exprt &cond () const
597618 {
598619 return op0 ();
@@ -643,11 +664,19 @@ inline code_whilet &to_code_while(codet &code)
643664class code_dowhilet :public codet
644665{
645666public:
667+ // deprecated, will go away
646668 code_dowhilet ():codet(ID_dowhile)
647669 {
648670 operands ().resize (2 );
649671 }
650672
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+
651680 const exprt &cond () const
652681 {
653682 return op0 ();
@@ -774,6 +803,7 @@ inline code_fort &to_code_for(codet &code)
774803class code_gotot :public codet
775804{
776805public:
806+ // deprecated, will go away
777807 code_gotot ():codet(ID_goto)
778808 {
779809 }
@@ -947,6 +977,7 @@ inline code_returnt &to_code_return(codet &code)
947977class code_labelt :public codet
948978{
949979public:
980+ // deprecated, will go away
950981 code_labelt ():codet(ID_label)
951982 {
952983 operands ().resize (1 );
@@ -1014,6 +1045,7 @@ inline code_labelt &to_code_label(codet &code)
10141045class code_switch_caset :public codet
10151046{
10161047public:
1048+ // deprecated, will go away
10171049 code_switch_caset ():codet(ID_switch_case)
10181050 {
10191051 operands ().resize (2 );
@@ -1188,6 +1220,7 @@ inline const code_asmt &to_code_asm(const codet &code)
11881220class code_expressiont :public codet
11891221{
11901222public:
1223+ // deprecated, will go away
11911224 code_expressiont ():codet(ID_expression)
11921225 {
11931226 operands ().resize (1 );
@@ -1238,6 +1271,7 @@ inline const code_expressiont &to_code_expression(const codet &code)
12381271class side_effect_exprt :public exprt
12391272{
12401273public:
1274+ // deprecated, will go away
12411275 explicit side_effect_exprt (const irep_idt &statement):
12421276 exprt(ID_side_effect)
12431277 {
@@ -1301,6 +1335,7 @@ inline const side_effect_exprt &to_side_effect_expr(const exprt &expr)
13011335class side_effect_expr_nondett :public side_effect_exprt
13021336{
13031337public:
1338+ // deprecated, will go away
13041339 side_effect_expr_nondett ():side_effect_exprt(ID_nondet)
13051340 {
13061341 set_nullable (true );
@@ -1352,12 +1387,23 @@ inline const side_effect_expr_nondett &to_side_effect_expr_nondet(
13521387class side_effect_expr_function_callt :public side_effect_exprt
13531388{
13541389public:
1390+ // deprecated, will go away
13551391 side_effect_expr_function_callt ():side_effect_exprt(ID_function_call)
13561392 {
13571393 operands ().resize (2 );
13581394 op1 ().id (ID_arguments);
13591395 }
13601396
1397+ side_effect_expr_function_callt (
1398+ const exprt &_function,
1399+ const exprt::operandst &_arguments):side_effect_exprt(ID_function_call)
1400+ {
1401+ operands ().resize (2 );
1402+ op1 ().id (ID_arguments);
1403+ function ()=_function;
1404+ arguments ()=_arguments;
1405+ }
1406+
13611407 exprt &function ()
13621408 {
13631409 return op0 ();
@@ -1409,6 +1455,7 @@ inline const side_effect_expr_function_callt
14091455class side_effect_expr_throwt :public side_effect_exprt
14101456{
14111457public:
1458+ // deprecated, will go away
14121459 side_effect_expr_throwt ():side_effect_exprt(ID_throw)
14131460 {
14141461 }
0 commit comments