Project

General

Profile

Actions
Copy link

Feature #6545

closed

Invoke BenchExec task with several C files

Added by Ilja Zakharov almost 9 years ago. Updated about 7 years ago.

Status:
Closed
Priority:
Urgent
Assignee:
Ilja Zakharov
Category:
Tasks generation
Target version:
0.2
Start date:
01/28/2016
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

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

Related issues 4 (1 open — 3 closed)

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

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

Actions
Blocked by Klever - Feature #7800: Refactoring of VTGClosedIlja Zakharov12/13/2016

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

Actions
Actions
Copy link
 #1

Updated by Ilja Zakharov almost 9 years ago

  • Category set to Scheduling
Actions
Copy link
 #2

Updated by Evgeny Novikov almost 9 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.

Actions
Copy link
 #3

Updated by Evgeny Novikov over 7 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.

Actions
Copy link
 #4

Updated by Evgeny Novikov over 7 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.

Actions
Copy link
 #5

Updated by Ilja Zakharov over 7 years ago

  • Status changed from New to Resolved

Done in 6545-multiple-files.

Actions
Copy link
 #6

Updated by Evgeny Novikov about 7 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.

Actions
Copy link

Also available in: Atom PDF