tlaplus/tlaplus

SANY allows @ in odd locations

Aperta

#1153 aperta il 25 feb 2025

 (1 commento) (0 reazioni) (0 assegnatari)Java (179 fork)batch import
SANYToolsbuggood first issue

Metriche repository

Star
 (2153 stelle)
Metriche merge PR
 (Nessuna PR mergiata in 30 g)

Descrizione

This should be enforced at the syntax level; SANY seems to treat @ (the function-except value symbol) as an ordinary valid identifier and allows it in odd locations. The following all parse correctly:

---- MODULE Test ----
CONSTANT @
====
---- MODULE Test ----
@ == 0
====

There are some haphazard checks for this, like this will trigger an "Attempted to declare '@' as a variable" error:

---- MODULE Test ----
VARIABLE @
====

Found during work on #1140.

Guida contributor