Feature #6545

Invoke BenchExec task with several C files

Added by Ilja Zakharov over 4 years ago. Updated almost 3 years ago.

Tasks generation
Target version:
Start date:
Due date:
% Done:


Estimated time:
Published in build:


Implement checking tasks with several files with BenchExec in native scheduler without cilling.

Related issues

Has duplicate Klever - Feature #8382: Provide a way to prepare verification tasks without CILRejected08/24/2017

Blocked by Klever - Feature #6632: Update BenchExec to last stable versionClosed01/29/2016

Blocked by Klever - Feature #7800: Refactoring of VTGClosed12/13/2016

Blocks Klever - Bug #8453: Some rules are broken and cannot be used without CILNew09/21/2017




Updated by Ilja Zakharov over 4 years ago

  • Category set to Scheduling

Updated by Evgeny Novikov over 4 years ago

  • Subject changed from Invoke benchexec task with several c files to Invoke BenchExec task with several C files
  • Description updated (diff)

Here is my related question to Philipp and his answer:

 How to pass several input files to the verifier? If several files
 are specified as follows: <tasks> <include>file1.c</include>
 <include>file2.c</include> ... </tasks> the verifier is launched
 for each individual file rather than for all of them.

Currently this can be done with an <append> tag inside a <tasks> tag.
All files specified in the <append> tag are appended to all tasks from
this <tasks> tag.
We do not know yet what the best way would be to specify multiple files,
and would like to hear suggestions on this.


Updated by Evgeny Novikov about 3 years ago

  • Priority changed from Low to High
  • Tracker changed from Bug to Feature
  • Category changed from Scheduling to Tasks generation

Indeed this isn't a bug. In addition verification tasks (benchmarks) are generated within Core now, so, I specified the proper category.


Updated by Evgeny Novikov about 3 years ago

  • Assignee set to Ilja Zakharov
  • Priority changed from High to Urgent
  • Target version set to 0.2

I guess that this feature can be trivially implemented. But let's do that after completing Core refactoring.


Updated by Ilja Zakharov about 3 years ago

  • Status changed from New to Resolved

Done in 6545-multiple-files.


Updated by Evgeny Novikov almost 3 years ago

  • Status changed from Resolved to Closed

After minor improvements I merged the branch to master in 74336519.

So, now there is an easy way to run verifiers with multiple input files. BTW, coverage looks better in this case.

Also available in: Atom PDF