From 385e70f358c57968a90b9bf8dfde20f8c3fccc97 Mon Sep 17 00:00:00 2001 From: Fonenantsoa Maurica <maurica.fonenantsoa@gmail.com> Date: Fri, 30 Mar 2018 10:58:38 +0200 Subject: [PATCH] Refman and Changelog. --- src/plugins/e-acsl/doc/Changelog | 1 + src/plugins/e-acsl/doc/refman/predicate.tex | 2 +- src/plugins/e-acsl/doc/refman/term.tex | 2 +- 3 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog index c9cfb7651e5..56e12f92853 100644 --- a/src/plugins/e-acsl/doc/Changelog +++ b/src/plugins/e-acsl/doc/Changelog @@ -19,6 +19,7 @@ # configure configure ############################################################################### +- E-ACSL [2018/03/30] Support for let binding. - E-ACSL [2018/02/21] New option -e-acsl-replace-libc-functions to replace a few libc functions by built-ins that efficiently detects when they are incorrectly called. diff --git a/src/plugins/e-acsl/doc/refman/predicate.tex b/src/plugins/e-acsl/doc/refman/predicate.tex index a72f293e044..ae1dcfb6108 100644 --- a/src/plugins/e-acsl/doc/refman/predicate.tex +++ b/src/plugins/e-acsl/doc/refman/predicate.tex @@ -13,7 +13,7 @@ | [ { pred "^^" pred } ] ; exclusive or | [ term "?" pred ":" pred ] ; ternary condition | [ pred "?" pred ":" pred ]; - | { "\let" id "=" term ";" pred }; local binding + | "\let" id "=" term ";" pred ; local binding | { "\let" id "=" pred ";" pred }; | [ "\forall" binders ";" ] ; [ integer-guards "==>" pred ]; univ. integer quantification diff --git a/src/plugins/e-acsl/doc/refman/term.tex b/src/plugins/e-acsl/doc/refman/term.tex index 33576d7718f..6af096790d6 100644 --- a/src/plugins/e-acsl/doc/refman/term.tex +++ b/src/plugins/e-acsl/doc/refman/term.tex @@ -29,7 +29,7 @@ | { id "(" term ("," term)* ")" } ; function application | "(" term ")" ; parentheses | [ term "?" term ":" term ] ; ternary condition - | { "\let" id "=" term ";" term } ; local binding + | "\let" id "=" term ";" term ; local binding | "sizeof" "(" term ")" ; | "sizeof" "(" C-type-name ")" ; | id ":" term ; syntactic naming -- GitLab