Skip to content

Commit a20f4f6

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 a20f4f6

File tree

1 file changed

+30
-4
lines changed

1 file changed

+30
-4
lines changed

src/goto-programs/initialize_goto_model.cpp

Lines changed: 30 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -133,10 +133,36 @@ 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+
// NOLINTNEXTLINE(whitespace/braces)
147+
std::string{"couldn't find function with name `"} +
148+
entry_function_name + "' in symbol table",
149+
"--function"};
150+
}
151+
auto const entry_language =
152+
get_language_from_mode(entry_function_sym->mode);
153+
CHECK_RETURN(entry_language != nullptr);
154+
entry_language->set_message_handler(message_handler);
155+
entry_language->set_language_options(options);
156+
entry_point_generation_failed =
157+
entry_language->generate_support_functions(goto_model.symbol_table);
158+
}
159+
if(entry_point_generation_failed || !options.is_set("function"))
160+
{
161+
// Allow all language front-ends to try to provide the user-specified
162+
// (--function) entry-point, or some language-specific default:
163+
entry_point_generation_failed =
164+
language_files.generate_support_functions(goto_model.symbol_table);
165+
}
140166
}
141167

142168
if(entry_point_generation_failed)

0 commit comments

Comments
 (0)