0002507: Frama-C reports “invalid ghost in extern linkage specification” while loading files

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0002507

Frama-C

Kernel

public

2020-06-06 23:39

2020-10-06 10:00

Reporter

dgenin

Assigned To

AllanBlanchard

Priority

normal

Severity

major

Reproducibility

have not tried

Status

closed

Resolution

no change required

Platform

x86

Ubuntu

OS Version

19.10

Product Version

Frama-C 20-Calcium

Target Version

Fixed in Version

Summary

0002507: Frama-C reports “invalid ghost in extern linkage specification” while loading files

Description

As I try to load my project files Frama-C reports the following error in the Console window and stops processing

  [kernel] FRAMAC_SHARE/libc/__fc_alloc_axiomatic.h:30:
  invalid ghost in extern linkage specification:
  Location: between lines 30 and 45, before or at token: }
  28 #include "__fc_define_wchar_t.h"
  29

  30 __BEGIN_DECLS
  31
  32 /*@ ghost extern int __fc_heap_status __attribute__((FRAMA_C_MODEL)); */
  33
  34 /*@ axiomatic dynamic_allocation {
  35 @ predicate is_allocable{L}(integer n) // Can a block of n bytes be allocated?
  36 @ reads __fc_heap_status;
  37 @ // The logic label L is not used, but it must be present because the
  38 @ // predicate depends on the memory state
  39 @ axiom never_allocable{L}:
  40 @ \forall integer i;
  41 @ i < 0 || i > __FC_SIZE_MAX ==> !is_allocable(i);
  42 @ }
  43 */
  44
  45 __END_DECLS

  46
  47 __POP_FC_STDLIB

Steps To Reproduce

not sure

Tags

No tags attached.

Attached Files

Relationships

Relationships

Notes
~0006978 dgenin (reporter) 2020-06-09 17:13	I traced the issue to the case of the file extension. It seems that if the file extension is .C the file is interpreted as C++ (maybe) and including stdlib.h causes the fault. I haven't checked if other librareris cause an issue. If the extension is .c then the file is interpreted as plain C and the file loads normally.

~0006980 AllanBlanchard (developer) 2020-10-06 10:00	This indeed due to the fact that the `.C` is seen as a C++ file. Note that for C++, an experimental Front-end is available: Frama-Clang.

Notes

Date Modified	Username	Field	Change
Issue History
2020-06-06 23:39	dgenin	New Issue
2020-06-09 17:13	dgenin	Note Added: 0006978
2020-10-06 10:00	AllanBlanchard	Note Added: 0006980
2020-10-06 10:00	AllanBlanchard	Status	new => closed
2020-10-06 10:00	AllanBlanchard	Assigned To	=> AllanBlanchard
2020-10-06 10:00	AllanBlanchard	Resolution	open => no change required

Issue History