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
Reporterpascal 
Assigned Tovirgile 
PriorityhighSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
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 http://bts.frama-c.com [^]

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/log.ml", line 319, characters 10-11
Called from file "src/kernel/file.ml", line 852, characters 5-96
Called from file "src/kernel/file.ml", line 1008, characters 4-27
Re-raised at file "src/kernel/file.ml", line 1001, characters 23-44
Called from file "src/kernel/ast.ml", line 57, characters 29-45
Called from file "src/project/computation.ml", line 172, characters 17-21
Called from file "src/kernel/file.ml", line 1052, characters 2-14
Called from file "src/project/project.ml", line 379, characters 12-15
Re-raised at file "src/project/project.ml", line 384, characters 10-11
Called from file "src/toplevel/main.ml", line 43, characters 2-420
Called from file "src/toplevel/main.ml", line 56, characters 4-18
Re-raised at file "src/toplevel/main.ml", line 35, characters 2-797
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", 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
(0000340)
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.
(0000421)
pascal (reporter)
2009-09-29 09:20
edited on: 2009-09-29 09:45

More information:

1/ This is mentioned in http://c-faq.com/decl/decldef.html [^]

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 http://stackoverflow.com/questions/1433204 [^]


- 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 - 2017 MantisBT Team
Powered by Mantis Bugtracker