Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000213Frama-CKernelpublic2009-08-06 20:172014-02-12 16:55
Assigned Tovirgile 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090601-beta1 
Target VersionFixed in VersionFrama-C Boron-20100401 
Summary0000213: crash in parser when double definition of variable in two different files, in some order
DescriptionManzana:frama-c pascal$ cat first_def.c int x; Manzana:frama-c pascal$ cat double_def.c int x=2; ~/frama-c-Beryllium-20090601-beta1/bin/toplevel.opt -metrics double_def.c first_def.c [kernel...] preprocessing with "gcc -C -E -I. double_def.c" [kernel...] preprocessing with "gcc -C -E -I. first_def.c" [kernel] internal error: Trying to add the same varinfo twice: x (vid:719) [kernel] error: kernel failed to complete because of an unexpected internal error. [kernel] error: please report at Backtrace obtained in bytecode, with -debug 1: [kernel] internal error: Trying to add the same varinfo twice: x (vid:719) Fatal error: exception Log.AbortFatal("kernel") Raised at file "src/kernel/", line 319, characters 10-11 Called from file "src/kernel/", line 852, characters 5-96 Called from file "src/kernel/", line 1008, characters 4-27 Re-raised at file "src/kernel/", line 1001, characters 23-44 Called from file "src/kernel/", line 57, characters 29-45 Called from file "src/project/", line 172, characters 17-21 Called from file "src/kernel/", line 1052, characters 2-14 Called from file "src/project/", line 379, characters 12-15 Re-raised at file "src/project/", line 384, characters 10-11 Called from file "src/toplevel/", line 43, characters 2-420 Called from file "src/toplevel/", line 56, characters 4-18 Re-raised at file "src/toplevel/", line 35, characters 2-797 Called from file "", line 134, characters 6-20 Called from file "src/kernel/", line 85, characters 4-35
Additional InformationIf you fail to reproduce, try changing the order of the two files.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
virgile (developer)
2009-08-17 18:39

The standard is not really clear on this subject: Based on 6.9.2 one could argue that int x; is a tentative definition which, in absence of other definition should be equivalent to int x = 0; (and thus should result in a clash with the definition of x in the other file). However, the example of this section seems to imply that we have an external declaration (as for a function), and thus that both x variables are linked to the same object. This is what gcc does.
pascal (reporter)
2009-09-29 09:20
edited on: 2009-09-29 09:45

More information: 1/ This is mentioned in 2/ This is mentioned in the C standard in informative Annex J as a common extension: J.5.11 Multiple external definitions There may be more than one external definition for the identifier of an object, with or without the explicit use of the keyword extern; if the definitions disagree, or more than one is initialized, the behavior is undefined (6.9.2). 3/ See also the top answer for

- Issue History
Date Modified Username Field Change
2009-08-06 20:17 pascal New Issue
2009-08-17 18:39 virgile Note Added: 0000340
2009-08-26 10:42 signoles Status new => acknowledged
2009-09-24 16:59 virgile Status acknowledged => assigned
2009-09-24 16:59 virgile Assigned To => virgile
2009-09-24 16:59 virgile Status assigned => acknowledged
2009-09-29 09:20 pascal Note Added: 0000421
2009-09-29 09:45 pascal Note Edited: 0000421
2010-02-10 15:09 svn Checkin
2010-02-10 15:09 svn Status acknowledged => resolved
2010-02-10 15:09 svn Resolution open => fixed
2010-04-13 15:30 signoles Status resolved => new
2010-04-13 15:31 signoles Status new => closed
2010-04-13 15:33 signoles Fixed in Version => Frama-C Boron

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker