@@ -417,12 +417,10 @@ std::unique_ptr<generate_function_bodiest> generate_function_bodies_factory(
417
417
if (std::regex_match (id2string (symbol.first ), cprover_prefix))
418
418
{
419
419
messages.warning () << " generate function bodies: "
420
- << " matched global '"
421
- << id2string (symbol.first )
420
+ << " matched global '" << id2string (symbol.first )
422
421
<< " ' begins with __CPROVER, "
423
422
<< " havoc-ing this global may interfere"
424
- << " with analysis"
425
- << messaget::eom;
423
+ << " with analysis" << messaget::eom;
426
424
}
427
425
globals_to_havoc.push_back (symbol.first );
428
426
}
@@ -487,13 +485,11 @@ void replace_function_bodies(
487
485
{
488
486
if (std::regex_match (id2string (function.first ), cprover_prefix))
489
487
{
490
- messages.warning ()
491
- << " generate function bodies: matched function '"
492
- << id2string (function.first )
493
- << " ' begins with __CPROVER "
494
- << " the generated body for this function "
495
- << " may interfere with analysis"
496
- << messaget::eom;
488
+ messages.warning () << " generate function bodies: matched function '"
489
+ << id2string (function.first )
490
+ << " ' begins with __CPROVER "
491
+ << " the generated body for this function "
492
+ << " may interfere with analysis" << messaget::eom;
497
493
}
498
494
did_generate_body = true ;
499
495
generate_function_body.generate_function_body (
0 commit comments