0000905: 14403: last slicing bug (csmith) - Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0000905

Frama-C

Plug-in > slicing

public

2011-07-31 12:59

2011-12-19 10:04

Reporter

pascal

Assigned To

Anne

Priority

normal

Severity

minor

Reproducibility

have not tried

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C GIT, precise the release id

Target Version

Fixed in Version

Frama-C Nitrogen-20111001

Summary

0000905: 14403: last slicing bug (csmith)

Description

The 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 Information

Le 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].

Tags

No tags attached.

Attached Files

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