ESBMC Symbol Table

1. Namespacet

A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in them.

The basic idea is that you might want to combine a value table and a type table, so that for a variable you can lookup both of these essential properties, in one structure.

2. contextt

1
2
3
symbol_base_mapt symbol_base_map;
symbolst symbols;
ordered_symbolst ordered_symbols;

3. symbolt/symbolst

  • GOTO conversion component constructs a goto-program from a symbol table. Each symbol in the symbol table with function type (that is, the symbol’s type field contains a code_typet) will be converted to a corresponding GOTO program. Function goto_convertt::convert turns each codet in the symbol table into corresponding GOTO instructions.