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

Remove the 'vector' data type by compilation into arrays. More...

Go to the source code of this file.

Functions

void remove_vector (symbol_table_baset &, goto_functionst &)
 removes vector data type
 
void remove_vector (goto_modelt &)
 removes vector data type
 
bool has_vector (const goto_functionst &)
 returns true iff any of the given goto functions has instructions that use the vector type
 
bool has_vector (const goto_modelt &)
 returns true iff the given goto model has instructions that use the vector type
 

Remove the 'vector' data type by compilation into arrays.

Definition in file remove_vector.h.

◆ has_vector() [1/2]

returns true iff any of the given goto functions has instructions that use the vector type

Definition at line 390 of file remove_vector.cpp.

◆ has_vector() [2/2]

returns true iff the given goto model has instructions that use the vector type

Definition at line 407 of file remove_vector.cpp.

◆ remove_vector() [2/2]