@@ -473,18 +473,21 @@ code_contractst::create_ensures_instruction(
473
473
}
474
474
475
475
bool code_contractst::apply_function_contract (
476
- goto_programt &goto_program,
477
- goto_programt::targett target)
476
+ const irep_idt &function,
477
+ goto_programt &function_body,
478
+ goto_programt::targett &target)
478
479
{
480
+ const auto &const_target =
481
+ static_cast <const goto_programt::targett &>(target);
479
482
// Return if the function is not named in the call; currently we don't handle
480
483
// function pointers.
481
- PRECONDITION (as_const (*target). call_function ().id () == ID_symbol);
484
+ PRECONDITION (const_target-> call_function ().id () == ID_symbol);
482
485
483
486
// Retrieve the function type, which is needed to extract the contract
484
487
// components.
485
- const irep_idt &function =
486
- to_symbol_expr (as_const (*target). call_function ()).get_identifier ();
487
- const symbolt &function_symbol = ns.lookup (function );
488
+ const irep_idt &target_function =
489
+ to_symbol_expr (const_target-> call_function ()).get_identifier ();
490
+ const symbolt &function_symbol = ns.lookup (target_function );
488
491
const auto &type = to_code_with_contract_type (function_symbol.type );
489
492
490
493
// Isolate each component of the contract.
@@ -499,15 +502,15 @@ bool code_contractst::apply_function_contract(
499
502
if (type.return_type () != empty_typet ())
500
503
{
501
504
// Check whether the function's return value is not disregarded.
502
- if (as_const (* target). call_lhs ().is_not_nil ())
505
+ if (target-> call_lhs ().is_not_nil ())
503
506
{
504
507
// If so, have it replaced appropriately.
505
508
// For example, if foo() ensures that its return value is > 5, then
506
509
// rewrite calls to foo as follows:
507
510
// x = foo() -> assume(__CPROVER_return_value > 5) -> assume(x > 5)
508
511
symbol_exprt ret_val (
509
- CPROVER_PREFIX " return_value" , as_const (*target). call_lhs ().type ());
510
- common_replace.insert (ret_val, as_const (*target). call_lhs ());
512
+ CPROVER_PREFIX " return_value" , const_target-> call_lhs ().type ());
513
+ common_replace.insert (ret_val, const_target-> call_lhs ());
511
514
}
512
515
else
513
516
{
@@ -521,10 +524,10 @@ bool code_contractst::apply_function_contract(
521
524
// fresh variable to replace __CPROVER_return_value with.
522
525
const symbolt &fresh = get_fresh_aux_symbol (
523
526
type.return_type (),
524
- id2string (function ),
527
+ id2string (target_function ),
525
528
" ignored_return_value" ,
526
- target ->source_location ,
527
- symbol_table.lookup_ref (function ).mode ,
529
+ const_target ->source_location ,
530
+ symbol_table.lookup_ref (target_function ).mode ,
528
531
ns,
529
532
symbol_table);
530
533
symbol_exprt ret_val (CPROVER_PREFIX " return_value" , type.return_type ());
@@ -534,7 +537,7 @@ bool code_contractst::apply_function_contract(
534
537
}
535
538
536
539
// Replace formal parameters
537
- const auto &arguments = target ->call_arguments ();
540
+ const auto &arguments = const_target ->call_arguments ();
538
541
auto a_it = arguments.begin ();
539
542
for (auto p_it = type.parameters ().begin ();
540
543
p_it != type.parameters ().end () && a_it != arguments.end ();
@@ -551,9 +554,9 @@ bool code_contractst::apply_function_contract(
551
554
// and only refer to the common symbols to be replaced.
552
555
common_replace (assigns);
553
556
554
- const auto &mode = symbol_table.lookup_ref (function ).mode ;
557
+ const auto &mode = symbol_table.lookup_ref (target_function ).mode ;
555
558
556
- is_fresh_replacet is_fresh (*this , log , function );
559
+ is_fresh_replacet is_fresh (*this , log , target_function );
557
560
is_fresh.create_declarations ();
558
561
559
562
// Insert assertion of the precondition immediately before the call site.
@@ -567,14 +570,14 @@ bool code_contractst::apply_function_contract(
567
570
converter.goto_convert (
568
571
code_assertt (requires),
569
572
assertion,
570
- symbol_table.lookup_ref (function ).mode );
573
+ symbol_table.lookup_ref (target_function ).mode );
571
574
assertion.instructions .back ().source_location = requires.source_location ();
572
575
assertion.instructions .back ().source_location .set_comment (
573
576
" Check requires clause" );
574
577
assertion.instructions .back ().source_location .set_property_class (
575
578
ID_precondition);
576
579
is_fresh.update_requires (assertion);
577
- insert_before_swap_and_advance (goto_program , target, assertion);
580
+ insert_before_swap_and_advance (function_body , target, assertion);
578
581
}
579
582
580
583
// Gather all the instructions required to handle history variables
@@ -590,11 +593,11 @@ bool code_contractst::apply_function_contract(
590
593
ensures_pair = create_ensures_instruction (
591
594
assumption,
592
595
ensures.source_location (),
593
- symbol_table.lookup_ref (function ).mode );
596
+ symbol_table.lookup_ref (target_function ).mode );
594
597
595
598
// add all the history variable initialization instructions
596
599
// to the goto program
597
- insert_before_swap_and_advance (goto_program , target, ensures_pair.second );
600
+ insert_before_swap_and_advance (function_body , target, ensures_pair.second );
598
601
}
599
602
600
603
// Create a series of non-deterministic assignments to havoc the variables
@@ -604,9 +607,8 @@ bool code_contractst::apply_function_contract(
604
607
assigns_clauset assigns_clause (assigns, log , ns);
605
608
606
609
// Retrieve assigns clause of the caller function if exists.
607
- const irep_idt &caller_function = target->source_location .get_function ();
608
610
auto caller_assigns =
609
- to_code_with_contract_type (ns.lookup (caller_function ).type ).assigns ();
611
+ to_code_with_contract_type (ns.lookup (function ).type ).assigns ();
610
612
611
613
if (caller_assigns.is_not_nil ())
612
614
{
@@ -617,31 +619,32 @@ bool code_contractst::apply_function_contract(
617
619
caller_assigns_clause.generate_subset_check (assigns_clause),
618
620
assigns_clause.location ));
619
621
subset_check_assertion.instructions .back ().source_location .set_comment (
620
- " Check that " + id2string (function) +
621
- " 's assigns clause is a subset of " + id2string (caller_function) +
622
+ " Check that " + id2string (target_function) +
623
+ " 's assigns clause is a subset of " +
624
+ id2string (const_target->source_location .get_function ()) +
622
625
" 's assigns clause" );
623
626
insert_before_swap_and_advance (
624
- goto_program , target, subset_check_assertion);
627
+ function_body , target, subset_check_assertion);
625
628
}
626
629
627
630
// Havoc all targets in global write set
628
631
auto assigns_havoc = assigns_clause.generate_havoc_code ();
629
632
630
633
// Insert the non-deterministic assignment immediately before the call site.
631
- insert_before_swap_and_advance (goto_program , target, assigns_havoc);
634
+ insert_before_swap_and_advance (function_body , target, assigns_havoc);
632
635
}
633
636
634
637
// To remove the function call, insert statements related to the assumption.
635
638
// Then, replace the function call with a SKIP statement.
636
639
if (!ensures.is_false ())
637
640
{
638
641
is_fresh.update_ensures (ensures_pair.first );
639
- insert_before_swap_and_advance (goto_program , target, ensures_pair.first );
642
+ insert_before_swap_and_advance (function_body , target, ensures_pair.first );
640
643
}
641
644
*target = goto_programt::make_skip ();
642
645
643
646
// Add this function to the set of replaced functions.
644
- summarized.insert (function );
647
+ summarized.insert (target_function );
645
648
return false ;
646
649
}
647
650
@@ -1223,7 +1226,8 @@ bool code_contractst::replace_calls(const std::set<std::string> &functions)
1223
1226
if (found == functions.end ())
1224
1227
continue ;
1225
1228
1226
- fail |= apply_function_contract (goto_function.second .body , ins);
1229
+ fail |= apply_function_contract (
1230
+ goto_function.first , goto_function.second .body , ins);
1227
1231
}
1228
1232
}
1229
1233
}
0 commit comments