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
73
74
75
76
77
78
79
80
81
82
83
84
|
/// Author: Diffblue Ltd.
#include <iostream>
#include <util/cout_message.h>
#include <util/config.h>
#include <util/simplify_expr.h>
#include <util/cmdline.h>
#include <util/options.h>
#include <langapi/mode.h>
#include <ansi-c/ansi_c_language.h>
#include <ansi-c/expr2c.h>
#include <goto-programs/goto_convert_functions.h>
#include <goto-programs/wp.h>
int main(int argc, const char **argv)
{
try
{
cmdlinet cmdline;
config.set(cmdline);
register_language(new_ansi_c_language);
console_message_handlert message_handler;
ansi_c_languaget language;
language.set_message_handler(message_handler);
language.parse(std::cin, "");
symbol_tablet symbol_table;
language.typecheck(symbol_table, "cin");
goto_functionst goto_functions;
goto_convert(symbol_table, goto_functions, message_handler);
goto_functionst::function_mapt::const_iterator
f_it=goto_functions.function_map.find("f");
if(f_it==goto_functions.function_map.end())
{
std::cerr << "no function f" << std::endl;
return 2;
}
const goto_programt &p=f_it->second.body;
// p.output(namespacet(symbol_table), "f", std::cout);
forall_goto_program_instructions(it, p)
{
if(it->is_end_function()) break;
codet code=it->code;
it++;
if(!it->is_assert())
{
std::cerr << "f is expected to have assertion" << std::endl;
return 4;
}
exprt post=it->guard;
namespacet ns(symbol_table);
exprt pre=wp(code, post, ns);
std::cout << "CODE: " << expr2c(code, ns)
<< "wp(" << expr2c(post, ns) << "): "
<< expr2c(pre, ns) << std::endl;
simplify(pre, ns);
std::cout << "Simp: " << expr2c(pre, ns) << std::endl;
std::cout << std::endl;
}
}
catch(const std::string &s)
{
std::cerr << s << std::endl;
}
}
|
