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
0000844Frama-CPlug-in > Evapublic2011-05-28 23:452011-10-10 14:14
Reporteryakobowski 
Assigned Topascal 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000844: Incorrect results with low slevel
DescriptionThe following program is correct and always terminates. However, with no slevel, the value analysis incorrectly states that main and memset do not terminate. (Analyzed with -value -slevel 0) void* memset (void* dest, int val, unsigned int len) { unsigned char *ptr = (unsigned char*)dest; while (len-- > 0) { *ptr++ = val; } return dest; } extern int k; void main () { int v; int x = k ? 2 : 3; memset(&v,42,x); }
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0001932)
pascal (reporter)
2011-05-29 00:30
edited on: 2011-05-29 00:30

 I note that you have not disabled relations yet. alu:~ pascal$ svn diff ~/ppc Index: /Users/pascal/ppc/src/value/eval.ml =================================================================== --- /Users/pascal/ppc/src/value/eval.ml (revision 13685) +++ /Users/pascal/ppc/src/value/eval.ml (working copy) @@ -304,7 +304,7 @@ (struct let name = "UseRelations" let dependencies = [] let kind = `Internal - let default () = true + let default () = false end) let () = alu:~ pascal$ ~/ppc/bin/toplevel.byte -val u.c ... [value] Values for function main: X ? {0; 1} len ? {0; 1; 2; 4294967295} alu:~ pascal$ cat u.c int X; main(int c, int d, int e){ unsigned len; len = c ? 0 : (e ? 1 : (d ? 2 : 3)); { unsigned int tmp_0 = len; len--; if (! (tmp_0 > (unsigned int)0)) { X=1; } } return X; } alu:~ pascal$ ~/ppc/bin/toplevel.opt -val u.c # old version [value] Values for function main: len ? {0; 1; 2}
(0001933)
pascal (reporter)
2011-05-29 01:49

 Fixed in 13686 (relations disabled)

- Issue History
Date Modified Username Field Change
2011-05-28 23:45 yakobowski New Issue
2011-05-28 23:45 yakobowski Status new => assigned
2011-05-28 23:45 yakobowski Assigned To => pascal
2011-05-29 00:30 pascal Note Added: 0001932
2011-05-29 00:30 pascal Note Edited: 0001932
2011-05-29 01:49 pascal Note Added: 0001933
2011-05-29 01:49 pascal Status assigned => resolved
2011-05-29 01:49 pascal Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker