TRAIAN 3.5 released on October 29, 2021

The CONVECS team is pleased to announce that version 3.5 of the TRAIAN compiler for LOTOS NT is available.

Release Notes

TRAIAN 3.5 has been prepared by Hubert Garavel, Frederic Lang, and Wendelin Serwe. It was released four months after version 3.4 of TRAIAN.

TRAIAN 3.5 brings two language changes, four code-generation changes, twenty-four static-semantics changes, and ten bug fixes (see below their description).

Language Changes

TRAIAN 3.5 introduces various changes to the LOTOS NT language in order to further align it with the LNT language supported by the CADP toolbox. The LOTOS NT Reference Manual and the style files for text editors have been updated to reflect these changes.

The syntax of LOTOS NT was extended with "in var" and "out var" parameters in LOTOS NT. Parameters declared "in var" are "in" parameters that can be assigned in the function body. Parameters declared "out var" are "out" parameters that can be used (after being assigned) in the function body. See item 306 in the HISTORY.txt file.

The "!implementedby", "!comparedby", "!printedby", and "!enumeratedby" pragmas of LOTOS NT to allow identifiers prefixed with "C:" or "LOTOS:". See item 322 in the HISTORY.txt file.

Code-Generation Changes

The "lotosnt_predefined.h" library was enhanced as follows:
- The NULL macro is no longer defined.
- The NULL_ADT_NONE macro is no longer defined (the C code generated using TRAIAN 3.4 needs to be recompiled using TRAIAN 3.5).
- Many identifiers named TRAIAN_ADT_* have been removed or renamed; for instance, TRAIAN_ADT_SINGLETON was renamed to TRAIAN_SINGLETON.
- TRAIAN_ADT_MATCH_TRUE was incorrectly named and was renamed to TRAIAN_MATCH_ADT_TRUE.
See item 287 in the HISTORY.txt file.

The code libraries and the C code generated by TRAIAN have been enhanced in several ways:
- Extra spaces and newlines have been deleted.
- Missing spaces and newlines have been inserted.
- All occurrences of stderr have been replaced with stdout, to be aligned with the conventions of the CADP toolbox.
- A call to "exit (1)" was replaced by a call to "raise (15)", according to the conventions of the CADP toolbox.
- The definition of TRAIAN_ADTI_raise_event() in file "lotosnt_exceptions.h" was simplified by removing some dead code and by adding "__attribute__ ((noreturn))" for Gcc.
- The C code generated by TRAIAN was simplified by removing some dead code after calling TRAIAN_ADTI_not_reached().
See item 289 in the HISTORY.txt file.

The C code generated by TRAIAN to avoid "-Wclobbered" warnings emitted by Gcc. See item 291 in the HISTORY.txt file.

The predefined libraries and the C code generated by TRAIAN have been modified to make sure that the result of all memory allocations, using either malloc() or calloc(), is properly checked against the NULL pointer. In particular, the C code for converting LOTOS NT values to character strings, for allocating hash tables, and for creating exceptions has been made safer. See item 312 in the HISTORY.txt file.

Static-Semantics Changes

An irrelevant warning inherited from TRAIAN 2.*:
```
   variable X not assigned in this branch but in some other branch(es)
```
was removed. On the one hand, this warning was incompletely implemented, as certain situations were not reported. On the other hand, removing this warning allows one to write LOTOS NT code more freely, without being forced to assign the same variables in all branches of "if", "case", and "trap" instructions. See item 292 in the HISTORY.txt file.

A new warning was added:
```
   handler for event E never executed
```
to report when a "trap" instruction has a handler for some event E but does not raise E in its body, e.g.,
```
   trap 
      exception E is ... 
   in
      return false
   end trap
```
See item 295 in the HISTORY.txt file.

A new warning was added:
```
   event parameter E never used
```
to draw attention to functions declaring an event parameter that is not used in the body of the function. See item 296 in the HISTORY.txt file.

A new warning was added:
```
   variable parameter X never used
```
to report when a function declares a variable parameter X that is not used in the body of the function. See item 297 in the HISTORY.txt file.

A new warning was added:
```
   useless assignment to X
```
to report about variables that are assigned values never used later. To avoid such warnings, the existing LOTOS NT code needs to be cleaned up in various ways:
- Useless assignments, many of which were required by former versions of TRAIAN, should be removed.
- Useless occurrences of variables in patterns (i.e., free variables whose value is not used later) should be replaced with "any".
- "use" instructions can be added to silence these warnings.
See item 298 in the HISTORY.txt file.

A new warning was added:
```
   loop label L never used
```
to draw attention to loops that are declared with a label L and whose body contains no "break L" instruction. See item 300 in the HISTORY.txt file.

