Project

General

Profile

Bug #6629

Used CIL is outdated

Added by Evgeny Novikov almost 4 years ago. Updated 7 months ago.

Status:
Closed
Priority:
Normal
Category:
Addons
Target version:
Start date:
03/13/2019
Due date:
% Done:

100%

Estimated time:
(Total: 0.00 h)
Detected in build:
svn
Platform:
Published in build:

Description

At the moment version 1.5.1 is used. It was released on 14 Jul 2012. See the official CIL page.


Subtasks

Bug #9531: Environment models for void functions should not return any valuesClosedEvgeny Novikov

Actions
Feature #9532: Update CPAcheckerClosedEvgeny Novikov

Actions
Feature #9535: Increase memory limit for Frama-C (CIL)ClosedEvgeny Novikov

Actions

Related issues

Related to C Instrumentation Framework - Bug #5323: Incorrect type for pointer in ___del_dma_poolClosed10/08/2014

Actions
Blocks Klever - Bug #6775: Well known CIL issuesRejected02/03/2016

Actions
Blocked by Deductive Verification Tools for Linux Kernel - Feature #9519: Frama-C CIL is too inefficientClosed03/07/2019

Actions
Blocked by Klever - Feature #9536: Update CIFClosed03/13/2019

Actions
Blocked by Deductive Verification Tools for Linux Kernel - Bug #9537: Frama-C (CIL) reports strange error about type redefinitionClosed03/13/2019

Actions
Blocked by Deductive Verification Tools for Linux Kernel - Bug #9543: Frama-C (CIL) dislikes large enumeratorsClosed03/14/2019

Actions
Blocked by Deductive Verification Tools for Linux Kernel - Bug #9544: Better support of fields declared using flexible array membersClosed03/14/2019

Actions
Blocked by Deductive Verification Tools for Linux Kernel - Bug #9546: Frama-C (CIL) for GCC does not behave like GCC when casting ternary operatorsClosed03/15/2019

Actions

History

#1

Updated by Evgeny Novikov about 1 year ago

  • 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.

#2

Updated by Evgeny Novikov 9 months 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.

#3

Updated by Evgeny Novikov 9 months ago

#4

Updated by Evgeny Novikov 9 months ago

  • Blocked by Bug #9533: Can't find array size added
#5

Updated by Evgeny Novikov 9 months ago

  • Blocked by Bug #9534: Incorrect printing of Linux BUILD_BUG_ON added
#6

Updated by Evgeny Novikov 9 months ago

  • Blocked by deleted (Bug #9533: Can't find array size)
#7

Updated by Evgeny Novikov 9 months ago

  • Blocked by deleted (Bug #9534: Incorrect printing of Linux BUILD_BUG_ON)
#8

Updated by Evgeny Novikov 9 months ago

#9

Updated by Evgeny Novikov 9 months ago

  • Blocked by Bug #9537: Frama-C (CIL) reports strange error about type redefinition added
#10

Updated by Evgeny Novikov 9 months ago

  • Blocked by Bug #9543: Frama-C (CIL) dislikes large enumerators added
#11

Updated by Evgeny Novikov 9 months ago

  • Blocked by Bug #9544: Better support of fields declared using flexible array members added
#12

Updated by Evgeny Novikov 9 months ago

  • Blocked by Bug #9546: Frama-C (CIL) for GCC does not behave like GCC when casting ternary operators added
#13

Updated by Evgeny Novikov 9 months 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.

#14

Updated by Evgeny Novikov 9 months 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.

#15

Updated by Evgeny Novikov 7 months ago

  • Status changed from Closed to Open
#16

Updated by Evgeny Novikov 7 months 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.

#17

Updated by Evgeny Novikov 7 months ago

  • Related to Bug #5323: Incorrect type for pointer in ___del_dma_pool added

Also available in: Atom PDF