CAESAR.OPEN manual page
Table of Contents

Name

caesar.open - OPEN/CAESAR connection for the LOTOS language

Synopsis

caesar.open [-link|-include] [caesar_opt] spec[.lotos] [cc_opt] user[.a|.c|.o] [user_opt]

Description

Taking as input a LOTOS program spec.lotos and an OPEN/CAESAR program user[.a|.c|.o], caesar.open generates an executable program user. To do so, caesar.open performs appropriate calls to caesar , caesar.adt , and the C compiler, avoiding recompilation whenever possible. Finally, user is executed.

According to the principles of the OPEN/CAESAR architecture, user is obtained by combining three different modules:

Processing of the Graph Module

caesar.open automatically invokes caesar if the graph module spec.c does not exist or is out of date.

caesar.open automatically invokes caesar.adt if the abstract data type implementation spec.h does not exist or is out of date. However, if spec.h exists and has not been generated using caesar.adt , it will not be overwritten, even if it is out of date (in this case, a warning is issued).

caesar.open takes into account the dependencies possibly created by spec.c, spec.h, spec.t, and spec.f.

Processing of the Exploration Module

The exploration module user[.a|.c|.o] is supposed to contain an OPEN/CAESAR application program, such as exhibitor , terminator , xsimulator ...

The exploration module can be supplied in three different forms. It can be either an archive file (with .a suffix), or a source C program (with .c suffix) or an object code file (with .o suffix).

If user.a is not present in the current directory, caesar.open attempts to fetch it in the OPEN/CAESAR binary library $CADP/bin.`arch`.

If user.c is not present in the current directory, caesar.open attempts to fetch it in the OPEN/CAESAR source library $CADP/src/open_caesar.

If user.o is not present in the current directory, caesar.open attempts to fetch it in the OPEN/CAESAR binary library $CADP/bin.`arch`.

If no suffix (.a, .c, .o) is specified on the command line for the exploration module user, caesar.open will make successive attempts to fetch this exploration module: first, as a source C program with .c suffix; then as an archive file with .a suffix; finally as an object code file with suffix .o.

Determination of Include or Link Mode

If the exploration module is in source form, caesar.open examines user.c in order to determine automatically whether link mode or include mode should be used.

If the exploration module is in archive form or in object code form, only the link mode is allowed.

Options

-include
Select include mode. Not a default option.

-link      
Select link mode. Default option.

The options caesar_opt, if any, are passed to caesar and to caesar.adt .

The options cc_opt, if any, are passed to the C compiler.

The options user_opt if any, are passed to user.

Examples:

caesar.open spec.lotos -O user.a
or
caesar.open spec.lotos -O user.c
or
caesar.open spec.lotos -O user.o
or
caesar.open -comments -gc spec.lotos user -size 1000

Exit Status

When the source is erroneous, error messages are issued. Exit status is 0 if everything is alright, 1 otherwise.

Author

Hubert Garavel (INRIA Rhone-Alpes)

Operands

spec.lotos
LOTOS specification (input)

spec.h      
implementation in C of data types

spec.t      
external type C implementation

spec.f      
external function C implementation

spec.c      
graph module gen. by CAESAR from spec.lotos      

spec.o      
object code gen. by the C compiler. from spec.c      

user.a      
exploration module (archive, input)

user.c      
exploration module (source, input)

user.o      
exploration module (object code, input)

user      
executable program (output)

Files

/tmp/caesar.open.*
temporary files

$CADP/incl/caesar_graph.h
interface of the graph module

$CADP/incl/caesar_*.h
interfaces of the storage module

$CADP/bin.`arch`/libcaesar.a
object code of the storage module

$CADP/src/open_caesar/*.c
library of exploration modules (source)

$CADP/bin.`arch`/*.a
library of exploration modules (archive)

$CADP/bin.`arch`/*.o
library of exploration modules (object code)

See Also

OPEN/CAESAR Reference Manual, caesar , caesar.adt , lotos

Additional information is available from the CADP Web page located at http://cadp.inria.fr

Directives for installation are given in files $CADP/INSTALLATION_*.

Recent changes and improvements to this software are reported and commented in file $CADP/HISTORY.

Bugs

Please report new bugs to Hubert.Garavel@inria.fr


Table of Contents