cprover
Loading...
Searching...
No Matches
goto_check.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: GOTO Programs
4
5Author: 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,
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().
void goto_check(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options, message_handlert &message_handler)
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.