cprover
goto_convert.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Program Transformation
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_CONVERT_H
13 #define CPROVER_GOTO_PROGRAMS_GOTO_CONVERT_H
14 
15 #include <util/message.h>
16 #include <util/std_code.h>
17 
18 #include "goto_program.h"
19 
20 // start from given code
21 void goto_convert(
22  const codet &code,
23  symbol_tablet &symbol_table,
24  goto_programt &dest,
25  message_handlert &message_handler);
26 
27 // start from "main"
28 void goto_convert(
29  symbol_tablet &symbol_table,
30  goto_programt &dest,
31  message_handlert &message_handler);
32 
33 #endif // CPROVER_GOTO_PROGRAMS_GOTO_CONVERT_H
The symbol table.
Definition: symbol_table.h:52
void goto_convert(const codet &code, symbol_tablet &symbol_table, goto_programt &dest, message_handlert &message_handler)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
A statement in a programming language.
Definition: std_code.h:19
Concrete Goto Program.