cprover
goto_check.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: GOTO Programs
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "goto_check.h"
13 
14 #include "goto_check_c.h"
15 
16 #include <util/symbol.h>
17 
19  const irep_idt &function_identifier,
20  goto_functionst::goto_functiont &goto_function,
21  const namespacet &ns,
22  const optionst &options,
23  message_handlert &message_handler)
24 {
25  const auto &function_symbol = ns.lookup(function_identifier);
26 
27  if(function_symbol.mode == ID_C)
28  {
30  function_identifier, goto_function, ns, options, message_handler);
31  }
32 }
33 
35  const namespacet &ns,
36  const optionst &options,
37  goto_functionst &goto_functions,
38  message_handlert &message_handler)
39 {
40  goto_check_c(ns, options, goto_functions, message_handler);
41 }
42 
44  const optionst &options,
45  goto_modelt &goto_model,
46  message_handlert &message_handler)
47 {
48  goto_check_c(options, goto_model, message_handler);
49 }
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
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
void goto_check(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options, message_handlert &message_handler)
Definition: goto_check.cpp:18
Checks for Errors in C and Java Programs.
void goto_check_c(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options, message_handlert &message_handler)
Program Transformation.
Symbol table entry.