diff --git a/regression/contracts/variant_missing_invariant_warning/test.desc b/regression/contracts/variant_missing_invariant_warning/test.desc index 30e327c36a5..be05a219c40 100644 --- a/regression/contracts/variant_missing_invariant_warning/test.desc +++ b/regression/contracts/variant_missing_invariant_warning/test.desc @@ -1,11 +1,11 @@ CORE main.c --apply-loop-contracts -activate-multi-line-match ^The loop at file main.c line 4 function main does not have a loop invariant, but has a decreases clause. Hence, a default loop invariant \('true'\) is being used.$ ^\[main.1\].*Check loop invariant before entry: SUCCESS$ ^\[main.2\].*Check that loop invariant is preserved: SUCCESS$ ^\[main.3\].*Check decreases clause on loop iteration: SUCCESS$ +^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/contracts/variant_multidimensional_ackermann/main.c b/regression/contracts/variant_multidimensional_ackermann/main.c new file mode 100644 index 00000000000..7d0c08e663e --- /dev/null +++ b/regression/contracts/variant_multidimensional_ackermann/main.c @@ -0,0 +1,40 @@ +#include + +int ackermann(int m, int n); + +int main() +{ + int m = 3; + int n = 5; + int result = ackermann(m, n); + + printf("Result of the Ackermann function: %d\n", result); + return 0; +} + +int ackermann(int m, int n) + // clang-format off +__CPROVER_requires(0 <= m && 0 <= n) +__CPROVER_ensures(__CPROVER_return_value >= 0) +// clang-format on +{ + while(m > 0) + // clang-format off + __CPROVER_loop_invariant(0 <= m && 0 <= n) + __CPROVER_decreases(m, n) + // clang-format on + { + if(n == 0) + { + m--; + n = 1; + } + else + { + n = ackermann(m, n - 1); + m--; + } + } + + return n + 1; +} diff --git a/regression/contracts/variant_multidimensional_ackermann/test.desc b/regression/contracts/variant_multidimensional_ackermann/test.desc new file mode 100644 index 00000000000..30290d17349 --- /dev/null +++ b/regression/contracts/variant_multidimensional_ackermann/test.desc @@ -0,0 +1,34 @@ +CORE +main.c +--apply-loop-contracts --replace-all-calls-with-contracts +^\[precondition.1\] .* Check requires clause: SUCCESS$ +^\[precondition.2\] .* Check requires clause: SUCCESS$ +^\[ackermann.1\] .* Check loop invariant before entry: SUCCESS$ +^\[ackermann.2\] .* Check that loop invariant is preserved: SUCCESS$ +^\[ackermann.3\] .* Check decreases clause on loop iteration: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +It tests whether we can prove (only partially) the termination of the Ackermann +function using a multidimensional decreases clause. + +Note that this particular implementation of the Ackermann function contains +both a while-loop and recursion. Therefore, to fully prove the termination of +the Ackermann function, we must prove both +(i) the termination of the while-loop and +(ii) the termination of the recursion. +Because CBMC does not support termination proofs of recursions (yet), we cannot +prove the latter, but the former. Hence, the termination proof in the code is +only "partial." + +Furthermore, the Ackermann function has a function contract that the result +is always non-negative. This post-condition is necessary for establishing +the loop invariant. However, in this test, we do not enforce the function +contract. Instead, we assume that the function contract is correct and use it +(i.e. replace a recursive call of the Ackermann function with its contract). + +We cannot verify/enforce the function contract of the Ackermann function, since +CBMC does not support function contracts for recursively defined functions. +As of now, CBMC only supports function contracts for non-recursive functions. diff --git a/regression/contracts/variant_multidimensional_not_decreasing_fail1/main.c b/regression/contracts/variant_multidimensional_not_decreasing_fail1/main.c new file mode 100644 index 00000000000..0bee402c26b --- /dev/null +++ b/regression/contracts/variant_multidimensional_not_decreasing_fail1/main.c @@ -0,0 +1,22 @@ +int main() +{ + int i = 0; + int j = 0; + int N = 10; + while(i < N) + // clang-format off + __CPROVER_loop_invariant(0 <= i && i <= N && 0 <= j && j <= N) + __CPROVER_decreases(N - i, j) + // clang-format on + { + if(j < N) + { + j++; + } + else + { + i++; + j = 0; + } + } +} diff --git a/regression/contracts/variant_multidimensional_not_decreasing_fail1/test.desc b/regression/contracts/variant_multidimensional_not_decreasing_fail1/test.desc new file mode 100644 index 00000000000..8a5f22d5745 --- /dev/null +++ b/regression/contracts/variant_multidimensional_not_decreasing_fail1/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--apply-loop-contracts +^\[main.1\] .* Check loop invariant before entry: SUCCESS$ +^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.3\] .* Check decreases clause on loop iteration: FAILURE$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +This test fails because the given multidimensional decreases clause does not +monotonically decrease. A mistake is in the second component of the +decreases clause: j. It should instead be N - j. diff --git a/regression/contracts/variant_multidimensional_not_decreasing_fail2/main.c b/regression/contracts/variant_multidimensional_not_decreasing_fail2/main.c new file mode 100644 index 00000000000..bef032c8e4d --- /dev/null +++ b/regression/contracts/variant_multidimensional_not_decreasing_fail2/main.c @@ -0,0 +1,22 @@ +int main() +{ + int i = 0; + int j = 0; + int N = 10; + while(i < N) + // clang-format off + __CPROVER_loop_invariant(0 <= i && i <= N && 0 <= j && j <= N) + __CPROVER_decreases(i, N - j) + // clang-format on + { + if(j < N) + { + j++; + } + else + { + i++; + j = 0; + } + } +} diff --git a/regression/contracts/variant_multidimensional_not_decreasing_fail2/test.desc b/regression/contracts/variant_multidimensional_not_decreasing_fail2/test.desc new file mode 100644 index 00000000000..755888da300 --- /dev/null +++ b/regression/contracts/variant_multidimensional_not_decreasing_fail2/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--apply-loop-contracts +^\[main.1\] .* Check loop invariant before entry: SUCCESS$ +^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.3\] .* Check decreases clause on loop iteration: FAILURE$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +This test fails because the given multidimensional decreases clause does not +monotonically decrease. A mistake is in the first component of the +decreases clause: i. It should instead be N - i. diff --git a/regression/contracts/variant_multidimensional_two_index_variables/main.c b/regression/contracts/variant_multidimensional_two_index_variables/main.c new file mode 100644 index 00000000000..a4b889a03b4 --- /dev/null +++ b/regression/contracts/variant_multidimensional_two_index_variables/main.c @@ -0,0 +1,22 @@ +int main() +{ + int i = 0; + int j = 0; + int N = 10; + while(i < N) + // clang-format off + __CPROVER_loop_invariant(0 <= i && i <= N && 0 <= j && j <= N) + __CPROVER_decreases(N - i, N - j) + // clang-format on + { + if(j < N) + { + j++; + } + else + { + i++; + j = 0; + } + } +} diff --git a/regression/contracts/variant_multidimensional_two_index_variables/test.desc b/regression/contracts/variant_multidimensional_two_index_variables/test.desc new file mode 100644 index 00000000000..7f1172c952f --- /dev/null +++ b/regression/contracts/variant_multidimensional_two_index_variables/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--apply-loop-contracts +^\[main.1\] .* Check loop invariant before entry: SUCCESS$ +^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.3\] .* Check decreases clause on loop iteration: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +It tests whether a multidimensional decreases clause works properly. diff --git a/regression/contracts/variant_not_decreasing_fail/test.desc b/regression/contracts/variant_not_decreasing_fail/test.desc index 84e9b8fae5e..fe019a58bfb 100644 --- a/regression/contracts/variant_not_decreasing_fail/test.desc +++ b/regression/contracts/variant_not_decreasing_fail/test.desc @@ -1,11 +1,9 @@ CORE main.c --apply-loop-contracts -^main.c function main$ ^\[main.1\] .* Check loop invariant before entry: SUCCESS$ ^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$ ^\[main.3\] .* Check decreases clause on loop iteration: FAILURE$ -^.* 1 of 3 failed \(2 iterations\)$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts/variant_parsing_tuple_fail/main.c b/regression/contracts/variant_parsing_multiple_clauses_fail/main.c similarity index 75% rename from regression/contracts/variant_parsing_tuple_fail/main.c rename to regression/contracts/variant_parsing_multiple_clauses_fail/main.c index e0a0f07eb2a..4026bd25beb 100644 --- a/regression/contracts/variant_parsing_tuple_fail/main.c +++ b/regression/contracts/variant_parsing_multiple_clauses_fail/main.c @@ -5,7 +5,8 @@ int main() while(i != N) // clang-format off __CPROVER_loop_invariant(0 <= i && i <= N) - __CPROVER_decreases(N - i, 42) + __CPROVER_decreases(N - i) + __CPROVER_decreases(42) // clang-format on { i++; diff --git a/regression/contracts/variant_parsing_multiple_clauses_fail/test.desc b/regression/contracts/variant_parsing_multiple_clauses_fail/test.desc new file mode 100644 index 00000000000..33fd4093a26 --- /dev/null +++ b/regression/contracts/variant_parsing_multiple_clauses_fail/test.desc @@ -0,0 +1,16 @@ +CORE +main.c +--apply-loop-contracts +activate-multi-line-match +^main.c.*error: syntax error before '__CPROVER_decreases'\n.*__CPROVER_decreases\(42\)$ +^PARSING ERROR$ +^EXIT=(1|64)$ +^SIGNAL=0$ +-- +-- +This test fails because we have multiple decreases clauses. CBMC only admits +one decreases clause for each loop. If one wants to write a multidimensional +decreases clause, it should be placed inside a single __CPROVER_decreases(...), +where each component of the multidimensional decreases clause is separated by a +comma. Hence, in this test, the correct syntax is +__CPROVER_decreases(N - i, 42). diff --git a/regression/contracts/variant_parsing_tuple_fail/test.desc b/regression/contracts/variant_parsing_tuple_fail/test.desc deleted file mode 100644 index f98beefcaf1..00000000000 --- a/regression/contracts/variant_parsing_tuple_fail/test.desc +++ /dev/null @@ -1,13 +0,0 @@ -CORE -main.c ---apply-loop-contracts -activate-multi-line-match -^main.c.*error: syntax error before ','\n.*__CPROVER_decreases\(N - i, 42\)$ -^PARSING ERROR$ -^EXIT=(1|64)$ -^SIGNAL=0$ --- --- -This test fails because the decreases clause has two arguments instead of just one. -Currently, we only support decreases clauses of single arguments - we do not -support decreases clauses of tuples (yet). diff --git a/regression/contracts/variant_weak_invariant_fail/test.desc b/regression/contracts/variant_weak_invariant_fail/test.desc index 0cec1b04c87..34be8a10621 100644 --- a/regression/contracts/variant_weak_invariant_fail/test.desc +++ b/regression/contracts/variant_weak_invariant_fail/test.desc @@ -1,11 +1,9 @@ CORE main.c --apply-loop-contracts -^main.c function main$ ^\[main.1\] .* Check loop invariant before entry: SUCCESS$ ^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$ ^\[main.3\] .* Check decreases clause on loop iteration: FAILURE$ -^.* 1 of 3 failed \(2 iterations\)$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts/variant_while_true_pass/test.desc b/regression/contracts/variant_while_true_pass/test.desc index ae57398ec60..a960e9d006e 100644 --- a/regression/contracts/variant_while_true_pass/test.desc +++ b/regression/contracts/variant_while_true_pass/test.desc @@ -1,16 +1,14 @@ CORE main.c --apply-loop-contracts -^main.c function main$ ^\[main.1\] .* Check loop invariant before entry: SUCCESS$ ^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$ ^\[main.3\] .* Check decreases clause on loop iteration: SUCCESS$ -^.*0 of 3 failed \(1 iterations\)$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ -- -- -This test succeeds. The purpose of this test is to check whether a decreases -clause can successfully prove the termination of a loop (i) whose exit condition -is 1 == 1 (i.e. true) and (ii) that will eventually exit via a break statement. +The purpose of this test is to check whether a decreases clause can +successfully prove the termination of a loop (i) whose exit condition is +1 == 1 (i.e. true) and (ii) that will eventually exit via a break statement. diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index 2324156c22f..5cfbdd45bc4 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/src/ansi-c/c_typecheck_code.cpp @@ -828,9 +828,11 @@ void c_typecheck_baset::typecheck_spec_decreases(codet &code) { if(code.find(ID_C_spec_decreases).is_not_nil()) { - exprt &variant = static_cast(code.add(ID_C_spec_decreases)); - - typecheck_expr(variant); - implicit_typecast_arithmetic(variant); + for(auto &decreases_clause_component : + (static_cast(code.add(ID_C_spec_decreases)).operands())) + { + typecheck_expr(decreases_clause_component); + implicit_typecast_arithmetic(decreases_clause_component); + } } } diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index ab444152907..6d9157f3633 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -509,10 +509,17 @@ cprover_contract_loop_invariant_list_opt: | cprover_contract_loop_invariant_list ; +ACSL_binding_expression_list: + ACSL_binding_expression + { init($$); mto($$, $1); } + | ACSL_binding_expression_list ',' ACSL_binding_expression + { $$=$1; mto($$, $3); } + ; + cprover_contract_decreases_opt: /* nothing */ { init($$); parser_stack($$).make_nil(); } - | TOK_CPROVER_DECREASES '(' ACSL_binding_expression ')' + | TOK_CPROVER_DECREASES '(' ACSL_binding_expression_list ')' { $$=$3; } ; @@ -2449,8 +2456,8 @@ iteration_statement: if(!parser_stack($6).operands().empty()) static_cast(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($6).operands()); - if(parser_stack($7).is_not_nil()) - parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($7)); + if(!parser_stack($7).operands().empty()) + static_cast(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($7).operands()); } | TOK_DO statement TOK_WHILE '(' comma_expression ')' cprover_contract_assigns_opt @@ -2464,8 +2471,8 @@ iteration_statement: if(!parser_stack($8).operands().empty()) static_cast(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($8).operands()); - if(parser_stack($9).is_not_nil()) - parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($9)); + if(!parser_stack($9).operands().empty()) + static_cast(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($9).operands()); } | TOK_FOR { @@ -2495,8 +2502,8 @@ iteration_statement: if(!parser_stack($10).operands().empty()) static_cast(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($10).operands()); - if(parser_stack($11).is_not_nil()) - parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($11)); + if(!parser_stack($11).operands().empty()) + static_cast(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($11).operands()); if(PARSER.for_has_scope) PARSER.pop_scope(); // remove the C99 for-scope diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 596b32c9520..b60a2aa4706 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -34,6 +34,12 @@ Date: February 2016 #include #include +// Create a lexicographic less-than relation between two tuples of variables. +// This is used in the implementation of multidimensional decreases clauses. +static exprt create_lexicographic_less_than( + const std::vector &lhs, + const std::vector &rhs); + exprt get_size(const typet &type, const namespacet &ns, messaget &log) { auto size_of_opt = size_of_expr(type, ns); @@ -86,6 +92,14 @@ void code_contractst::check_apply_loop_contracts( invariant = conjunction(invariant.operands()); } + // Vector representing a (possibly multidimensional) decreases clause + const auto decreases_clause_vector = decreases_clause.operands(); + + // Temporary variables for storing the multidimensional decreases clause + // at the start of and end of a loop body + std::vector old_temporary_variables; + std::vector new_temporary_variables; + // change // H: loop; // E: ... @@ -142,30 +156,40 @@ void code_contractst::check_apply_loop_contracts( converter.goto_convert(assumption, havoc_code, mode); } - // Temporary variables that store the decreases clause's values before and - // after the loop - symbol_exprt old_decreases_symbol = - new_tmp_symbol( - decreases_clause.type(), loop_head->source_location, function_name, mode) - .symbol_expr(); - symbol_exprt new_decreases_symbol = - new_tmp_symbol( - decreases_clause.type(), loop_head->source_location, function_name, mode) - .symbol_expr(); + // Create fresh temporary variables that store the multidimensional + // decreases clause's value before and after the loop + for(const auto &clause : decreases_clause.operands()) + { + old_temporary_variables.push_back( + new_tmp_symbol( + clause.type(), loop_head->source_location, function_name, mode) + .symbol_expr()); + new_temporary_variables.push_back( + new_tmp_symbol( + clause.type(), loop_head->source_location, function_name, mode) + .symbol_expr()); + } if(!decreases_clause.is_nil()) { - // Generate: a declaration of the temporary variable that stores the - // decreases clause's value before the loop - havoc_code.add(goto_programt::make_decl( - old_decreases_symbol, loop_head->source_location)); - - // Generate: an assignment to store the decreases clause's value before the - // loop - code_assignt old_decreases_assignment{old_decreases_symbol, - decreases_clause}; - old_decreases_assignment.add_source_location() = loop_head->source_location; - converter.goto_convert(old_decreases_assignment, havoc_code, mode); + // Generate: declarations of the temporary variables that stores the + // multidimensional decreases clause's value before the loop + for(const auto &old_temp_var : old_temporary_variables) + { + havoc_code.add( + goto_programt::make_decl(old_temp_var, loop_head->source_location)); + } + + // Generate: assignments to store the multidimensional decreases clause's + // value before the loop + for(size_t i = 0; i < old_temporary_variables.size(); i++) + { + code_assignt old_decreases_assignment{old_temporary_variables[i], + decreases_clause_vector[i]}; + old_decreases_assignment.add_source_location() = + loop_head->source_location; + converter.goto_convert(old_decreases_assignment, havoc_code, mode); + } } // non-deterministically skip the loop if it is a do-while loop @@ -193,33 +217,45 @@ void code_contractst::check_apply_loop_contracts( if(!decreases_clause.is_nil()) { - // Generate: a declaration of a temporary variable that stores the decreases - // clause after one arbitrary iteration of the loop - havoc_code.add(goto_programt::make_decl( - new_decreases_symbol, loop_head->source_location)); - - // Generate: an assignment to store the decreases clause's value after one - // iteration of the loop - code_assignt new_decreases_assignment{new_decreases_symbol, - decreases_clause}; - new_decreases_assignment.add_source_location() = loop_head->source_location; - converter.goto_convert(new_decreases_assignment, havoc_code, mode); - - // Generate: assertion that the decreases clause's value after the loop is - // smaller than the value before the loop - code_assertt monotonic_decreasing_assertion{ - binary_relation_exprt(new_decreases_symbol, ID_lt, old_decreases_symbol)}; + // Generate: declarations of temporary variables that stores the + // multidimensional decreases clause's value after one arbitrary iteration + // of the loop + for(const auto &new_temp_var : new_temporary_variables) + { + havoc_code.add( + goto_programt::make_decl(new_temp_var, loop_head->source_location)); + } + + // Generate: assignments to store the multidimensional decreases clause's + // value after one iteration of the loop + for(size_t i = 0; i < new_temporary_variables.size(); i++) + { + code_assignt new_decreases_assignment{new_temporary_variables[i], + decreases_clause_vector[i]}; + new_decreases_assignment.add_source_location() = + loop_head->source_location; + converter.goto_convert(new_decreases_assignment, havoc_code, mode); + } + + // Generate: assertion that the multidimensional decreases clause's value + // after the loop is smaller than the value before the loop. + // Here, we use the lexicographic order. + code_assertt monotonic_decreasing_assertion{create_lexicographic_less_than( + new_temporary_variables, old_temporary_variables)}; monotonic_decreasing_assertion.add_source_location() = loop_head->source_location; converter.goto_convert(monotonic_decreasing_assertion, havoc_code, mode); havoc_code.instructions.back().source_location.set_comment( "Check decreases clause on loop iteration"); - // Discard the temporary variables that store decreases clause's values - havoc_code.add(goto_programt::make_dead( - old_decreases_symbol, loop_head->source_location)); - havoc_code.add(goto_programt::make_dead( - new_decreases_symbol, loop_head->source_location)); + // Discard the temporary variables that store decreases clause's value + for(size_t i = 0; i < old_temporary_variables.size(); i++) + { + havoc_code.add(goto_programt::make_dead( + old_temporary_variables[i], loop_head->source_location)); + havoc_code.add(goto_programt::make_dead( + new_temporary_variables[i], loop_head->source_location)); + } } auto offset = havoc_code.instructions.size(); @@ -235,6 +271,52 @@ void code_contractst::check_apply_loop_contracts( loop_end->set_condition(boolean_negate(loop_end->get_condition())); } +// Create a lexicographic less-than relation between two tuples of variables. +// This is used in the implementation of multidimensional decreases clauses. +static exprt create_lexicographic_less_than( + const std::vector &lhs, + const std::vector &rhs) +{ + PRECONDITION(lhs.size() == rhs.size()); + + if(lhs.empty()) + { + return false_exprt(); + } + + // Store conjunctions of equalities. + // For example, suppose that the two input vectors are and . + // Then this vector stores . + // In fact, the last element is unnecessary, so we do not create it. + exprt::operandst equality_conjunctions(lhs.size()); + equality_conjunctions[0] = binary_relation_exprt(lhs[0], ID_equal, rhs[0]); + for(unsigned int i = 1; i < equality_conjunctions.size() - 1; i++) + { + binary_relation_exprt component_i_equality{lhs[i], ID_equal, rhs[i]}; + equality_conjunctions[i] = + and_exprt(equality_conjunctions[i - 1], component_i_equality); + } + + // Store inequalities between the i-th components of the input vectors + // (i.e. lhs and rhs). + // For example, suppose that the two input vectors are and . + // Then this vector stores . + exprt::operandst lexicographic_individual_comparisons(lhs.size()); + lexicographic_individual_comparisons[0] = + binary_relation_exprt(lhs[0], ID_lt, rhs[0]); + for(unsigned int i = 1; i < lexicographic_individual_comparisons.size(); i++) + { + binary_relation_exprt component_i_less_than{lhs[i], ID_lt, rhs[i]}; + lexicographic_individual_comparisons[i] = + and_exprt(equality_conjunctions[i - 1], component_i_less_than); + } + return disjunction(lexicographic_individual_comparisons); +} + bool code_contractst::has_contract(const irep_idt fun_name) { const symbolt &function_symbol = ns.lookup(fun_name);