Anonymous | Login | Signup for a new account | 2019-12-07 05:07 CET | ![]() |
Main | My View | View Issues | Change Log | Roadmap | Repositories |
View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
0001074 | Frama-C | Plug-in > Eva | public | 2012-01-28 11:34 | 2012-09-19 17:16 | ||||
Reporter | yakobowski | ||||||||
Assigned To | pascal | ||||||||
Priority | normal | Severity | major | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Platform | OS | OS Version | |||||||
Product Version | Frama-C Nitrogen-20111001 | ||||||||
Target Version | Fixed in Version | Frama-C Oxygen-20120901 | |||||||
Summary | 0001074: Imprecise result on almost deterministic program | ||||||||
Description | ----- memsetff.c --------
int t[10];
void main (char c) {
for (int i=0;i | ||||||||
Tags | No tags attached. | ||||||||
Attached Files | |||||||||
![]() |
|
(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. |
![]() |
|||
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 |