|
|
|
The CONVECS team is pleased to announce
that version 3.7 of the TRAIAN compiler for LOTOS NT is available.
TRAIAN 3.7 brings
four language changes,
four library changes,
ten static-semantics changes,
five code-generation changes,
and nineteen bug fixes
(see below their description).
TRAIAN 3.7 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 demo examples have been updated to reflect these changes.
traian_upc 2022-LOTNT-POINTER [<file> or <directory>]that will perform the following actions:
- variable X may be uninitialized - variable X never used - useless assignment to X - "in" parameter X modified (should be an "in var" parameter) - "in var" parameter X never modified (should be an "in" parameter) - "in var" parameter X overwritten before used (should be a local variable) - process with "out" parameter(s) but no normal termination - "out" parameter X both used and modified (should be an "out var" parameter) - process with "in out" parameter(s) but no normal termination - "out var" parameter X never used (should be an "out" parameter) - dead code after "raise" behaviour - loop label L never used - loop body is executed at most onceetc. See item 377 in the HISTORY.txt file.
event parameter PRINT never usedSee item 381 in the HISTORY.txt file.
- variable Y may be uninitialized
- write-write conflict for variable X:
X is assigned in the 1st and 2nd parallel branches
- read-write conflict for variable X:
X is modified in the 1st, 3rd, and 5th parallel branches
but used in the 2nd, 4th, and 6th parallel branches
etc.
See item 394 in the HISTORY.txt file.
process MAIN [PRINT: any] is
var X, Y : BOOL in
X := any Bool;
if X then
Y := not (X)
else
stop
end if;
PRINT (Y)
end var
end process
This program was rejected with an error message stating that variable
Y was possibly uninitialized in PRINT (Y). From now on,
such programs are accepted, as TRAIAN discards the "else" branch, since
no execution can take place after "stop".
See item 395 in the HISTORY.txt file.
process P [PRINT : any] (X : T) is
case X
var Y : nat in
C1 -> PRINT ("C1")
| C2 (any) -> PRINT ("C2")
end case
end process
triggers the following warning:
variable Y never usedSee item 397 in the HISTORY.txt file.
- dead code after infinite loop - dead code after "raise" and "stop" behaviours - dead code after "stop" behaviourSee item 399 in the HISTORY.txt file.
illegal behaviour in initialization of "for" loopSee item 400 in the HISTORY.txt file.
hidden event G never accessedSee item 401 in the HISTORY.txt file.
processes not yet fully implementedSee item 366 in the HISTORY.txt file.
/* generated by traian 3.7 */which prevents unintended deletion of user files that would be also named "*_f.h" or "*_t.h". See item 383 in the HISTORY.txt file.
channel C is
(x1: INT),
(x1, x2: INT)
end channel
...
hide G:C in
G (0)
end hide
TRAIAN emitted the following error message:
event G used with incorrect type
...
channel C cannot match the offer type:
(NAT|INT)
From now on, TRAIAN accepts the above code without errors, as the profiles of
channel C are used to resolve overloading of constant 0, the type of
which is either NAT or INT.
See item 367 in the HISTORY.txt file.
trap
exception E is
return Y
in
for X := N while X -[E] M > 1 by X := X -[UNEXPECTED] M
loop
Y := X;
use Y
end loop
end trap
where variable Y is used in the event handler for event E,
but could be uninitialized at this point, because E can be triggered
from the "while" condition of the "for" loop (possibly before
the first iteration), whereas Y is only initialized in the loop body.
From now on, the events raised in the "while" condition of a loop are
taken into account by the dataflow analysis.
See item 371 in the HISTORY.txt file.
trap
exception E is
return X
in
eval P (?X);
raise E
end trap
by reporting that X was not initialized in the event handler,
because all variables passed as "out" parameters to a function without
result (e.g., "?X" in the above example) were not taken into account
when determining the variables initialized before an event is raised.
See item 372 in the HISTORY.txt file.
trap
exception E is
return Y
in
eval Y := F [E] (!?X)
end trap
where variable Y could be used before being initialized in the handler
for event E. From now on, the events raised in procedure calls are
more finely analyzed.
See item 373 in the HISTORY.txt file.
function F (in var X: BOOL) : BOOL is
var Y: BOOL in
for null while X by X := Y loop
Y := false
end loop;
return X
end var
end function
where some variable Y was properly initialized in the body of a
"for" loop and used in the "by" clause of this loop.
See item 376 in the HISTORY.txt file.
function F (X : bool) : bool is
var Y : bool in
for null while X by null loop
Y := true
end loop;
return Y -- not initialized if X is false
end var
end function
From now on, TRAIAN no longer assumes that the body of a "for" loop is
executed at least once, which is not certain, and emits the following error
message:
variable Y may be uninitializedfor the above example. See item 378 in the HISTORY.txt file.
function F : BOOL is
trap
exception Y is
raise Y
in
...
end trap
end function
See item 379 in the HISTORY.txt file.
process P called with incorrect profile
in behaviour
P [E]
the call uses process profile:
P [none]
but the called process has profile:
P [any]
See item 380 in the HISTORY.txt file.
event parameter E never accessedeven if E was used in the "raise" part of a "require" or "ensure" clause of the function where E was declared. From now on, pre- and post-conditions are taken into account when analyzing event parameters. See item 382 in the HISTORY.txt file.
event parameter E never accessedeven if an "access E" instruction was present. See item 384 in the HISTORY.txt file.
function F (out X:NAT, Y:NAT) : BOOL is
loop
if Y > 0 then
loop
null
end loop
end if;
return false
end loop
end function
Formerly, only a warning was displayed:
function with "out" parameter(s) but no normal terminationFrom now on, a fatal error message is emitted:
function F may return without assigning parameter XSee item 385 in the HISTORY.txt file.
function F (out X : BOOL) is
return;
X := false
end function
From now on, occurrences in dead code of assignments to "out"
parameters are ignored, so that the above program triggers an error message
of the following form:
function F may return without assigning parameter XSee item 387 in the HISTORY.txt file.
function F (X : BOOL) : BOOL is
loop L in
return not (X);
break L -- (this is dead code)
end loop
end function
with the following error message:
function F may terminate without returning a valueFrom now on, such programs are accepted by TRAIAN, as dataflow analysis no longer considers occurrences of "break" instructions in dead code. See item 388 in the HISTORY.txt file.
function F (X : NAT) : NAT is
var X1, X2 : NAT in
trap
exception E is
return X1 + X2
in
X2 := 0;
if X < 3 then
X1 := 0;
raise E
else
return 0
end if
end trap
end var
end function
for which TRAIAN 3.6 emitted an error message:
variable X1 may be uninitializedin the event handler. From now on, dataflow analysis for "raise" is aligned on the analysis for "break" intructions. See item 396 in the HISTORY.txt file.
function F1 (X : Bool) : Bool is
var Y : Bool in
loop L in
if X then
break L
end if;
Y := not (X) -- no more warning here
end loop;
return Y
end var
end function
function F2 [E : none] (X : T, out Y : BOOL, Z : BOOL) is
loop L in
case X in
NIL ->
if Z then
raise E
else
Y := false; -- no more warning here
break L
end if
| any ->
Y := true -- no more warning here
end case
end loop
end function
See item 398 in the HISTORY.txt file.
integer overflow detected: op "+"The implementation of the succ() and card() functions for these types have been updated accordingly. See item 405 in the HISTORY.txt file.
#ifdef lint ... #endifdirectives that caused Gcc 10 warnings. See item 406 in the HISTORY.txt file.
TRAIAN 3.7 can be freely downloaded from the TRAIAN Web Page located at: