The description of the W_shl_sat_l() operator in the STL Manual 18.6.2 ("Operators with complexity weight of 1") has various smaller mistakes:
\NewOperator{W\_shl\_sat\_l(W\_1, var1)}
Arithmetically shifts left the 64-bit W\_v1 by v1 positions with lower 32-bit saturation and returns the 32 LSB of 64-bit result.\\
If v1 is negative, the result is shifted to right by (-var1) positions and sign extended.
After shift operation, returns the 32 MSB of 64-bit result.
It should read correctly:
\NewOperator{W\_shl\_sat\_l(W\_var1, var2)}
Arithmetically shifts left the 64-bit W\_var1 by var2 positions with lower 32-bit saturation and returns the 32 LSB of 64-bit result.\\
If var2 is negative, the result is shifted to right by (-var2) positions and sign extended.
After shift operation, returns the 32 LSB of 64-bit result.