The data-flow analysis of TRAIAN better detects infinite loops nested in other loops. For instance, the following LOTOS NT program:
```
   function F (...) : BOOL is
      loop L in
         loop
	    null
         end loop
      end loop;
      return false
   end function
```
now triggers the following warning for its "return" line:
```
   dead code after infinite loop
```
See item 301 in the HISTORY.txt file.

The data-flow analysis of TRAIAN for "break" instructions was made more precise. See item 304 in the HISTORY.txt file.

A new warning was added:

   "in" parameter X overwritten before used (should be a local variable)

See item 307 in the HISTORY.txt file.

A new warning was added:

   "in out" parameter X never modified (should be an "in" parameter)

See item 308 in the HISTORY.txt file.

A new warning was added:

   "in out" parameter X overwritten before used (should be an "out" parameter)

See item 309 in the HISTORY.txt file.

A new warning was added:

   "in" parameter X modified (should be an "in var" parameter)

See item 310 in the HISTORY.txt file.

A new warning was added:

   "out" parameter X both used and modified (should be an "out var" parameter)

See item 311 in the HISTORY.txt file.

The data-flow analysis of TRAIAN was modified, so that the following warning:
```
   variable parameter X never used
```
is also emitted for "in var" parameters, as well as for "in" parameters. See item 313 in the HISTORY.txt file.

Two new warnings have been added:

   "in var" parameter X never modified (should be an "in" parameter)

and

   "in var" parameter X overwritten before used (should be a local variable)

See item 314 in the HISTORY.txt file.

Two new warnings have been added:

   "out var" parameter X never used (should be an "out" parameter)

and

   "in out" parameter X overwritten before used (should be an "out var" parameter)

See item 315 in the HISTORY.txt file.

The former TRAIAN warning:

   infinite loop inside another loop

was replaced by a new, simpler warning:

   infinite loop

that is triggered more frequently, due to the more precise data-flow analysis performed by TRAIAN. For instance, this warning is now triggered by the following LOTOS NT programs:

   function F1 is
      var N : int in
         N := 0;
         loop
	    N := N + 1
         end loop
      end var
   end function

   function F2 is
      loop
         trap
	    exception E is null
         in
	    raise E
         end trap
      end loop
   end function

See item 316 in the HISTORY.txt file.

The data-flow analysis of TRAIAN was enhanced to take pre-conditions ("require") and post-conditions ("ensure") into account for determining the set of used LOTOS NT variables. The same change was done in LNT2LOTOS. See item 317 in the HISTORY.txt file.

A new warning was added:
```
   loop body is executed at most once
```
to detect "loop" instructions that are useless because the loop body is executed zero or one time at most, due to "break", "raise", or "return" instructions (or nested infinite loops as well) that are necessarily executed, e.g.:
```
   loop
      raise E
   end loop
```
See item 318 in the HISTORY.txt file.

A new warning was added:

   function with "out" parameter(s) but no normal termination

which is emitted for functions such as:

   function F1 [E : none] (out X : BOOL) is
      X := true;
      raise E
   end function

   function F2 (out var X : Int) is
      X := 0;
      loop
         X := X + 1
      end loop
   end function

This warning replaces an error message:

   function F may return without assigning parameter X

that was too restrictive. See item 319 in the HISTORY.txt file.

A new warning was added:

   function with "in out" parameter(s) but no normal termination

See item 320 in the HISTORY.txt file.

A new warning was added:

   function with result but no normal termination

which is emitted for LOTOS NT programs such as:

   function G [E : none] : bool is
      raise E
   end function

See item 321 in the HISTORY.txt file.

Gate typing of actions in LOTOS NT process definitions has been implemented. Previously, TRAIAN required that all actions had the channel "any", leading to the rejection of correct LOTOS NT processes. For instance:
```
    process MAIN is
       i
    end process
```
is now accepted by TRAIAN, whereas it was previously rejected with a error message:
```
   event i is declared with channel NONE instead of any
```
See item 323 in the HISTORY.txt file.

The TRAIAN warnings have been enhanced to give more complete explanations about the reason why some LOTOS NT code fragments are dead. For instance, the following program:

   function F [E : none] (X : BOOL) : BOOL is
      if X then
         loop
	    null
         end loop
      else
         raise E
      end if;
      return X -- warning here
   end function

will trigger a warning of the form:

   dead code after infinite loop and "raise" instruction

whereas the following code fragment:

   function F (X : BOOL) : BOOL is
      loop L in
         if X then
	    return TRUE
         else
	    break L
         end if;
         return X -- warning here
      end loop;
      return FALSE
   end function

will trigger a warning of the form:

   dead code after "break" and "return" instruction

See item 324 in the HISTORY.txt file.

Bug Fixes

