Project

General

Profile

Actions
Copy link

Feature #10546

closed

Cause Weaver to output preprocessed source files and models

Added by Evgeny Novikov over 3 years ago. Updated over 3 years ago.

Status:
Closed
Priority:
Urgent
Assignee:
Evgeny Novikov
Category:
Tasks generation
Target version:
3.0
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 1 (0 open — 1 closed)

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

Actions
Actions
Copy link
 #1

Updated by Evgeny Novikov over 3 years ago

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

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

Actions
Copy link
 #2

Updated by Evgeny Novikov over 3 years ago

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

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

Actions
Copy link

Also available in: Atom PDF