(Total: 0.00 h)
At the moment version 1.5.1 is used. It was released on 14 Jul 2012. See the official CIL page.
- Target version set to 3.0
- Priority changed from Normal to Urgent
- Assignee set to Ilja Zakharov
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.
- Assignee changed from Ilja Zakharov to Evgeny Novikov
- Blocked by Bug #9533: Can't find array size added
- Blocked by Bug #9534: Incorrect printing of Linux BUILD_BUG_ON added
- Blocked by deleted (Bug #9533: Can't find array size)
- Blocked by deleted (Bug #9534: Incorrect printing of Linux BUILD_BUG_ON)
- Blocked by Bug #9537: Frama-C (CIL) reports strange error about type redefinition added
- Blocked by Bug #9543: Frama-C (CIL) dislikes large enumerators added
- Blocked by Bug #9544: Better support of fields declared using flexible array members added
- Blocked by Bug #9546: Frama-C (CIL) for GCC does not behave like GCC when casting ternary operators added
- 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.
- 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.
- Status changed from Closed to Open
- 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.
- Related to Bug #5323: Incorrect type for pointer in ___del_dma_pool added
Also available in: Atom