CBMC
Loading...
Searching...
No Matches
dump_c.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dump C from Goto Program
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_INSTRUMENT_DUMP_C_H
13#define CPROVER_GOTO_INSTRUMENT_DUMP_C_H
14
15#include <iosfwd>
16#include <string>
17
18class goto_functionst;
19class namespacet;
20
21void dump_c(
22 const goto_functionst &src,
23 const bool use_system_headers,
24 const bool use_all_headers,
25 const bool include_harness,
26 const namespacet &ns,
27 std::ostream &out);
28
30 const goto_functionst &src,
31 const bool use_system_headers,
32 const bool use_all_headers,
33 const bool include_harness,
34 const namespacet &ns,
35 const std::string module,
36 std::ostream &out);
37
38void dump_cpp(
39 const goto_functionst &src,
40 const bool use_system_headers,
41 const bool use_all_headers,
42 const bool include_harness,
43 const namespacet &ns,
44 std::ostream &out);
45
46#define OPT_DUMP_C \
47 "(dump-c)(dump-cpp)" \
48 "(dump-c-type-header):" \
49 "(no-system-headers)(use-all-headers)(harness)"
50
51#define HELP_DUMP_C \
52 " {y--dump-c} \t generate C source\n" \
53 " {y--dump-c-type-header} {um} \t " \
54 "generate a C header for types local in {um}\n" \
55 " {y--dump-cpp} \t generate C++ source\n" \
56 " {y--no-system-headers} \t generate C source expanding libc includes\n" \
57 " {y--use-all-headers} \t generate C source with all includes\n" \
58 " {y--harness} \t include input generator in output\n"
59
60#endif // CPROVER_GOTO_INSTRUMENT_DUMP_C_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
A collection of goto functions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
void dump_cpp(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &ns, std::ostream &out)
Definition dump_c.cpp:1681
void dump_c(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &ns, std::ostream &out)
Definition dump_c.cpp:1668
void dump_c_type_header(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &ns, const std::string module, std::ostream &out)
Definition dump_c.cpp:1703