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