Skip to content

Commit ad714bc

Browse files
Use mode of entry function to generate __CPROVER__start
Previously, when we compiled for instance a C file with no `main()` with goto-cc it would have no __CPROVER__start. CBMC would use the following logic to determine the entry point: 1. If `--function` is not passed, use existing `__CPROVER__start` -- in our case, we don't have an existing `__CPROVER__start`, so this doesn't work for us 2. If `--function` _is_ passed, and a `__CPROVER__start` exists: Generate a new entry point calling the passed entry function, based on the mode of the existing `__CPROVER__start` (I am not sure why this mode rather than the mode of `--function`) 3. Otherwise, iterate over the non-binary input files, determine the language to use based on The file extension for each source file, and try to generate an appropriate `__CPROVER__start` based on that The situation of having a single goto-binary with no `__CPROVER__start` as the input file doesn't fit any of these cases, so regardless of whether `--function` is passed CBMC is going to fail, complaining that it can't find or generate an entry point. This adds a fourth case to the list: 4. If `--function` is passed and there is no `__CPROVER__start`, select the language based on the mode of the function parameter and use it to generate `__CPROVER__start` This commit doesn't add tests for this change, but diffblue#4014 adds tests that, in the absence of this change, require hack-y workarounds (such as passing an empty file with a `.c` extension to force C mode for case 3 in the list above) to work.
1 parent 7d71afd commit ad714bc

File tree

1 file changed

+29
-4
lines changed

1 file changed

+29
-4
lines changed

src/goto-programs/initialize_goto_model.cpp

Lines changed: 29 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -133,10 +133,35 @@ goto_modelt initialize_goto_model(
133133
}
134134
else if(!binaries_provided_start)
135135
{
136-
// Allow all language front-ends to try to provide the user-specified
137-
// (--function) entry-point, or some language-specific default:
138-
entry_point_generation_failed=
139-
language_files.generate_support_functions(goto_model.symbol_table);
136+
if(options.is_set("function"))
137+
{
138+
// no entry point is present; Use the mode of the specified entry function
139+
// to generate one
140+
auto const &entry_function_name = options.get_option("function");
141+
auto const entry_function_sym =
142+
goto_model.symbol_table.lookup({entry_function_name});
143+
if(entry_function_sym == nullptr)
144+
{
145+
throw invalid_command_line_argument_exceptiont{
146+
std::string{"couldn't find function with name `"} +
147+
entry_function_name + "' in symbol table",
148+
"--function"};
149+
}
150+
auto const entry_language =
151+
get_language_from_mode(entry_function_sym->mode);
152+
CHECK_RETURN(entry_language != nullptr);
153+
entry_language->set_message_handler(message_handler);
154+
entry_language->set_language_options(options);
155+
entry_point_generation_failed =
156+
entry_language->generate_support_functions(goto_model.symbol_table);
157+
}
158+
if(entry_point_generation_failed || !options.is_set("function"))
159+
{
160+
// Allow all language front-ends to try to provide the user-specified
161+
// (--function) entry-point, or some language-specific default:
162+
entry_point_generation_failed =
163+
language_files.generate_support_functions(goto_model.symbol_table);
164+
}
140165
}
141166

142167
if(entry_point_generation_failed)

0 commit comments

Comments
 (0)