diff --git a/benchexec/runexecutor.py b/benchexec/runexecutor.py index 0e63cb1a4..28c314cc3 100644 --- a/benchexec/runexecutor.py +++ b/benchexec/runexecutor.py @@ -105,7 +105,14 @@ def main(argv=None): "--output", default="output.log", metavar="FILE", - help="name of file where command output (stdout and stderr) is written", + help="name of file where command standard output is written", + ) + io_args.add_argument( + "--error-output", + default=None, + metavar="FILE", + help="name of file where command standard error is written. If not specified, " + "the file for the standard output is used", ) io_args.add_argument( "--maxOutputSize", @@ -257,6 +264,7 @@ def signal_handler_kill(signum, frame): result = executor.execute_run( args=options.args, output_filename=options.output, + error_filename=options.error_output, stdin=stdin, hardtimelimit=options.timelimit, softtimelimit=options.softtimelimit,