Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001074Frama-CPlug-in > Evapublic2012-01-28 11:342012-09-19 17:16
Reporteryakobowski 
Assigned Topascal 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001074: Imprecise result on almost deterministic program
Description----- memsetff.c --------
int t[10];

void main (char c) {
  for (int i=0;i<sizeof(t);i++)
    ((char*)t)[i]=0xFF;

  Frama_C_show_each(t[1]);

  if(c)
    t[1] = 1;
}
------------------------
To be tested with
frama-c -val memsetff.c -precise-unions -big-ints-hex 0x10 -slevel 100000
(-precise-unions has not effect in this case)

The obtained possible values for t[1] are [1] ? [--..--], which is over-approximated.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0002636)
pascal (reporter)
2012-01-28 11:43

 Offsetmaps do not have a lattice structure. Improving things here mean making them worse somewhere else, unless we are careful and make sure that the new treatment is only applied when it gains information, and not when it loses information.

Here is a program for which is would be easy to provide a less precise result:

int a, b;
char t[2];

int main(int c)
{
  t[0] = (int) &a;
  t[1] = (int) &b;
  if (c) *(short*)t = 12;
}

It currently gives:

          t[0] IN {{ garbled mix of &{a} (origin: Arithmetic {t.c:6}) }}
           [1] IN {{ garbled mix of &{b} (origin: Arithmetic {t.c:7}) }}

But with the wrong change, it could give garbled mix of &{a, b} for both elements in t.
(0002637)
yakobowski (manager)
2012-01-28 12:04
edited on: 2012-01-28 17:18

 > Offsetmaps do not have a lattice structure.

Sure. The question is now along this line: does choosing one strategy for join in some cases, and another in some other cases, break some invariant of the abstract interpretation mechanism (ie. "sorry, the analysis is precise, bot does no longer converge"), or can we safely improve the heuristics?
(0002638)
pascal (reporter)
2012-01-28 12:11

 > does choosing one strategy for join in some cases, and another in some other cases, break some invariant

Nothing gets any more broken than it already is, as far as I can tell.

The obvious heuristic is when joining [0..15] -> a on the one hand and [0..7] -> b, [8..15] -> c on the other hand, if b and c are included in V_Or_Uninitialized.top_int.

A more general heuristic is when b and c's value components are included in V.top_int, and have the same indeterminateness flags.

- Issue History
Date Modified Username Field Change
2012-01-28 11:34 yakobowski New Issue
2012-01-28 11:34 yakobowski Status new => assigned
2012-01-28 11:34 yakobowski Assigned To => pascal
2012-01-28 11:34 yakobowski Reproducibility have not tried => always
2012-01-28 11:34 yakobowski Product Version Frama-C GIT, precise the release id => Frama-C Nitrogen-20111001
2012-01-28 11:43 pascal Note Added: 0002636
2012-01-28 12:04 yakobowski Note Added: 0002637
2012-01-28 12:11 pascal Note Added: 0002638
2012-01-28 17:18 yakobowski Note Edited: 0002637
2012-01-30 14:11 svn Checkin
2012-01-30 14:11 svn Status assigned => resolved
2012-01-30 14:11 svn Resolution open => fixed
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker