Skip to content

Commit 1f1de48

Browse files
author
Thomas Kiley
authored
Merge pull request #5407 from thk123/fix-help-text
Fix help text in goto-harness
2 parents 62df39e + 589e718 commit 1f1de48

File tree

3 files changed

+16
-2
lines changed

3 files changed

+16
-2
lines changed
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--harness-type call-function --function test --associated-array-size array:sze
4+
Expected parameter: \"sze\" on function \"test\"
5+
^EXIT=1$
6+
^SIGNAL=0$
7+
--
8+
--
9+
Tes the error message for invalid array size association is reported correctly.

src/goto-harness/function_call_harness_generator.cpp

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -508,7 +508,11 @@ function_call_harness_generatort::implt::declare_arguments(
508508
associated_array_size_argument == parameter_name_to_argument_name.end())
509509
{
510510
throw invalid_command_line_argument_exceptiont{
511-
"associated array size is not there",
511+
"could not find parameter to associate the array size of array \"" +
512+
id2string(parameter_name) + "\" (Expected parameter: \"" +
513+
id2string(associated_array_size_parameter) + "\" on function \"" +
514+
id2string(function_to_call.display_name()) + "\" in " +
515+
function_to_call.location.as_string() + ")",
512516
"--" FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT};
513517
}
514518
function_argument_to_associated_array_size.insert(

src/goto-harness/goto_harness_parse_options.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -174,7 +174,8 @@ void goto_harness_parse_optionst::help()
174174
<< " goto-harness <in> <out> --harness-function-name <name> --harness-type "
175175
"<harness-type> [harness options]\n"
176176
<< "\n"
177-
<< "<in> <out> goto binaries to read from / write to\n"
177+
<< "<in> goto binaries to read from\n"
178+
<< "<out> C file to write the harness to\n"
178179
<< "--harness-function-name the name of the harness function to "
179180
"generate\n"
180181
<< "--harness-type one of the harness types listed below\n"

0 commit comments

Comments
 (0)