Project

General

Profile

Feature #10692

Update to Frama-C 20.0

Added by Evgeny Novikov 3 months ago. Updated about 1 month ago.

Status:
Closed
Priority:
High
Category:
Addons
Target version:
Start date:
01/28/2021
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

Frama-C 20.0 exists for a long period of time, but we are still using Frama-C 18.0. Perhaps the update will not change anything for us, but we need to evaluate it. Moreover, it will be easier for developers since they will not need to backport fixes and changes to 18.0.

In addition to this update, it has sense to start using new option "-more-files" recently supported by Mikhail. That option allows to enumerate input source files within a file and to pass this file to toplevel.opt as it was with old CIL.

#1

Updated by Evgeny Novikov 3 months ago

  • Description updated (diff)
#2

Updated by Evgeny Novikov about 2 months ago

  • Status changed from New to Resolved

I implemented this in branch frama-c-20.0. Let's see on testing results.

#3

Updated by Evgeny Novikov about 2 months ago

I updated Frama-C (CIL) one more time. This is necessary to avoid regressions with returns from void functions.

#4

Updated by Evgeny Novikov about 2 months ago

  • Status changed from Resolved to Closed

New Frama-C helped to pass tests, so, I merged the branch to master in 908b4e099.

#5

Updated by Evgeny Novikov about 1 month ago

  • Status changed from Closed to Open

It turned out that new Frama-C takes ~3 times more CPU time. Mikhail has fixed that, so, we need to update Frama-C one more time.

#6

Updated by Evgeny Novikov about 1 month ago

  • Status changed from Open to Resolved

I updated Frama-C in branch update-frama-c. Let's wait for CI and see on testing on ~2000 drivers of Linux 5.5.

#7

Updated by Evgeny Novikov about 1 month ago

  • Status changed from Resolved to Closed

After update Frama-C spends almost the same amount of CPU time as it was before.

#8

Updated by Evgeny Novikov about 1 month ago

The branch passed tests, so, I merged the branch to master in 853a647.

Also available in: Atom PDF