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 "validate_goto_model.h"
17 #include <util/symbol_table.h>
18 
21 {
22 public:
24  {
25  }
26 
31  virtual bool can_produce_function(const irep_idt &id) const = 0;
32 
40  const irep_idt &id) = 0;
41 
46  virtual const goto_functionst &get_goto_functions() const = 0;
47 
52  virtual const symbol_tablet &get_symbol_table() const = 0;
53 
58  // virtual void validate(const validation_modet vm) const = 0;
59  virtual void validate(
60  const validation_modet vm,
61  const goto_model_validation_optionst &goto_model_validation_options)
62  const = 0;
63 };
64 
65 #endif
Abstract interface to eager or lazy GOTO models.
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.
virtual void validate(const validation_modet vm, const goto_model_validation_optionst &goto_model_validation_options) const =0
Check that the goto model is well-formed.
virtual bool can_produce_function(const irep_idt &id) const =0
Determines if this model can produce a body for the given function.
virtual const symbol_tablet & get_symbol_table() const =0
Accessor to get the symbol table.
virtual const goto_functionst & get_goto_functions() const =0
Accessor to get a raw goto_functionst.
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
The symbol table.
Definition: symbol_table.h:14
Goto Programs with Functions.
Author: Diffblue Ltd.
validation_modet