CBMC
process_goto_program.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Process a Goto Program
4 
5 Author: Martin Brain, martin.brain@cs.ox.ac.uk
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_GOTO_PROGRAMS_PROCESS_GOTO_PROGRAM_H
10 #define CPROVER_GOTO_PROGRAMS_PROCESS_GOTO_PROGRAM_H
11 
12 class goto_modelt;
13 class optionst;
14 class messaget;
15 
22 bool process_goto_program(
23  goto_modelt &goto_model,
24  const optionst &options,
25  messaget &log);
26 
27 #endif // CPROVER_GOTO_PROGRAMS_PROCESS_GOTO_PROGRAM_H
goto_modelt
Definition: goto_model.h:27
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
log
double log(double x)
Definition: math.c:2776
process_goto_program
bool process_goto_program(goto_modelt &goto_model, const optionst &options, messaget &log)
Common processing and simplification of goto_programts.
Definition: process_goto_program.cpp:35