Feature #10692
closed
Added by Evgeny Novikov about 3 years ago.
Updated about 3 years ago.
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.
- Description updated (diff)
- Status changed from New to Resolved
I implemented this in branch frama-c-20.0. Let's see on testing results.
I updated Frama-C (CIL) one more time. This is necessary to avoid regressions with returns from void functions.
- Status changed from Resolved to Closed
New Frama-C helped to pass tests, so, I merged the branch to master in 908b4e099.
- 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.
- 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.
- Status changed from Resolved to Closed
After update Frama-C spends almost the same amount of CPU time as it was before.
The branch passed tests, so, I merged the branch to master in 853a647.
Also available in: Atom
PDF