Project

General

Profile

Actions
Copy link

Bug #6629

closed

Used CIL is outdated

Added by Evgeny Novikov almost 9 years ago. Updated over 5 years ago.

Status:
Closed
Priority:
Normal
Assignee:
Evgeny Novikov
Category:
Addons
Target version:
3.0
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 3 (0 open — 3 closed)

Bug #9531: Environment models for void functions should not return any valuesClosedEvgeny Novikov03/13/2019

Actions
Feature #9532: Update CPAcheckerClosedEvgeny Novikov03/13/2019

Actions
Feature #9535: Increase memory limit for Frama-C (CIL)ClosedEvgeny Novikov03/13/2019

Actions

Related issues 8 (0 open — 8 closed)

Related to C Instrumentation Framework - Bug #5323: Incorrect type for pointer in ___del_dma_poolClosedEvgeny Novikov10/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 inefficientClosedMikhail Mandrykin03/07/2019

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

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

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

Actions
Blocked by Deductive Verification Tools for Linux Kernel - Bug #9544: Better support of fields declared using flexible array membersClosedMikhail Mandrykin03/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 operatorsClosedMikhail Mandrykin03/15/2019

Actions
Actions
Copy link
 #1

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.

Actions
Copy link
 #2

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.

Actions
Copy link
 #3

Updated by Evgeny Novikov over 5 years ago

Actions
Copy link
 #4

Updated by Evgeny Novikov over 5 years ago

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

Updated by Evgeny Novikov over 5 years ago

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

Updated by Evgeny Novikov over 5 years ago

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

Updated by Evgeny Novikov over 5 years ago

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

Updated by Evgeny Novikov over 5 years ago

Actions
Copy link
 #9

Updated by Evgeny Novikov over 5 years ago

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

Updated by Evgeny Novikov over 5 years ago

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

Updated by Evgeny Novikov over 5 years ago

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

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
Actions
Copy link
 #13

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.

Actions
Copy link
 #14

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.

Actions
Copy link
 #15

Updated by Evgeny Novikov over 5 years ago

  • Status changed from Closed to Open
Actions
Copy link
 #16

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.

Actions
Copy link
 #17

Updated by Evgeny Novikov over 5 years ago

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

Also available in: Atom PDF