Feature #9535
closed
Bug #6629: Used CIL is outdated
Increase memory limit for Frama-C (CIL)
Added by Evgeny Novikov over 5 years ago.
Updated over 5 years ago.
Category:
Tasks generation
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 to Feature #9538: Reduce memory consumption by Frama-C (CIL) added
Perhaps, we will not need this if #9538 will shoot.
- 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.
- Related to deleted (Feature #9538: Reduce memory consumption by Frama-C (CIL))
- Blocked by Feature #9538: Reduce memory consumption by Frama-C (CIL) added
- Blocked by deleted (Feature #9538: Reduce memory consumption by Frama-C (CIL))
- Related to Feature #9538: Reduce memory consumption by Frama-C (CIL) added
- 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.
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.
- Status changed from Resolved to Closed
I merged the branch to master in c082518.
Also available in: Atom
PDF