cprover
abstract_goto_model.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Abstract GOTO Model
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_PROGRAMS_ABSTRACT_GOTO_MODEL_H
13 #define CPROVER_GOTO_PROGRAMS_ABSTRACT_GOTO_MODEL_H
14 
15 #include "goto_functions.h"
16 #include <util/symbol_table.h>
17 
20 {
21 public:
23  {
24  }
25 
30  virtual bool can_produce_function(const irep_idt &id) const = 0;
31 
39  const irep_idt &id) = 0;
40 
45  virtual const goto_functionst &get_goto_functions() const = 0;
46 
51  virtual const symbol_tablet &get_symbol_table() const = 0;
52 };
53 
54 #endif
abstract_goto_modelt::can_produce_function
virtual bool can_produce_function(const irep_idt &id) const =0
Determines if this model can produce a body for the given function.
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
abstract_goto_modelt::get_symbol_table
virtual const symbol_tablet & get_symbol_table() const =0
Accessor to get the symbol table.
abstract_goto_modelt::~abstract_goto_modelt
virtual ~abstract_goto_modelt()
Definition: abstract_goto_model.h:22
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
abstract_goto_modelt::get_goto_functions
virtual const goto_functionst & get_goto_functions() const =0
Accessor to get a raw goto_functionst.
abstract_goto_modelt::get_goto_function
virtual const goto_functionst::goto_functiont & get_goto_function(const irep_idt &id)=0
Get a GOTO function by name, or throw if no such function exists.
goto_functions.h
abstract_goto_modelt
Abstract interface to eager or lazy GOTO models.
Definition: abstract_goto_model.h:19
symbol_table.h
Author: Diffblue Ltd.