Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000032Frama-CPlug-in > jessiepublic2009-04-07 15:192009-04-10 10:23
Reportervirgile 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Lithium-20081201 
Target VersionFixed in Version 
Summary0000032: Internal error with assign specification on bi-dimensional arrays
Description[bug 7435 from old bts, reported by David Mentré] Hello, Using this code: === bidim_array.c int a[12][45] = {0, }; //@ assigns a[..][..]; void f(void) { a[1][3] = 42; } void main(void) { f(); } === The assigns clause triggers an internal error in Jessie. $ frama-c -jessie-analysis -jessie-gen-only bidim_array.c Parsing [preprocessing] running gcc -C -E -I. -include /usr/local/stow/frama-c-lithium-2008-12-01/share/frama-c/jessie/jessie_prolog.h -dD bidim_array.c Cleaning unused parts Symbolic link Starting semantical analysis Starting Jessie translation Fatal error: exception Assert_failure("src/jessie/interp.ml", 807, 33) Yours, d.
Additional InformationNormalization of multi-dimensional array accesses in jessie plugin is not compatible with use of range.
TagsNo tags attached.
Attached Files

- Relationships
related to 0000185assignedcmarche Frama-C cannot process properly arrays of structures 
related to 0001093assignedcmarche Passing multi-dimensional arrays via reference fails 

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2009-04-07 15:19 virgile New Issue
2009-04-07 15:42 signoles Status new => acknowledged
2009-04-10 10:23 signoles Status acknowledged => assigned
2009-04-10 10:23 signoles Assigned To => cmarche
2009-07-17 11:40 virgile Relationship added related to 0000185
2012-02-14 09:05 virgile Relationship added related to 0001093


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker