Project

General

Profile

Actions
Copy link

Feature #9530

open

Investigate cons and pros of Frama-C (CIL) slicing

Added by Evgeny Novikov about 5 years ago.

Status:
New
Priority:
High
Assignee:
-
Category:
Addons
Target version:
-
Start date:
03/13/2019
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

Here https://forge.ispras.ru/issues/9519#note-4 Mikhail reported awesome improvements in consuming computational resources by CPAchecker when using slicing in Frama-C (CIL) in advance. We do need to investigate how many cons and pros this slicing has. Possible drawbacks:
  • Frama-C (CIL) can take too much CPU time or/and RAM for performing slicing.
  • For sliced source code CPAchecker can output too bad witnesses that we will not be able to convert to nice error traces for manual analysis.
  • Different errors during slicing and in sliced source code.

No data to display

Actions
Copy link

Also available in: Atom PDF