@@ -72,7 +72,7 @@ class java_bytecode_instrumentt:public messaget
7272 void instrument_code (exprt &expr);
7373 void add_expr_instrumentation (code_blockt &block, const exprt &expr);
7474 void prepend_instrumentation (codet &code, code_blockt &instrumentation);
75- codet instrument_expr (const exprt &expr);
75+ optionalt< codet> instrument_expr (const exprt &expr);
7676};
7777
7878const std::vector<std::string> exception_needed_classes = { // NOLINT
@@ -328,13 +328,12 @@ void java_bytecode_instrumentt::add_expr_instrumentation(
328328 code_blockt &block,
329329 const exprt &expr)
330330{
331- codet expr_instrumentation=instrument_expr (expr);
332- if (expr_instrumentation!=code_skipt ())
331+ if (optionalt<codet> expr_instrumentation = instrument_expr (expr))
333332 {
334- if (expr_instrumentation. get_statement ()== ID_block)
335- block.append (to_code_block (expr_instrumentation));
333+ if (expr_instrumentation-> get_statement () == ID_block)
334+ block.append (to_code_block (* expr_instrumentation));
336335 else
337- block.move_to_operands (expr_instrumentation);
336+ block.move_to_operands (* expr_instrumentation);
338337 }
339338}
340339
@@ -475,17 +474,15 @@ void java_bytecode_instrumentt::instrument_code(exprt &expr)
475474// / either assertions or runtime exceptions.
476475// / \param expr: the expression for which we compute
477476// / instrumentation
478- // / \return: The instrumentation required for `expr`
479- codet java_bytecode_instrumentt::instrument_expr (
480- const exprt &expr)
477+ // / \return: The instrumentation for `expr` if required
478+ optionalt<codet> java_bytecode_instrumentt::instrument_expr (const exprt &expr)
481479{
482480 code_blockt result;
483481 // First check our operands:
484482 forall_operands (it, expr)
485483 {
486- codet op_result=instrument_expr (*it);
487- if (op_result!=code_skipt ())
488- result.move_to_operands (op_result);
484+ if (optionalt<codet> op_result = instrument_expr (*it))
485+ result.move_to_operands (*op_result);
489486 }
490487
491488 // Add any check due at this node:
@@ -556,7 +553,7 @@ codet java_bytecode_instrumentt::instrument_expr(
556553 }
557554
558555 if (result==code_blockt ())
559- return code_skipt () ;
556+ return {} ;
560557 else
561558 return result;
562559}
0 commit comments