1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
|
/*******************************************************************\
Module: Unit tests for goto_program::validate
Author: Diffblue Ltd.
\*******************************************************************/
#include <util/bitvector_types.h>
#include <util/namespace.h>
#include <util/symbol_table.h>
#include <goto-programs/goto_function.h>
#include <testing-utils/use_catch.h>
SCENARIO(
"Validation of well-formed function call codes",
"[core][goto-programs][validate]")
{
GIVEN("A program with one function call")
{
symbol_tablet symbol_table;
const signedbv_typet type1(32);
const signedbv_typet type2(64);
const code_typet code_type({}, type1);
symbolt var_symbol{"a", type1, irep_idt{}};
symbol_exprt var_a = var_symbol.symbol_expr();
symbolt var_symbol2{"b", type2, irep_idt{}};
symbol_exprt var_b = var_symbol2.symbol_expr();
symbolt fun_symbol{"foo", code_type, irep_idt{}};
symbol_exprt fun_foo = fun_symbol.symbol_expr();
goto_functiont goto_function;
auto &instructions = goto_function.body.instructions;
instructions.emplace_back(goto_program_instruction_typet::FUNCTION_CALL);
symbol_table.insert(var_symbol);
symbol_table.insert(var_symbol2);
symbol_table.insert(fun_symbol);
namespacet ns(symbol_table);
WHEN("Return type matches")
{
code_function_callt function_call(var_a, fun_foo, {});
instructions.back() = goto_programt::make_function_call(function_call);
REQUIRE(instructions.back().code().get_statement() == ID_function_call);
THEN("The consistency check succeeds")
{
goto_function.body.validate(ns, validation_modet::INVARIANT);
REQUIRE(true);
}
}
WHEN("Return type differs from function type")
{
code_function_callt function_call(var_b, fun_foo, {});
instructions.back() = goto_programt::make_function_call(function_call);
THEN("The consistency check fails")
{
REQUIRE_THROWS_AS(
goto_function.body.validate(ns, validation_modet::EXCEPTION),
incorrect_goto_program_exceptiont);
}
}
}
}
|
