5.6 Linkage Declarations

The syntax of a linkage-declaration is the same as in C++ [ANSI95]; these provide the ability to declare (and specify) the interfaces of functions written in other languages. See section 5.5 C++ Namespace and Using Declarations for the syntax of declaration-seq.

linkage-declaration ::= extern string-literal { [ declaration-seq ] }
        | extern string-literal declaration

For example, the following are examples of linkage-declarations. (See section 6 Function Specifications for explanations of the notation in the specifications.)

// @(#)$Id: linkage_declaration.lh,v 1.6 1997/06/03 20:30:12 leavens Exp $

extern "C" double ceil(double x);

extern "C" double floor(double x);
//@ behavior {
//@   ensures returns /\ x - 1 < result /\ result <= x;
//@ }

extern "C" {
  // @spec int seed_value;

  void srand(int seed);
  //@ behavior {
  //@   modifies seed_value;
  //@   ensures returns /\ assigned(seed_value, post) /\ seed_value' = seed;
  //@ }

  int rand();
  //@ behavior {
  //@   requires assigned(seed_value, pre);
  //@   ensures returns /\ 0 < result /\ result <= INT_MAX;
  //@ }
}

Go to the first, previous, next, last section, table of contents.