Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #1658

Closed
Open
Created Nov 07, 2009 by Pascal Cuoq@pascal

Precise widening when a loop condition involves a char or short

ID0000325: This issue was created automatically from Mantis Issue 325. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0000325 Frama-C Plug-in > Eva public 2009-11-07 2014-02-12
Reporter pascal Assigned To pascal Resolution fixed
Priority normal Severity feature Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Beryllium-20090902 Target Version - Fixed in Version Frama-C Boron-20100401

Description :

Depending the type of i, the range is not the same. The range of i in the loop is [0..10] (for int) or [0..15] for char or short.


void main(void) { char i=0; int j=0; while (i<10) i++; while (j<10) j++; }

[value] ====== VALUES COMPUTED ====== [value] Values for function main: i IN {10; 11; 12; 13; 14; 15; } j IN {10; }


Note that the AST for the two loops is different: i = (char)0; j = 0; while ((int )i < 10) {i = (char )((int )i + 1);} while (j < 10) {j ++;}

CIL transforms the code thus because the standard specifies that operators such as ++ do not operate on types smaller than int, and that values of these types are implicitly promoted to int in these conditions.

Meanwhile, in the absence of any loop-related option, the value analysis tries to keep computations short at the price of precision by using a technique called "widening". In order to limit the loss of precision, however, various heuristics are used, including a syntactic one for the j loop that recognizes that j IN [0..10] is a good candidate for the loop invariant.

These heuristic does not currently recognize the condition ((int )i < 10) as one where it would be valuable to try the same kind of invariant.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking