Feature #9535
Bug #6629: Used CIL is outdated
Increase memory limit for Frama-C (CIL)
0%
Description
Unfortunately it seems that Frama-C (CIL) needs much more memory than previously used CIL. Maybe 1 GB instead of 300 MB will be enough to have the same results. Also we need to increase the default memory limit for deciding verification jobs.
Related issues
History
Updated by Evgeny Novikov 4 months ago
Updated by - Related to Feature #9538: Reduce memory consumption by Frama-C (CIL) added
Updated by Evgeny Novikov 4 months ago
- Status changed from New to Open
I did both in branch frama-c-cil. But in one case it did not help. Let's wait for #9538 since too greedy CIL is not good.
Updated by Evgeny Novikov 4 months ago
- Related to deleted (Feature #9538: Reduce memory consumption by Frama-C (CIL))
Updated by Evgeny Novikov 4 months ago
- Blocked by Feature #9538: Reduce memory consumption by Frama-C (CIL) added
Updated by Evgeny Novikov 4 months ago
- Blocked by deleted (Feature #9538: Reduce memory consumption by Frama-C (CIL))
Updated by Evgeny Novikov 4 months ago
- Related to Feature #9538: Reduce memory consumption by Frama-C (CIL) added
Updated by Evgeny Novikov 4 months ago
- Status changed from Open to Resolved
One more iteration helped. Unfortunately, Frama-C (CIL) needs very much RAM for merging some source files. At the moment the limit is 2 GB rather than 300 MB as it was for CIL. Job limits start from 3 GB and they are 5 GB even for jobs that have only 2 parallel task generators and one sub-job worker of course. Nevertheless for simple tests one can use much more aggressive parallelism.
Updated by Evgeny Novikov 4 months ago
After Mikhail made considerable optimizations (#9538) I reduced the CIL memory limit from 2 GB to 1 GB. I didn't change job limits, since specified values seem to be much better.
Updated by Evgeny Novikov 4 months ago
- Status changed from Resolved to Closed
I merged the branch to master in c082518.