cprover
goto_check.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Checks for Errors in C and Java Programs
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_ANALYSES_GOTO_CHECK_H
13 #define CPROVER_ANALYSES_GOTO_CHECK_H
14 
16 
17 class goto_modelt;
18 class namespacet;
19 class optionst;
20 class message_handlert;
21 
22 void goto_check(
23  const namespacet &,
24  const optionst &,
27 
28 void goto_check(
29  const irep_idt &function_identifier,
31  const namespacet &,
32  const optionst &,
34 
36 
37 #endif // CPROVER_ANALYSES_GOTO_CHECK_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
A collection of goto functions.
::goto_functiont goto_functiont
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
void goto_check(const namespacet &, const optionst &, goto_functionst &, message_handlert &)
Definition: goto_check.cpp:34
Goto Programs with Functions.