CBMC
Loading...
Searching...
No Matches
abstract_goto_model.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Abstract GOTO Model
4
5Author: 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
18class symbol_tablet;
19
22{
23public:
25 {
26 }
27
32 virtual bool can_produce_function(const irep_idt &id) const = 0;
33
41 const irep_idt &id) = 0;
42
47 virtual const goto_functionst &get_goto_functions() const = 0;
48
53 virtual const symbol_tablet &get_symbol_table() const = 0;
54
59 // virtual void validate(const validation_modet vm) const = 0;
60 virtual void validate(
61 const validation_modet vm,
63 const = 0;
64};
65
66#endif
Abstract interface to eager or lazy GOTO models.
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 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 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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
A collection of goto functions.
::goto_functiont goto_functiont
The symbol table.
Goto Programs with Functions.
validation_modet