File tree 1 file changed +7
-7
lines changed
1 file changed +7
-7
lines changed Original file line number Diff line number Diff line change @@ -281,8 +281,7 @@ class code_assumet:public codet
281
281
public:
282
282
inline code_assumet ():codet(ID_assume)
283
283
{
284
- // will change to resize(1) in the future
285
- reserve_operands (1 );
284
+ operands ().resize (1 );
286
285
}
287
286
288
287
inline explicit code_assumet (const exprt &expr):codet(ID_assume)
@@ -320,8 +319,7 @@ class code_assertt:public codet
320
319
public:
321
320
inline code_assertt ():codet(ID_assert)
322
321
{
323
- // will change to resize(1) in the future
324
- reserve_operands (1 );
322
+ operands ().resize (1 );
325
323
}
326
324
327
325
inline explicit code_assertt (const exprt &expr):codet(ID_assert)
@@ -723,7 +721,8 @@ class code_returnt:public codet
723
721
public:
724
722
inline code_returnt ():codet(ID_return)
725
723
{
726
- reserve_operands (1 );
724
+ operands ().resize (1 );
725
+ op0 ().make_nil ();
727
726
}
728
727
729
728
explicit inline code_returnt (const exprt &_op):codet(ID_return)
@@ -738,13 +737,14 @@ class code_returnt:public codet
738
737
739
738
inline exprt &return_value ()
740
739
{
741
- operands ().resize (1 );
742
740
return op0 ();
743
741
}
744
742
745
743
inline bool has_return_value () const
746
744
{
747
- return operands ().size ()==1 ;
745
+ if (operands ().empty ())
746
+ return false ; // backwards compatibility
747
+ return return_value ().is_not_nil ();
748
748
}
749
749
};
750
750
You can’t perform that action at this time.
0 commit comments