Project

General

Profile

Feature #10546

Cause Weaver to output preprocessed source files and models

Added by Evgeny Novikov 3 months ago. Updated 3 months ago.

Status:
Closed
Priority:
Urgent
Category:
Tasks generation
Target version:
Start date:
10/20/2020
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

After #10080 Weaver does not do any preprocessing as it relies upon CIF outputs preprocessed code. But resulting files have ".c" extension that forces Frama-C (CIL) to invoke preprocessor on them.


Related issues

Related to Klever - Feature #10080: Do not preprocess source code outputted by CIFClosed01/28/2020

Actions

History

#1

Updated by Evgeny Novikov 3 months ago

  • Status changed from New to Resolved
  • Description updated (diff)

I implemented this feature in branch cif-cpp-ext. Small tests passed and demonstrated slight performance improvement. Let's wait for CI.

#2

Updated by Evgeny Novikov 3 months ago

  • Related to Feature #10080: Do not preprocess source code outputted by CIF added
#3

Updated by Evgeny Novikov 3 months ago

  • Status changed from Resolved to Closed

CI tests passed demonstrating ~10% improvement in working time of FVTP. So, I merged the branch to master in 576035b2e.

Also available in: Atom PDF