0000770: r12430, some assertions are localized at Cabs2cil_start:0 (csmith)

Frama-C Bug Tracking System - Frama-C
View Issue Details

ID	Project	Category	View Status	Date Submitted	Last Update
0000770	Frama-C	Kernel	public	2011-03-30 10:57	2014-02-12 16:59

Reporter	pascal
Assigned To	virgile
Priority	normal	Severity	minor	Reproducibility	always
Status	closed	Resolution	fixed
Platform		OS		OS Version
Product Version
Target Version		Fixed in Version	Frama-C Nitrogen-20111001

Summary	0000770: r12430, some assertions are localized at Cabs2cil_start:0 (csmith)
Description	bin/toplevel.opt -val -slevel 70000 -unspecified-access dummy_loc.i Result: ... Cabs2cil_start:0:[kernel] warning: Unspecified sequence with side effect: ... Cabs2cil_start:0:[kernel] warning: undefined multiple accesses in expression. assert \separated(l_934,& l_922); ... The attached file is pre-processed but it was made from ordinary .c and .h files on a Linux system (computation server).
Steps To Reproduce
Additional Information
Tags	No tags attached.
Relationships
Attached Files	dummy_loc.i (189,870) 2011-03-30 10:57 https://bts.frama-c.com/file_download.php?file_id=188&type=bug

Issue History
Date Modified	Username	Field	Change
2011-03-30 10:57	pascal	New Issue
2011-03-30 10:57	pascal	File Added: dummy_loc.i
2011-03-30 10:59	pascal	Status	new => assigned
2011-03-30 10:59	pascal	Assigned To	=> virgile
2011-03-31 10:43	svn	Checkin
2011-04-01 18:26	svn	Checkin
2011-04-01 18:26	svn	Status	assigned => resolved
2011-04-01 18:26	svn	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
2014-02-12 16:59		Note Added: 0004814
2014-02-12 16:59		Status	closed => resolved

Notes