A few C files of demos 01 and 02 had not been updated with respect to the changes brought to TRAIAN 3.4, namely the renaming of TRAIAN_ADT_EQ_*, TRAIAN_ADT_PRINT_*, and TRAIAN_ADT_TYPE_* to TRAIAN_EQ_*, TRAIAN_PRINT_*, and TRAIAN_TYPE_*, respectively. See item 285 in the HISTORY.txt file.

A few LOTOS NT files of demos 02 and 04 had not been updated with respect to the changes brought to TRAIAN 3.4, namely the removal of redundant "in" keywords in "case" instructions. See item 286 in the HISTORY.txt file.

The data-flow analysis of TRAIAN 3.4 accepted incorrect LOTOS NT programs, e.g.:
```
   function F (a, b, c, d : int, out q1, q2 : int) : nat
   is
      trap
	 exception E1 is return 1
	 exception E2 is return 2
      in
	 q1 := a div[E1] b;
	 q2 := c div[E2] d
      end trap;
      return 0
   end function
```
This program is now rejected with an error message stating that q1 and q2 may be, in certain cases, uninitialized when F returns. Also, some irrelevant warnings of the form:
```
   variable X not assigned in this branch but in some other branch(es)
```
have been suppressed. See item 288 in the HISTORY.txt file.

The data-flow analysis of TRAIAN 3.4 rejected some correct LOTOS NT programs with error messages of the form:

   variable X may be uninitialized

For instance, the following programs are now accepted:

   function F1 (X : NAT) : NAT is
      var N : NAT in
         if X == 0 then
   	 return 1
         else
   	 N := X + 1
         end if;
         return N
         -- there was an error: variable N may be uninitialized
      end var
   end function
   
   function F2 (X : NAT) : NAT is
      var N : NAT in
         case X in
   	 0 -<
   	    return 1
         |  N -lt;
   	    N := N + 1
         end case;
         return N
         -- there was an error: variable N may be uninitialized
      end var
   end function
   
   function F3 (X : NAT) : NAT is
      var N : NAT in
         trap
   	 exception E is
   	    N := 0
         in
   	 case X -[E] 1 in
   	    0 -<
   	       return 1
   	 |  N -<
   	       N := N + 1
   	 end case
         end trap;
         return N
         -- there was an error: variable N may be uninitialized
      end var
   end function
   
   function F4 [E : none] (X : int) : bool is
      var Y : bool in
         if X < 0 then
            raise E
         else
            Y := X + 1
         end if ;
         return Y
         -- there was an error: variable  may be uninitialized
      end var
   end function

See item 290 in the HISTORY.txt file.

The data-flow analysis of TRAIAN 3.4 rejected some correct LOTOS NT programs with a fatal error message:
```
   "return" inside a loop
```
that was irrelevant, as the targeted problem was actually not the presence of a "return" in a loop, but the fact that the loop was executed only once because of this "return" instruction. See item 293 in the HISTORY.txt file.

The data-flow analysis of TRAIAN 3.4 rejected some correct LOTOS NT programs with a fatal error message:
```
   function F may return without assigning parameter Y
```
if they raised an exception in some branch of an "if" or "case" instruction, e.g.,
```
   function F [E : none] (X : T, out Y : bool) is
      case X in
         NIL ->
	    raise E
      |  any ->
	    Y := X
      end case
   end function
```
See item 294 in the HISTORY.txt file.

The data-flow analysis of TRAIAN 3.4 rejected some correct LOTOS NT programs such as:

   function F (X: Bool) : Bool is
      loop L in
         return (X)
      end loop
   end function

with the following error message:

   function F may terminate without returning a value

See item 299 in the HISTORY.txt file.

The data-flow analysis of TRAIAN 3.4 rejected some correct programs such as:

   function F (X : nat) : nat is
      return X + 1;
      X := X + 1
   end function

with the following error message:

   function F may terminate without returning a value

See item 302 in the HISTORY.txt file.

The data-flow analysis of TRAIAN 3.4 triggered improper warnings of the form
```
   dead code following a "return" instruction
```
concerning "for" and "while" loops with false conditions. For instance, programs such as: for ... while FALSE by ... loop return TRUE end loop; return FALSE no longer trigger the following warning: since TRAIAN knows that the loop will never be executed. See item 303 in the HISTORY.txt file.

The verification of pattern exhaustiveness in TRAIAN 3.4 sometimes triggered spurious warnings:
```
   incomplete patterns in "case" instruction
```
Such warnings are no longer emitted, and their message was enhanced to be more precise and more informative. See item 305 in the HISTORY.txt file.

Future Work

TRAIAN 3.5 will continue to evolve, our goal being to merge LOTOS NT and LNT in one single language.

Download

TRAIAN 3.5 can be freely downloaded from the TRAIAN Web Page located at:

http://vasy.inria.fr/traian