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
Assigned Tocmarche 
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é]

Using this code:
=== bidim_array.c
int a[12][45] = {0, };

//@ assigns a[..][..];
void f(void)
  a[1][3] = 42;

void main(void)

The assigns clause triggers an internal error in Jessie.

$ frama-c -jessie-analysis -jessie-gen-only bidim_array.c
[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/", 807, 33)

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