diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex index e532cf02b0f6ebd3b2e3aa950c40bfea5881f82e..4266ddd7e32525ee9990447e923a4d91831c2c42 100644 --- a/src/plugins/e-acsl/doc/refman/changes_modern.tex +++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex @@ -126,6 +126,12 @@ in \lstinline|\\at|} \subsection*{Version \eacslpluginversion} +\begin{itemize} +\item \changeinsection{expressions}{support of bitwise operations} +\end{itemize} + +\subsection*{Version Scandium-21} + \begin{itemize} \item \changeinsection{reals}{support of rational numbers and operations} \item \changeinsection{fn-behavior}{remove abrupt clauses from the list of diff --git a/src/plugins/e-acsl/doc/refman/intro_modern.tex b/src/plugins/e-acsl/doc/refman/intro_modern.tex index 8be890311bc013277597ff2790eae605cd7ba441..869c0d0e427e8504a1638ab7d97df20c439366a4 100644 --- a/src/plugins/e-acsl/doc/refman/intro_modern.tex +++ b/src/plugins/e-acsl/doc/refman/intro_modern.tex @@ -48,7 +48,6 @@ currently implemented into the \framac's \eacsl plug-in. \hline terms & \lstinline|\\true| and \lstinline|\\false| \\ - & bitwise operators \\ & let binding \\ & t-sets \\ \hline diff --git a/src/plugins/e-acsl/doc/refman/term.tex b/src/plugins/e-acsl/doc/refman/term.tex index 6af096790d609911bff64586e68fff1e7e26180b..0582703adc5a5512f462b839fd56885c2dc1a268 100644 --- a/src/plugins/e-acsl/doc/refman/term.tex +++ b/src/plugins/e-acsl/doc/refman/term.tex @@ -4,11 +4,11 @@ | real ; real constants | string ; string constants | character ; character constants - \ - bin-op ::= "+" | "-" | "*" | [ "/" ] | [ "%" ] | { "<<" } | { ">>" }; + \ + bin-op ::= "+" | "-" | "*" | [ "/" ] | [ "%" ] | "<<" | ">>"; | "==" | "!=" | "<=" | ">=" | ">" | "<" ; | [ "&&" ] | [ "||" ] | [ "^^" ] ; boolean operations - | { "&" } | { "|" } | { "-->" } | { "<-->" } | "^" ; bitwise operations + | "&" | "|" | "-->" | "<-->" | "^" ; bitwise operations \ unary-op ::= "+" | "-" ; unary plus and minus | "!" ; boolean negation