Table of Contents
caesar.adt - translation of LOTOS abstract data types into C
caesar.adt
[
-cc options] [
-comments] [
-debug] [
-depend] [
-english] [
-error] [
-external] [
-force]
[
-french] [
-functionality] [
-indent] [
-infix] [
-iso] [
-macro] [
-map] [
-more command]
[
-newstyle] [
-numeral integer] [
-oldstyle] [
-prefix] [
-silent] [
-trace] [
-verbose]
[
-version] [
-warning]
filename[
.lotos]
caesar.adt [Gar89c,GT93]
is a compiler that translates LOTOS abstract data types into executable
code. Quite often, the code generated is given as input to the
caesar
compiler, but it can also be used for other purpose.
Taking as input filename.lotos,
which contains a LOTOS specification, optionally accompanied by filename.t,
which contains hand-written C code, caesar.adt produces an output file filename.h
that contains C types and functions implementing the LOTOS sorts and operations
defined in filename.lotos.
Refer to the lotos
manual page for a detailed
description of the conventions to be followed by filename.lotos and filename.t.
- -cc options
- Pass options to the C compiler when it is invoked. options
is a list of compiler options (enclosed in quotes or double quotes). These
options are appended to the compiler options, if any, contained in the
$CADP_CC environment variable (see ENVIRONMENT VARIABLES below). Not a default
option.
- -comments
- Issue a warning message for each LOTOS sort or operation
which is not properly labelled by a special comment of the form
(*!...*). Not
a default option.
- -debug
- Generate extra C code that helps to debug partial
non-constructor definitions. When a C function aborts because the corresponding
LOTOS operation is not completely defined by its equations, the name of
the function and the actual values of its arguments are displayed. Not
a default option.
- -depend
- Display the list of library files included (directly
or transitively) in filename[.lotos] and stop. This list may be incomplete
if the LOTOS specification is syntactically incorrect. Not a default option.
- -english
- Print messages in English. Opposite of -french. This option overrides
the $CADP_LANGUAGE environment variable (see ENVIRONMENT VARIABLES below).
- -error
- A file, filename.err, is generated by caesar.adt. It contains detailed
error diagnostics. When it terminates, caesar.adt displays the content of
this file on the screen, using the $CADP/src/com/cadp_more command, unless
-error option is set.
- -external
- Generate a skeleton file filename.t.proto and/or
a skeleton file filename.f.proto if the LOTOS specification contains sorts
and/or operations declared
(*! external *). These skeleton files are incomplete,
but form a basis for producing filename.t and filename.f. They have to be
completed manually (at the places marked "...") with an implementation in
C for external sorts and constructors, and/or operations. Also, it may be
necessary to modify manually the order of C type declarations in order
to avoid forward references. Not a default option.
Note: if filename.t.proto
and/or filename.f.proto already exist in the current directory, caesar.adt
will not overwrite them, because they might have been modified manually.
- -force
- Force caesar.adt to regenerate filename.h even if not necessary. Not
a default option. By default caesar.adt will attempt not to regenerate filename.h
if this file already exists in the current directory, and if it has been
modified more recently than:
(1) the corresponding LOTOS file (filename.lotos, filename.lot, or filename.l),
(2) than any LOTOS library transitively included (using the "library" clause)
in this LOTOS file,
(3) than any C file included (using the "#include" clause) in filename.h
itself,
(4) than the filename.t file if this file exists in the current directory,
and
(5) than the filename.f file if this file exists in the current directory.
- -french
- Print messages in French. Opposite of -english. This option overrides
the $CADP_LANGUAGE environment variable (see ENVIRONMENT VARIABLES below).
Even when this option is set, some warning and error messages related to
lexical and syntactic analysis may still be displayed in English.
- -functionality
- Do not check functionality constraints (``
exit'' and ``noexit''). Not a default
option.
- -indent
- Do not format using the shell-script located in $CADP/src/com/cadp_indent
the generated file filename.h, nor the files filename.f.proto and filename.t.proto
generated by option -external. This option can be useful when the indent(1)
program invoked by cadp_indent crashes with a core dump, although cadp_indent
is designed to recover properly in such event. Not a default option.
- -infix
- Generate C code to print LOTOS binary operations in infix form when appropriate.
Not a default option.
- -iso
- Use the standard LOTOS semantics as defined in
ISO/IEC International Standard 8807, disabling the various language enhancements
mentioned in the section EXTENSIONS TO LOTOS of the lotos
manual
page and implemented in caesar.adt. Not a default option. Not to be used when
processing LOTOS specifications generated by lnt2lotos
- -macro
- Prevent
LOTOS non-constructor operations to be implemented by C macro-definitions
(
#define): all LOTOS non-constructor operations will be implemented as C
functions instead. Not a default option.
- -map
- Generate filename.map which gives
correspondence between sort and operation names occuring in filename.lotos
and C type and function names occuring in filename.h. Not a default option.
- -more command
- Use command to display the error messages, instead of "$CADP/src/com/cadp_more"
which is the default. command is a shell command (preferably enclosed in
quotes or double quotes) containing the pathname of the chosen pager, possibly
followed by a list of options. Not a default option.
- -newstyle
- In the generated
C code, use the new-style function declarations (i.e., with prototypes) introduced
in ANSI/ISO Standard C. Default option.
- -numeral integer
- Specify the range
of values to be used for implementing numeral sorts, i.e., all sorts S that
have two constructor operations F1 : -> S and F2 : S -> S, and are thus isomorphic
to natural numbers. If integer is greater than zero, the range of values
will be 0...(integer-1). If integer is less than zero, the range of values
will be 0...((2^(-integer))-1). With 64-bit versions of caesar.adt, the highest
positive values for integer are interpreted as the negative numbers -64,
-63, ..., -2, -1. By default, numeral sorts are represented using a single byte
(default value of integer is 256). This option does not apply to those numeral
sorts S for which filename.t defines a corresponding macro
CAESAR_ADT_HASH_....
-oldstyle In the generated C code, use the old-style function declarations
(i.e., without prototypes) available in Kerninghan and Ritchie C. Not a default
option.
- -prefix
- Generate C code that prints LOTOS binary operations always
in prefix form. Default option.
- -silent
- Execute silently. Opposite of -verbose.
Default option is -verbose.
- -trace
- Generate extra C code that traces all calls
and returns for a selected set of C functions. This option also sets the
-macro option. Not a default option.
- -verbose
- Print one line for each successive
phase performed by caesar.adt to inform the user about the progress of activities.
Opposite of -silent. Default option is -verbose.
- -version
- Display the current
version number of the software and stop. Not a default option.
- -warning
- Suppress
all warning messages, keeping (more severe) error messages, at the risk
of leaving undetected issues in the LOTOS specification. Not a default option.
The architecture of
caesar.adt
follows the principles
exposed in Section 1 of [GT93]. The translation from LOTOS to C proceeds
in several successive phases:
- - syntax analysis phase
- The LOTOS specification
is lexically and syntactically analyzed using a scanner and a parser that
have been generated by the SYNTAX tool of INRIA, which produces analyzers
that emit pertinent error messages and perform, as much as possible, automatic
error recovery. Incorrect LOTOS specifications are rejected; otherwise,
an abstract syntax tree is built. This phase is shared with caesar
- - semantic analysis phase
- The static semantics constraints of the standard
LOTOS definition are checked on the abstract syntax tree. This is done
in several steps: binding of processes, binding of gates, binding of types,
analysis of type signatures, binding of sorts, binding of variables, binding
of operations, and analysis of process functionality. The LOTOS specifications
not matching these constraints are rejected. This phase is also shared with
caesar
- - interface phase
- The abstract syntax tree is traversed and
its fragment that represents the abstract data types defined in the source
LOTOS specification is extracted and copied into the input tree, a simpler
syntax tree, which is itself specified using LOTOS abstract data types.
From this point, all the forthcoming translation steps are written in
LOTOS, meaning that the caesar.adt translator compiles itself (i.e., is bootstrapped).
- - verification phase
- The additional static semantics constraints listed
in the section "RESTRICTIONS ON THE DATA PART" of the lotos
manual
page are checked, and the LOTOS specifications not satisfying these constraints
are rejected.
- - type survey phase
- If a file named filename.t exists, an auxiliary
C program that includes this file is generated, compiled, and executed
so as to obtain information on how external LOTOS sorts are implemented
in filename.t. This phase may fail if the contents of filename.t are incorrect
or incomplete.
- - compilation phase
- The abstract sorts and operations represented
in the input tree are translated into concrete types and functions, which
are stored in the output tree, another syntax tree closer to imperative
languages, such as C.
- - optimization phase
- Various transformations are applied
to the output tree, so as to reduce the space taken by types and the time
spent in functions.
- - C translation phase
- The output tree is traversed and
decompiled to produce C code stored in filename.h.
- - indentation phase
- The
shell-script cadp_indent is invoked to format the generated file filename.h
unless option -indent is set.
- $CADP_LANGUAGE
- If this
variable is set, its value determines the language in which diagnostic
messages will be reported. Possible values are 'english' and 'french'. Incorrect
values will be ignored silently. If this variable is unset, it is given
the default value 'english'.
- $CADP_CC
- If this variable is set, its value
determines the name of the C compiler that will be invoked by caesar.adt.
See file $CADP/INSTALLATION_2 for detailed information about this variable.
If this variable is unset, the script-shell $CADP/src/com/cadp_cc will automatically
determine the C compiler to be used by default.
- $CADP_TMP
- If this variable
is set, its value determines the directory in which temporary files are
created. If this variable is unset, it is given the default value '/tmp'.
- $PAGER
- If this variable is set, its value will be used by the script-shell $CADP/src/com/cadp_more
to display error and warning messages.
When the source is erroneous,
error messages are issued. Exit status is 0 if everything is alright, 1
otherwise.
- filename.lotos
- LOTOS specification (input)
- filename.t
- external C implementation for types (input)
- filename.t.proto
- skeleton for
filename.t (output)
- filename.f
- external C implementation for functions (input)
- filename.f.proto
- skeleton for filename.f (output)
- filename.h
- C implementation
(output)
- filename.err
- detailed error messages (output)
- filename.map
- ADT correspondence
table (output)
- libname.lib
- user ADT library (input)
For simplicity, the
standard error stream is not used; all messages are written to the standard
output stream, which is made unbuffered. The file filename.err is created
at the beginning of execution and removed, if empty, at the end of execution.
- $CADP/lib/libname.lib
- predefined ADT library (input)
- $CADP/src/com/cadp_cc
- C compiler shell
- $CADP/src/com/cadp_more
- pager shell
- $CADP/LICENSE
- license
file
- $CADP_TMP/*.c
- C code generated during type survey (temporary)
- $CADP_TMP/*.x
- binary code for type survey (temporary)
- $CADP_TMP/*.tsv
- results of type
survey (temporary)
[Gar89c] Hubert Garavel. Compilation of
LOTOS Abstract Data Types. In Son T. Vuong, editor, Proceedings of the 2nd
International Conference on Formal Description Techniques (FORTE'89), Vancouver,
Canada. North Holland, pages 147-162, December 1989. Available from
http://cadp.inria.fr/publications/Garavel-89-c.html
[GT93] Hubert Garavel and Philippe Turlier. CAESAR.ADT : un compilateur pour
les types abstraits algebriques du langage LOTOS. In Rachida Dssouli and
Gregor v. Bochmann, editors, Actes du Colloque Francophone pour l'Ingenierie
des Protocoles (CFIP'93), Montreal, Canada, 1993. Available from http://cadp.inria.fr/publications/Garavel-Turlier-93.html
caesar
,
caesar.indent
,
lotos
lotos.open
,
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.
Please report bugs to
cadp@inria.fr
Table of Contents
