Bug #6629
closedUsed CIL is outdated
Added by Evgeny Novikov almost 9 years ago. Updated over 5 years ago.
100%
Description
At the moment version 1.5.1 is used. It was released on 14 Jul 2012. See the official CIL page.
Updated by Evgeny Novikov about 6 years ago
- Assignee set to Ilja Zakharov
- Priority changed from Normal to Urgent
- Target version set to 3.0
I suggest that we will not get rid of CIL at least in a near future as we did not do that during many past years. So, at least we should to use a more modern version that can help to get rid of many CIL related issues without increasing verification time.
Updated by Evgeny Novikov over 5 years ago
- Assignee changed from Ilja Zakharov to Evgeny Novikov
Thanks to Mikhail, I am ready to test a new version of CIL included into Deductive Verification Tools for Linux Kernel.
Updated by Evgeny Novikov over 5 years ago
- Blocked by Feature #9519: Frama-C CIL is too inefficient added
Updated by Evgeny Novikov over 5 years ago
- Blocked by Bug #9533: Can't find array size added
Updated by Evgeny Novikov over 5 years ago
- Blocked by Bug #9534: Incorrect printing of Linux BUILD_BUG_ON added
Updated by Evgeny Novikov over 5 years ago
- Blocked by deleted (Bug #9533: Can't find array size)
Updated by Evgeny Novikov over 5 years ago
- Blocked by deleted (Bug #9534: Incorrect printing of Linux BUILD_BUG_ON)
Updated by Evgeny Novikov over 5 years ago
- Blocked by Feature #9536: Update CIF added
Updated by Evgeny Novikov over 5 years ago
- Blocked by Bug #9537: Frama-C (CIL) reports strange error about type redefinition added
Updated by Evgeny Novikov over 5 years ago
- Blocked by Bug #9543: Frama-C (CIL) dislikes large enumerators added
Updated by Evgeny Novikov over 5 years ago
- Blocked by Bug #9544: Better support of fields declared using flexible array members added
Updated by Evgeny Novikov over 5 years ago
- Blocked by Bug #9546: Frama-C (CIL) for GCC does not behave like GCC when casting ternary operators added
Updated by Evgeny Novikov over 5 years ago
- Status changed from New to Resolved
I switched Klever to Frama-C (CIL) from Deductive Verification Tools for Linux Kernel in branch frama-c-cil and made everything required in addition there. Now the branch undergoes testing. I hope that this is the last iteration.
Updated by Evgeny Novikov over 5 years ago
- Status changed from Resolved to Closed
I merged the branch to master in c082518. Enjoy new CIL!
Don't forget to update your local Klever add-ons and deployment configuration files.
Updated by Evgeny Novikov over 5 years ago
- Status changed from Open to Closed
I do not know why Forge changed the priority for this issue itself. Also, I can not return the proper priority back. Please, consider it as an Urgent issue.
Updated by Evgeny Novikov over 5 years ago
- Related to Bug #5323: Incorrect type for pointer in ___del_dma_pool added