CBMC: /home/runner/work/cbmc/cbmc/src/goto-programs/remove_vector.h Source File

CBMC
Loading...
Searching...
No Matches
remove_vector.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Remove the 'vector' data type by compilation into arrays
4
5Author: Daniel Kroening
6
7Date: September 2014
8
9\*******************************************************************/
10
13
14#ifndef CPROVER_GOTO_PROGRAMS_REMOVE_VECTOR_H
15#define CPROVER_GOTO_PROGRAMS_REMOVE_VECTOR_H
16
17class goto_functionst;
18class goto_modelt;
19class symbol_table_baset;
20
21void remove_vector(symbol_table_baset &, goto_functionst &);
22
23void remove_vector(goto_modelt &);
24
27bool has_vector(const goto_functionst &);
28
31bool has_vector(const goto_modelt &);
32
33#endif // CPROVER_GOTO_PROGRAMS_REMOVE_VECTOR_H
A collection of goto functions.
The symbol table base class interface.
bool has_vector(const goto_functionst &)
returns true iff any of the given goto functions has instructions that use the vector type
void remove_vector(symbol_table_baset &, goto_functionst &)
removes vector data type

AltStyle によって変換されたページ (->オリジナル) /