Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000905Frama-CPlug-in > slicingpublic2011-07-31 12:592011-12-19 10:04
Reporterpascal 
Assigned ToAnne 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000905: 14403: last slicing bug (csmith)
DescriptionThe value analysis does not find any alarm and finds the values below

~/ppc/bin/toplevel.opt -val-signed-overflow-alarms -no-val-show-progress -cpp-command "gcc -m32 -E -C -I runtime -D__FRAMAC" -no-results -slevel 100000 -machdep x86_32 s.31013054.p.c -val


[value] Called Frama_C_show_each({3781742995})
[value] Called Frama_C_show_each({4095739724})
[value] Called Frama_C_show_each({550094235})
[value] Called Frama_C_show_each({252820852})
[value] Called Frama_C_show_each({624713289})
[value] Called Frama_C_show_each({1426802424})
[value] Called Frama_C_show_each({397183221})
[value] Called Frama_C_show_each({320991826})
[value] Called Frama_C_show_each({1015897994})
[value] Called Frama_C_show_each({3069753974})
[value] Called Frama_C_show_each({4276963908})
[value] Called Frama_C_show_each({1968234281})
[value] Called Frama_C_show_each({1968234281})

Executing (32-bit) finds the same values as above.

But the program sliced with:

~/ppc/bin/toplevel.opt -val-signed-overflow-alarms -no-val-show-progress s.31013054.p.i -slice-calls Frama_C_show_each -slevel 5000 -slevel-function crc32_gentab:0 -then-on 'Slicing export' -print -ocode res.c

$ gcc -m32 res.c show_each.c
$ ./a.out
[value] Called Frama_C_show_each({3781742995})
[value] Called Frama_C_show_each({4095739724})
[value] Called Frama_C_show_each({550094235})
[value] Called Frama_C_show_each({252820852})
[value] Called Frama_C_show_each({624713289})
[value] Called Frama_C_show_each({1426802424})
[value] Called Frama_C_show_each({397183221})
[value] Called Frama_C_show_each({320991826})
[value] Called Frama_C_show_each({1015897994})
[value] Called Frama_C_show_each({1148365541})
[value] Called Frama_C_show_each({3051573531})
[value] Called Frama_C_show_each({2309422687})
[value] Called Frama_C_show_each({2309422687})
Additional InformationLe bug a pris 36h * 5 processeurs pour se montrer, ce sera presque sûrement le dernier, sauf si tu en introduis un nouveau en corrigeant celui-ci :)

1015897994 est la dernière valeur correcte. Cela indique une différence dans la valeur finale de g_89[2].
TagsNo tags attached.
Attached Filestgz file icon p.tgz [^] (71,831 bytes) 2011-07-31 12:59

- Relationships

-  Notes
(0002260)
Anne (reporter)
2011-09-13 16:56

Seems to be fixed in rev 15113

- Issue History
Date Modified Username Field Change
2011-07-31 12:59 pascal New Issue
2011-07-31 12:59 pascal Status new => assigned
2011-07-31 12:59 pascal Assigned To => Anne
2011-07-31 12:59 pascal File Added: p.tgz
2011-09-13 16:56 Anne Note Added: 0002260
2011-09-13 16:56 Anne Status assigned => resolved
2011-09-13 16:56 Anne 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
2011-12-19 10:03 pascal Status closed => feedback
2011-12-19 10:03 pascal Resolution fixed => reopened
2011-12-19 10:04 pascal Status feedback => closed
2011-12-19 10:04 pascal Resolution reopened => fixed
2011-12-19 10:04 pascal View Status private => public


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker