Anonymous Login Frama-C issues should now be submitted on Frama-C's GitLab
2021-03-06 02:28 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000213Frama-CKernelpublic2014-02-12 16:55
Assigned Tovirgile 
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




virgile (developer)

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)

Last edited: 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
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
2013-12-19 01:13 Source_changeset_attached => framac master 44184f29
2014-02-12 16:55 Source_changeset_attached => framac stable/neon 44184f29
+Issue History