From cdc50c430fb03c2766b871d63d576c585515d80d Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 8 Apr 2021 11:42:02 +0200
Subject: [PATCH] [e-acsl:refman] update summary of not-yet-implemented
features
---
.../e-acsl/doc/refman/intro_modern.tex | 54 ++++++++++++++-----
1 file changed, 40 insertions(+), 14 deletions(-)
diff --git a/src/plugins/e-acsl/doc/refman/intro_modern.tex b/src/plugins/e-acsl/doc/refman/intro_modern.tex
index f103d3e0357..328721a32e7 100644
--- a/src/plugins/e-acsl/doc/refman/intro_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/intro_modern.tex
@@ -46,27 +46,53 @@ currently implemented into the \framac's \eacsl plug-in.
& mathematical reals \\
\hline
terms
- & \lstinline|\\true| and \lstinline|\\false| \\
+ & truth values \lstinline|\\true| and \lstinline|\\false| \\
+ & functional updates \\
+ & irrational numbers \\
+ & built-in function \lstinline|\\length| over arrays \\
+ & conversions of structure to structure \\
& t-sets \\
+ & higher-order logic constructs \\
+ & hybrid functions \\
+ & labeled memory-related built-in functions \\
+ & finite sets \\
+ & finite lists \\
+ & \lstinline|\\exit_status|
+ \\
\hline
predicates
- & exclusive or operator \\ % \lstinline|^^|
- & let bindings \\
- & quantifications over non-integer types \\
- & \lstinline|\\specified|
+ & let bindings of predicates \\
+ & unguarded quantifications over small types \\
+ & quantifications over pointers and enums \\
+ & iterators \\
+ & comparisons of unions and structures \\
+ & t-sets \\
+ & hybrid predicates \\
+ & labeled memory-related built-in predicates \\
+ & dangling pointers \lstinline|\\dangling|
\\
\hline
- annotations
- & behavior-specific annotations \\
- & loop assigns \\
- & global annotations
+ clauses
+ & decreases clauses \\
+ & assigns clauses \\
+ & allocation and deallocation clauses \\
+ & abrupt clauses \\
+ & reads clauses
\\
\hline
- behavior clauses
- & assigns \\
- & allocates \\
- & decreases \\
- & abrupt termination
+ annotations
+ & behavior-specific annotations (introduced by \lstinline|for|) \\
+ & loop assigns \\
+ & loop allocations \\
+ & lemmas \\
+ & inductive predicates \\
+ & axiomatic definitions \\
+ & polymorphic logic types \\
+ & concrete logic types \\
+ & specification modules \\
+ & data invariants \\
+ & model variables and model fields \\
+ & volatile variables
\\
\hline
\end{tabular}
--
GitLab