Skip to content

Commit 94f96c0

Browse files
committed
symtab2gb should populate configt
For as long as goto-programs/ uses util/c_types.h, expression types generated during goto-program construction rely on bit widths to be configured.
1 parent 29a323f commit 94f96c0

File tree

1 file changed

+4
-0
lines changed

1 file changed

+4
-0
lines changed

src/symtab2gb/symtab2gb_parse_options.cpp

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,8 @@ Author: Diffblue Ltd.
1717
#include <goto-programs/link_goto_model.h>
1818
#include <goto-programs/write_goto_binary.h>
1919
#include <json-symtab-language/json_symtab_language.h>
20+
21+
#include <util/config.h>
2022
#include <util/exception_utils.h>
2123
#include <util/exit_codes.h>
2224
#include <util/invariant.h>
@@ -81,6 +83,7 @@ static void run_symtab2gb(
8183
throw invalid_source_file_exceptiont{
8284
"failed to typecheck symbol table from file '" + symtab_filename + "'"};
8385
}
86+
config.set_from_symbol_table(symtab);
8487
goto_modelt goto_model{};
8588
goto_model.symbol_table = symtab;
8689
goto_convert(goto_model, message_handler);
@@ -110,6 +113,7 @@ int symtab2gb_parse_optionst::doit()
110113
{
111114
gb_filename = cmdline.get_value(SYMTAB2GB_OUT_FILE_OPT);
112115
}
116+
config.set(cmdline);
113117
run_symtab2gb(symtab_filenames, gb_filename);
114118
return CPROVER_EXIT_SUCCESS;
115119
}

0 commit comments

Comments
 (0)