Fix argument check

thomasspriggs · thomasspriggs · commit 4322d6102704 · 2023-07-04T17:03:06.000+01:00
Zero arguments should trigger an error as should files which fail the
is_goto_binary check when a single file is specified.
diff --git a/src/goto-bmc/goto_bmc_parse_options.cpp b/src/goto-bmc/goto_bmc_parse_options.cpp
@@ -38,7 +38,7 @@ int goto_bmc_parse_optionst::doit()
 
   api_sessiont api{api_options};
 
-  if(cmdline.args.size() > 1 && !api.is_goto_binary(cmdline.args[0]))
+  if(cmdline.args.size() != 1 || !api.is_goto_binary(cmdline.args[0]))
   {
     log.error() << "Please give exactly one binary file" << messaget::eom;
     return CPROVER_EXIT_INCORRECT_TASK;

Original file line number	Diff line number	Diff line change
`@@ -38,7 +38,7 @@ int goto_bmc_parse_optionst::doit()`
`38`	`38`
`39`	`39`	`api_sessiont api{api_options};`
`40`	`40`
`41`		`- if(cmdline.args.size() > 1 && !api.is_goto_binary(cmdline.args[0]))`
	`41`	`+ if(cmdline.args.size() != 1 \|\| !api.is_goto_binary(cmdline.args[0]))`
`42`	`42`	`{`
`43`	`43`	`log.error() << "Please give exactly one binary file" << messaget::eom;`
`44`	`44`	`return CPROVER_EXIT_INCORRECT_TASK;`