diff --git a/ALL_VERSIONS b/ALL_VERSIONS
index 6f60aa58c52031931854e1eac39f5c8ed2b9f840..3b89335846656be9b460942dd746ce0cfb03a7a9 100644
--- a/ALL_VERSIONS
+++ b/ALL_VERSIONS
@@ -1,5 +1,6 @@
Version number Date of release Notes
============== =============== =====
+22.0 (Titanium) 2020, November 17
21.1 (Scandium) 2020, June 25 Bugs fixed
21.0 (Scandium) 2020, June 11
20.0 (Calcium) 2019, December 4
diff --git a/README.md b/README.md
index d426d5c40dbb996dda214ac9da696f8e60c06bad..afae47f12d44ad2c2cefc5b26cfe7f5034592ec3 100644
--- a/README.md
+++ b/README.md
@@ -96,7 +96,7 @@ via the GUI:
## Further reference
- Links to user and developer manuals, Frama-C archives,
- and plug-in manuals are available at <br> http://beta.frama-c.com/html/get-frama-c.html
+ and plug-in manuals are available at <br> http://frama-c.com/html/get-frama-c.html
- [StackOverflow](http://stackoverflow.com/questions/tagged/frama-c) has several
questions with the `frama-c` tag, which is monitored by several members of the
@@ -110,10 +110,10 @@ via the GUI:
the [issues tracking system](https://git.frama-c.com/pub/frama-c/issues),
for reporting bugs.
-- The [Frama-C documentation page](https://beta.frama-c.com/html/documentation.html)
+- The [Frama-C documentation page](https://frama-c.com/html/documentation.html)
contains links to all manuals and plugins description, as well as tutorials, courses
and more.
-- The [Frama-C blog](http://beta.frama-c.com/blog) has several posts about
+- The [Frama-C blog](http://frama-c.com/blog) has several posts about
new developments of Frama-C, as well as general discussions about the C
language, undefined behavior, floating-point computations, etc.
diff --git a/bin/build-src-distrib.sh b/bin/build-src-distrib.sh
index 272eb1caf79a83e93b09e0c8e75e8cf9559839bc..1bfb095e9c7ede6d469630aa0896568f7c4e48cd 100755
--- a/bin/build-src-distrib.sh
+++ b/bin/build-src-distrib.sh
@@ -5,14 +5,14 @@ set -u
# Executing this script requires bash 4.0 or higher
# (special use of the 'case' construct)
if test `echo $BASH_VERSION | sed "s/\([0-9]\).*/\1/" ` -lt 4; then
- echo "bash version >= 4 is required."
- exit 99
+ echo "bash version >= 4 is required."
+ exit 99
fi
# git-lfs needs to be installed
if ! command -v git-lfs >/dev/null 2>/dev/null; then
- echo "git-lfs is required"
- exit 99
+ echo "git-lfs is required"
+ exit 99
fi
# Set it to "no" in order to really execute the commands.
@@ -37,6 +37,8 @@ FRAMAC_VERSION_AND_CODENAME="${FRAMAC_VERSION}-${FRAMAC_VERSION_CODENAME}"
TARGZ_FILENAME=frama-c-${FRAMAC_VERSION_AND_CODENAME}.tar.gz
VERSION_MODIFIER=$(cat VERSION | sed -e s/[0-9.]*\\\(.*\\\)/\\1/)
+VERSION_MAJOR=$(cat VERSION | sed -e s/\\\([0-9]*\\\).[0-9]*.*/\\1/)
+VERSION_MINOR=$(cat VERSION | sed -e s/[0-9]*.\\\([0-9]*\\\).*/\\1/)
if test -n "$VERSION_MODIFIER"; then FINAL_RELEASE=no; else FINAL_RELEASE=yes; fi
@@ -47,35 +49,36 @@ if test "$FRAMAC_VERSION" != "$FRAMAC_TAG"; then
fi
run () {
- cmd=$1
- echo "$cmd"
- if test "$DEBUG" == "no"; then
- sh -c "$cmd" || { echo "Aborting step ${STEP}."; exit "${STEP}"; }
- fi
+ cmd=$1
+ echo "$cmd"
+ if test "$DEBUG" == "no"; then
+ sh -c "$cmd" || { echo "Aborting step ${STEP}."; exit "${STEP}"; }
+ fi
}
-GITLAB_DIR=./pub-frama-c
-GITLAB_GIT="git@git.frama-c.com:pub/frama-c.git"
+# GITLAB_DIR=./pub-frama-c
+# GITLAB_GIT="git@git.frama-c.com:pub/frama-c.git"
+
+# if test ! -d $GITLAB_DIR/.git; then
+# echo "WARNING: $GITLAB_DIR/.git directory not found; do you want to clone it? (y/n)"
+# read CHOICE
+# case "${CHOICE}" in
+# "Y"|"y")
+# run "git clone $GITLAB_GIT $GITLAB_DIR"
+# ;;
+# *)
+# echo "gitlab's public Frama-C project must be linked at $GITLAB_DIR \
+ # (clone or symbolic link)"
+# exit 1
+# ;&
+# esac
+# fi
+# GITLAB_BRANCH=$(git --git-dir=$GITLAB_DIR/.git rev-parse --abbrev-ref HEAD)
+# if test "$FRAMAC_BRANCH" != "$GITLAB_BRANCH"; then
+# echo "WARNING: switching pub-frama-c to current branch $FRAMAC_BRANCH"
+# run "git -C $GITLAB_DIR checkout -b $FRAMAC_BRANCH"
+# fi
-if test ! -d $GITLAB_DIR/.git; then
- echo "WARNING: $GITLAB_DIR/.git directory not found; do you want to clone it? (y/n)"
- read CHOICE
- case "${CHOICE}" in
- "Y"|"y")
- run "git clone $GITLAB_GIT $GITLAB_DIR"
- ;;
- *)
- echo "gitlab's public Frama-C project must be linked at $GITLAB_DIR \
- (clone or symbolic link)"
- exit 1
- ;&
- esac
-fi
-GITLAB_BRANCH=$(git --git-dir=$GITLAB_DIR/.git rev-parse --abbrev-ref HEAD)
-if test "$FRAMAC_BRANCH" != "$GITLAB_BRANCH"; then
- echo "WARNING: switching pub-frama-c to current branch $FRAMAC_BRANCH"
- run "git -C $GITLAB_DIR checkout -b $FRAMAC_BRANCH"
-fi
GITLAB_WIKI_GIT="git@git.frama-c.com:pub/frama-c.wiki"
GITLAB_WIKI=./frama-c.wiki
if test ! -d $GITLAB_WIKI/.git; then
@@ -121,14 +124,23 @@ fi
MANUALS_DIR="./doc/manuals"
# push on frama-c.com only for final releases
+WEBSITE_GIT="git@git.frama-c.com:pub/pub.frama-c.com.git"
if test "$FINAL_RELEASE" = "yes"; then
-WEBSITE_DIR="./website"
-if test \! -d $WEBSITE_DIR/.git ; then
- echo "ERROR: $WEBSITE_DIR/.git directory not found"
- echo "The Frama-C website repository must be linked at $WEBSITE_DIR (clone or symbolic link)"
- exit 1
-fi
-WEBSITE_BRANCH=`git --git-dir=$WEBSITE_DIR/.git rev-parse --abbrev-ref HEAD`
+ WEBSITE_DIR="./website"
+ if test \! -d $WEBSITE_DIR/.git ; then
+ echo "ERROR: $WEBSITE_DIR/.git directory not found; do you want to clone it? (y/n)"
+ read CHOICE
+ case "${CHOICE}" in
+ "Y"|"y")
+ run "git clone $WEBSITE_GIT website"
+ ;;
+ *)
+ echo "The Github Website repository must be linked at $WEBSITE_DIR (clone or symbolic link)"
+ exit 1
+ ;&
+ esac
+ fi
+ WEBSITE_BRANCH=`git --git-dir=$WEBSITE_DIR/.git rev-parse --abbrev-ref HEAD`
fi # FINAL_RELEASE == yes
BUILD_DIR_ROOT="/tmp/release"
@@ -137,24 +149,24 @@ BUILD_DIR="$BUILD_DIR_ROOT/frama-c"
echo "Frama-C Version : $FRAMAC_VERSION"
echo "Frama-C Branch : $FRAMAC_BRANCH"
echo "Final release : $FINAL_RELEASE"
-echo "pub/frama-c dir : $GITLAB_DIR"
-echo "pub/frama-c branch : $GITLAB_BRANCH"
+# echo "pub/frama-c dir : $GITLAB_DIR"
+# echo "pub/frama-c branch : $GITLAB_BRANCH"
echo "pub/frama-c wiki : $GITLAB_WIKI"
echo "Manuals Dir : $MANUALS_DIR"
if test "$FINAL_RELEASE" = "yes"; then
-echo "Website Dir : $WEBSITE_DIR"
-echo "Website Branch : $WEBSITE_BRANCH"
+ echo "Website Dir : $WEBSITE_DIR"
+ echo "Website Branch : $WEBSITE_BRANCH"
else
-echo "Intermediate release: website not updated"
+ echo "Intermediate release: website not updated"
fi
echo "Build Dir : $BUILD_DIR"
-DOWNLOAD_DIR="www/download"
+DOWNLOAD_DIR="download"
step () {
- STEP=$1
- echo
- echo "Step $1: $2"
+ STEP=$1
+ echo
+ echo "Step $1: $2"
}
export LC_CTYPE=en_US.UTF-8
@@ -174,157 +186,161 @@ Start at which step? (default is N, which cancels everything)
read STEP
case "${STEP}" in
- ""|"N")
- echo "Exiting without doing anything.";
- exit 0;
- ;&
- 0)
- step 0 "COMPILING PDF MANUALS"
- run "rm -rf $MANUALS_DIR"
- run "mkdir -p $MANUALS_DIR"
- run "doc/build-manuals.sh"
- ;&
- 1)
- run "git -C $GITLAB_DIR reset --hard"
- run "git -C $GITLAB_WIKI reset --hard"
- if test "$FINAL_RELEASE" = "yes"; then
- run "git -C $WEBSITE_DIR reset --hard"
- fi
- ;&
- 2)
- step 2 "BUILDING THE SOURCE DISTRIBUTION"
- # WARNING! MUST RUN git update-index BEFORE git diff-index!
- # See: https://stackoverflow.com/questions/36367190/git-diff-files-output-changes-after-git-status
- run "git update-index --refresh"
- if ! git diff-index HEAD --; then
- echo ""
- echo "### WARNING: uncommitted git changes will be discarded when creating archive!"
- echo "Proceed anyway? [y/N]"
- read CHOICE
- case "${CHOICE}" in
- "Y"|"y")
+ ""|"N")
+ echo "Exiting without doing anything.";
+ exit 0;
+ ;&
+ 0)
+ step 0 "COMPILING PDF MANUALS"
+ run "rm -rf $MANUALS_DIR"
+ run "mkdir -p $MANUALS_DIR"
+ run "doc/build-manuals.sh"
+ ;&
+ 1)
+ # run "git -C $GITLAB_DIR reset --hard"
+ run "git -C $GITLAB_WIKI reset --hard"
+ if test "$FINAL_RELEASE" = "yes"; then
+ run "git -C $WEBSITE_DIR reset --hard"
+ fi
+ ;&
+ 2)
+ step 2 "BUILDING THE SOURCE DISTRIBUTION"
+ # WARNING! MUST RUN git update-index BEFORE git diff-index!
+ # See: https://stackoverflow.com/questions/36367190/git-diff-files-output-changes-after-git-status
+ run "git update-index --refresh"
+ if ! git diff-index HEAD --; then
+ echo ""
+ echo "### WARNING: uncommitted git changes will be discarded when creating archive!"
+ echo "Proceed anyway? [y/N]"
+ read CHOICE
+ case "${CHOICE}" in
+ "Y"|"y")
;;
- *)
- echo "Stash or commit local changes, then run the script again."
- exit 1
- esac
- fi
- run "mkdir -p $BUILD_DIR_ROOT"
- run "rm -rf $BUILD_DIR"
- run "git worktree add -f --detach $BUILD_DIR $FRAMAC_BRANCH"
- run "cd $BUILD_DIR; autoconf"
- run "cd $BUILD_DIR; ./configure"
- run "cd $BUILD_DIR; make -j OPEN_SOURCE=yes src-distrib"
- # sanity check: markdown-report must be distributed
- run "tar tf $BUILD_DIR/$TARGZ_FILENAME | grep -q src/plugins/markdown-report"
- # populate release assets in wiki
- run "mkdir -p $GITLAB_WIKI/downloads"
- run "cp $BUILD_DIR/$TARGZ_FILENAME $GITLAB_WIKI/downloads/"
- if test "$FINAL_RELEASE" = "yes"; then
- SPEC_FILE="$DOWNLOAD_DIR/$TARGZ_FILENAME"
- run "rm -f $WEBSITE_DIR/$SPEC_FILE"
- run "cp $BUILD_DIR/$TARGZ_FILENAME $WEBSITE_DIR/$SPEC_FILE"
- run "git -C $WEBSITE_DIR add $SPEC_FILE"
- run "cp Changelog $WEBSITE_DIR/src/last-release/Changelog"
- run "cp src/plugins/wp/Changelog $WEBSITE_DIR/src/wpChangelog"
- run "cp src/plugins/wp/Changelog $WEBSITE_DIR/src/last-release/wpChangelog"
- run "cp src/plugins/e-acsl/doc/Changelog $WEBSITE_DIR/src/eacslChangelog"
- run "cp src/plugins/e-acsl/doc/Changelog $WEBSITE_DIR/src/last-release/eacslChangelog"
- fi
- ;&
- 3)
- #note: this step may fail if step 4 was performed,
- # because it will erase BUILD_DIR
- step 3 "BUILDING THE API BUNDLE"
- if test \! -d "$BUILD_DIR" ; then
- echo "ERROR: $BUILD_DIR does not exist, possibly removed by another step"
- exit 1
- fi
- run "cd $BUILD_DIR; make -j doc-distrib"
- if test "$FINAL_RELEASE" = "yes"; then
- SPEC_FILE="$DOWNLOAD_DIR/frama-c-${FRAMAC_VERSION_AND_CODENAME}-api.tar.gz"
- run "rm -f $WEBSITE_DIR/$SPEC_FILE"
- run "cp $BUILD_DIR/frama-c-api.tar.gz $WEBSITE_DIR/$SPEC_FILE"
- run "git -C $WEBSITE_DIR add $SPEC_FILE"
- fi
- ;&
- 4)
- step 4 "BUILDING THE DOCUMENTATION COMPANIONS"
- if test \! -d "$BUILD_DIR" ; then
- echo "ERROR: $BUILD_DIR does not exist, possibly removed by another step"
- exit 1
- fi
- run "cd $BUILD_DIR; make -j doc-companions"
- if test "$FINAL_RELEASE" = "yes"; then
- SPEC_FILE="$DOWNLOAD_DIR/hello-${FRAMAC_VERSION_AND_CODENAME}.tar.gz"
- RELE_FILE="$DOWNLOAD_DIR/hello.tar.gz"
- run "rm -f $WEBSITE_DIR/$SPEC_FILE $WEBSITE_DIR/$RELE_FILE"
- run "cp $BUILD_DIR/hello-${FRAMAC_VERSION_AND_CODENAME}.tar.gz $WEBSITE_DIR/$SPEC_FILE"
- run "git -C $WEBSITE_DIR add $SPEC_FILE"
- run "ln -s hello-${FRAMAC_VERSION_AND_CODENAME}.tar.gz $WEBSITE_DIR/$RELE_FILE";
- run "git -C $WEBSITE_DIR add $RELE_FILE"
+ *)
+ echo "Stash or commit local changes, then run the script again."
+ exit 1
+ esac
+ fi
+ run "mkdir -p $BUILD_DIR_ROOT"
run "rm -rf $BUILD_DIR"
- run "git worktree prune"
- fi
- ;&
- 5)
- step 5 "COPYING AND STAGING THE DISTRIBUTED MANUALS"
- PAGE_NAME=Frama-C-${FRAMAC_VERSION_AND_CODENAME}.md
- WIKI_PAGE=$GITLAB_WIKI/$PAGE_NAME
- run "mkdir -p $GITLAB_WIKI/manuals"
- run "sed -i -e '/<!-- LAST RELEASE -->/a \
+ run "git worktree add -f --detach $BUILD_DIR $FRAMAC_BRANCH"
+ run "cd $BUILD_DIR; autoconf"
+ run "cd $BUILD_DIR; ./configure"
+ run "cd $BUILD_DIR; make -j OPEN_SOURCE=yes src-distrib"
+ # sanity check: markdown-report must be distributed
+ run "tar tf $BUILD_DIR/$TARGZ_FILENAME | grep -q src/plugins/markdown-report"
+ # populate release assets in wiki
+ run "mkdir -p $GITLAB_WIKI/downloads"
+ run "cp $BUILD_DIR/$TARGZ_FILENAME $GITLAB_WIKI/downloads/"
+ if test "$FINAL_RELEASE" = "yes"; then
+ SPEC_FILE="$DOWNLOAD_DIR/$TARGZ_FILENAME"
+ run "rm -f $WEBSITE_DIR/$SPEC_FILE"
+ run "cp $BUILD_DIR/$TARGZ_FILENAME $WEBSITE_DIR/$SPEC_FILE"
+ run "git -C $WEBSITE_DIR add $SPEC_FILE"
+ fi
+ ;&
+ 3)
+ #note: this step may fail if step 4 was performed,
+ # because it will erase BUILD_DIR
+ step 3 "BUILDING THE API BUNDLE"
+ if test \! -d "$BUILD_DIR" ; then
+ echo "ERROR: $BUILD_DIR does not exist, possibly removed by another step"
+ exit 1
+ fi
+ run "cd $BUILD_DIR; make -j doc-distrib"
+ if test "$FINAL_RELEASE" = "yes"; then
+ SPEC_FILE="$DOWNLOAD_DIR/frama-c-${FRAMAC_VERSION_AND_CODENAME}-api.tar.gz"
+ run "rm -f $WEBSITE_DIR/$SPEC_FILE"
+ run "cp $BUILD_DIR/frama-c-api.tar.gz $WEBSITE_DIR/$SPEC_FILE"
+ run "git -C $WEBSITE_DIR add $SPEC_FILE"
+ fi
+ ;&
+ 4)
+ step 4 "BUILDING THE DOCUMENTATION COMPANIONS"
+ if test \! -d "$BUILD_DIR" ; then
+ echo "ERROR: $BUILD_DIR does not exist, possibly removed by another step"
+ exit 1
+ fi
+ run "cd $BUILD_DIR; make -j doc-companions"
+ if test "$FINAL_RELEASE" = "yes"; then
+ SPEC_FILE="$DOWNLOAD_DIR/hello-${FRAMAC_VERSION_AND_CODENAME}.tar.gz"
+ RELE_FILE="$DOWNLOAD_DIR/hello.tar.gz"
+ run "rm -f $WEBSITE_DIR/$SPEC_FILE $WEBSITE_DIR/$RELE_FILE"
+ run "cp $BUILD_DIR/hello-${FRAMAC_VERSION_AND_CODENAME}.tar.gz $WEBSITE_DIR/$SPEC_FILE"
+ run "git -C $WEBSITE_DIR add $SPEC_FILE"
+ run "ln -s hello-${FRAMAC_VERSION_AND_CODENAME}.tar.gz $WEBSITE_DIR/$RELE_FILE";
+ run "git -C $WEBSITE_DIR add $RELE_FILE"
+ run "rm -rf $BUILD_DIR"
+ run "git worktree prune"
+ fi
+ ;&
+ 5)
+ step 5 "COPYING AND STAGING THE DISTRIBUTED MANUALS"
+ PAGE_NAME=Frama-C-${FRAMAC_VERSION_AND_CODENAME}.md
+ WIKI_PAGE=$GITLAB_WIKI/$PAGE_NAME
+ run "mkdir -p $GITLAB_WIKI/manuals"
+ run "sed -i -e '/<!-- LAST RELEASE -->/a \
- [${FRAMAC_VERSION} (${FRAMAC_VERSION_CODENAME})](Frama-C-${FRAMAC_VERSION_AND_CODENAME})' $GITLAB_WIKI/Home.md"
- if test "$FINAL_RELEASE" = "yes"; then
- release_type="FINAL"
- else
- release_type="BETA"
- fi
- run "sed -i -e '/<!-- LAST ${release_type} RELEASE -->/a \
+ if test "$FINAL_RELEASE" = "yes"; then
+ release_type="FINAL"
+ else
+ release_type="BETA"
+ fi
+ run "sed -i -e '/<!-- LAST ${release_type} RELEASE -->/a \
- [${FRAMAC_VERSION} (${FRAMAC_VERSION_CODENAME})](Frama-C-${FRAMAC_VERSION_AND_CODENAME})' $GITLAB_WIKI/_sidebar.md"
- echo "# Frama-C release ${FRAMAC_VERSION} (${FRAMAC_VERSION_CODENAME})" > $WIKI_PAGE
- echo "## Sources" >> $WIKI_PAGE
- echo " - [$TARGZ_FILENAME](downloads/$TARGZ_FILENAME)" >> $WIKI_PAGE
- echo "" >> $WIKI_PAGE
- echo "## Manuals" >> $WIKI_PAGE
- for fpath in $MANUALS_DIR/*; do
- f=$(basename $fpath)
- f_no_ext=${f%.*}
- # E-ACSL-related files are stored in subdirectory e-acsl
- if [[ $f_no_ext =~ ^e-acsl.*$ ]]; then
- destdir="$WEBSITE_DIR/$DOWNLOAD_DIR/e-acsl"
- else
- destdir="$WEBSITE_DIR/$DOWNLOAD_DIR"
- fi
- if [[ -L $fpath ]]; then
- # symbolic links are copied to the website and prepended with 'frama-c-'
- # (except for acsl.pdf, which is copied as is)
- if [[ $f_no_ext =~ ^(e-)?acsl$ ]]; then
- ln="$f"
- else
- ln="frama-c-$f"
- fi
- run "rm -f $destdir/$ln"
- run "cp -P $fpath $destdir/$ln"
- run "git -C $destdir add $ln"
- else
- # non-symbolic links are copied as-is to the website, and also to
- # the Gitlab wiki, where they are also added as links
- f_no_pdf_ext="${f%.pdf}"
- echo "- [${f_no_pdf_ext%-${FRAMAC_VERSION_AND_CODENAME}}](manuals/$f)" >> $WIKI_PAGE
- run "cp $fpath $GITLAB_WIKI/manuals/"
- run "git -C $GITLAB_WIKI add manuals/$f"
- run "cp $fpath $destdir/$f"
- run "git -C $destdir add $f"
- fi
- done
+ echo "# Frama-C release ${FRAMAC_VERSION} (${FRAMAC_VERSION_CODENAME})" > $WIKI_PAGE
+ echo "## Sources" >> $WIKI_PAGE
+ echo " - [$TARGZ_FILENAME](downloads/$TARGZ_FILENAME)" >> $WIKI_PAGE
+ echo "" >> $WIKI_PAGE
+ echo "## Manuals" >> $WIKI_PAGE
+ for fpath in $MANUALS_DIR/*; do
+ f=$(basename $fpath)
+ f_no_ext=${f%.*}
+ # E-ACSL-related files are stored in subdirectory e-acsl
+ if [[ $f_no_ext =~ ^e-acsl.*$ ]]; then
+ destdir="$WEBSITE_DIR/$DOWNLOAD_DIR/e-acsl"
+ else
+ destdir="$WEBSITE_DIR/$DOWNLOAD_DIR"
+ fi
+ if [[ -L $fpath ]]; then
+ # symbolic links are copied to the website and prepended with 'frama-c-'
+ # (except for acsl.pdf, which is copied as is)
+ if [[ $f_no_ext =~ ^(e-)?acsl$ ]]; then
+ ln="$f"
+ else
+ ln="frama-c-$f"
+ fi
+ run "rm -f $destdir/$ln"
+ run "cp -P $fpath $destdir/$ln"
+ run "git -C $destdir add $ln"
+ else
+ # non-symbolic links are copied as-is to the website, and also to
+ # the Gitlab wiki, where they are also added as links
+ f_no_pdf_ext="${f%.pdf}"
+ echo "- [${f_no_pdf_ext%-${FRAMAC_VERSION_AND_CODENAME}}](manuals/$f)" >> $WIKI_PAGE
+ run "cp $fpath $GITLAB_WIKI/manuals/"
+ run "git -C $GITLAB_WIKI add manuals/$f"
+ run "cp $fpath $destdir/$f"
+ run "git -C $destdir add $f"
+ fi
+ done
+
+ INSTALL_WEBPAGE=html/installations/$(echo "$FRAMAC_VERSION_CODENAME" | tr '[:upper:]' '[:lower:]').md
+ INSTALL_WEBPAGE_PATH=$WEBSITE_DIR/$INSTALL_WEBPAGE
+ echo "----" > $INSTALL_WEBPAGE_PATH
+ echo "layout: doc_page" >> $INSTALL_WEBPAGE_PATH
+ echo "title: Installation instructions for $FRAMAC_VERSION_CODENAME" >> $INSTALL_WEBPAGE_PATH
+ echo "----" >> $INSTALL_WEBPAGE_PATH
+ cat ./INSTALL.md >> $INSTALL_WEBPAGE_PATH
+ run "git -C $WEBSITE_DIR add $INSTALL_WEBPAGE"
- run "git -C $GITLAB_WIKI add $PAGE_NAME"
- ;;
- *)
- echo "Bad entry: ${STEP}"
- echo "Exiting without doing anything.";
- exit 31
- ;;
+ run "git -C $GITLAB_WIKI add $PAGE_NAME"
+ ;;
+ *)
+ echo "Bad entry: ${STEP}"
+ echo "Exiting without doing anything.";
+ exit 31
+ ;;
esac
exit 0
diff --git a/devel_tools/docker/frama-c.custom/Dockerfile b/devel_tools/docker/frama-c.custom/Dockerfile
index c742082bbd45bb69371125d868de56357da68e84..0d93e4f5b41b8b06faa056db6d05c0cc5351d613 100644
--- a/devel_tools/docker/frama-c.custom/Dockerfile
+++ b/devel_tools/docker/frama-c.custom/Dockerfile
@@ -19,21 +19,25 @@ ENV PATH "/root/.opam/ocaml-base-compiler.4.08.1/bin:$PATH"
RUN opam update -y && opam install depext -y
# Install packages from reference configuration
+# Note: Python and time packages are only required for tests, but if so,
+# they need to be present before running './configure'
RUN apt-get update && opam update -y && opam depext --install -y --verbose \
- alt-ergo.2.0.0 \
+ alt-ergo.2.2.0 \
apron.v0.9.12 \
conf-graphviz.0.1 \
mlgmpidl.1.2.12 \
ocamlfind.1.8.1 \
ocamlgraph.1.8.8 \
ppx_deriving_yojson.3.5.2 \
- why3.1.3.1 \
+ why3.1.3.3 \
yojson.1.7.0 \
zarith.1.9.1 \
zmq.5.1.3 \
+ conf-python-3.1.0.0 \
+ conf-time.1 \
&& rm -rf /var/lib/apt/lists/*
-RUN why3 config --full-config
+RUN why3 config --detect
# with_source: keep Frama-C sources
ARG with_source=no
@@ -52,14 +56,11 @@ RUN cd /root && \
# with_test: run Frama-C tests; requires "with_source=yes"
ARG with_test=no
+# run general tests, then test that WP can see external provers
RUN if [ "${with_test}" != "no" ]; then \
- apt-get update && \
- opam update -y && opam depext --install -y \
- conf-python-3.1.0.0 \
- conf-time.1 \
- --verbose \
- && \
- rm -rf /var/lib/apt/lists/* && \
cd /root/frama-c && \
- make tests; \
+ make tests && \
+ (cd src/plugins/wp/tests/ && \
+ frama-c -wp wp_gallery/binary-multiplication-without-overflow.c \
+ -wp-prover alt-ergo,cvc4); \
fi
diff --git a/devel_tools/docker/frama-c.dev/Dockerfile b/devel_tools/docker/frama-c.dev/Dockerfile
index 67acc324b1438531ddb3f5e66a162f9004d8e6bf..ff51e8094c952ebdf3254a7b0ece8d5b37843218 100644
--- a/devel_tools/docker/frama-c.dev/Dockerfile
+++ b/devel_tools/docker/frama-c.dev/Dockerfile
@@ -19,6 +19,8 @@ ENV PATH "/root/.opam/ocaml-base-compiler.4.08.1/bin:$PATH"
RUN opam update -y && opam install depext -y
# Install packages from reference configuration
+# Note: Python and time packages are only required for tests, but if so,
+# they need to be present before running './configure'
RUN apt-get update && opam update -y && opam depext --install -y --verbose \
alt-ergo.2.2.0 \
apron.v0.9.12 \
@@ -31,6 +33,8 @@ RUN apt-get update && opam update -y && opam depext --install -y --verbose \
yojson.1.7.0 \
zarith.1.9.1 \
zmq.5.1.3 \
+ conf-python-3.1.0.0 \
+ conf-time.1 \
&& rm -rf /var/lib/apt/lists/*
RUN why3 config --detect
@@ -52,13 +56,6 @@ ARG with_test=no
# run general tests, then test that WP can see external provers
RUN if [ "${with_test}" != "no" ]; then \
- apt-get update && \
- opam update -y && opam depext --install -y \
- conf-python-3.1.0.0 \
- conf-time.1 \
- --verbose \
- && \
- rm -rf /var/lib/apt/lists/* && \
cd /root/frama-c && \
make tests && \
(cd src/plugins/wp/tests/ && \
diff --git a/doc/MakeLaTeXModern b/doc/MakeLaTeXModern
index d1b204a14b1ea83265f8686f43d31cfa3f116629..812842bc0f9a3ba2a7b32639fa05135c3bbb6148 100644
--- a/doc/MakeLaTeXModern
+++ b/doc/MakeLaTeXModern
@@ -1,24 +1,25 @@
+FRAMAC_DOC_ROOT_DIR?=..
FRAMAC_MODERN=frama-c-book.cls frama-c-cover.pdf frama-c-left.pdf frama-c-right.pdf
-frama-c-book.cls: ../frama-c-book.cls
+frama-c-book.cls: $(FRAMAC_DOC_ROOT_DIR)/frama-c-book.cls
@rm -f $@
@cp $< .
@chmod a-w $@
@echo "import $<"
-frama-c-cover.pdf: ../frama-c-cover.pdf
+frama-c-cover.pdf: $(FRAMAC_DOC_ROOT_DIR)/frama-c-cover.pdf
@rm -f $@
@cp $< .
@chmod a-w $@
@echo "import $<"
-frama-c-right.pdf: ../frama-c-right.pdf
+frama-c-right.pdf: $(FRAMAC_DOC_ROOT_DIR)/frama-c-right.pdf
@rm -f $@
@cp $< .
@chmod a-w $@
@echo "import $<"
-frama-c-left.pdf: ../frama-c-left.pdf
+frama-c-left.pdf: $(FRAMAC_DOC_ROOT_DIR)/frama-c-left.pdf
@rm -f $@
@cp $< .
@chmod a-w $@
diff --git a/doc/developer/changes.tex b/doc/developer/changes.tex
index 2230467a8ad62f1b5512330c647279b02c6a2b70..66ae55f2ea703e44e2d8a4e80ab62421c1b997ce 100644
--- a/doc/developer/changes.tex
+++ b/doc/developer/changes.tex
@@ -5,7 +5,7 @@
This chapter summarizes the major changes in this documentation between each
\framac release, from newest to oldest.
-\section*{Frama-C+dev}
+\section*{22.0 Titanium}
\begin{itemize}
\item \textbf{Testing}: Document new directives \texttt{TIMEOUT} and
\texttt{NOFRAMAC}
diff --git a/doc/userman/user-changes.tex b/doc/userman/user-changes.tex
index c2d128136851bdda4d32c1a012e7dd380691b341..103d9a2f2a8b8812e77a7f8f10ef5b2a7b478f1a 100644
--- a/doc/userman/user-changes.tex
+++ b/doc/userman/user-changes.tex
@@ -3,7 +3,7 @@
This chapter summarizes the changes in this documentation between each \FramaC
release. First we list changes of the last release.
-\section*{\nextframacversion}
+\section*{22.0 (Titanium)}
\begin{itemize}
\item \textbf{Getting Started:} added option
diff --git a/opam/opam b/opam/opam
index 05d570cb7a691803300c65d9ae32cd41864cbce3..8ea41587bfaced97d3eae73b1ceb21435640cce9 100644
--- a/opam/opam
+++ b/opam/opam
@@ -65,7 +65,7 @@ authors: [
homepage: "http://frama-c.com/"
license: "GNU Lesser General Public License version 2.1"
dev-repo: "git+https://git.frama-c.com/pub/frama-c.git"
-doc: "http://frama-c.com/download/user-manual-21.1-Scandium.pdf"
+doc: "http://frama-c.com/download/user-manual-22.0-Titanium.pdf"
bug-reports: "https://git.frama-c.com/pub/frama-c/issues"
tags: [
"deductive"
@@ -132,6 +132,10 @@ depopts: [
messages: [
"The Frama-C/Wp now uses Why-3 for all provers (Cf. deprecated -wp-prover native:alt-ergo)"
{alt-ergo:installed}
- "The Frama-C/Wp native support for Coq is now deprecated (use TIP or Why-3 instead)."
+ "The Frama-C/Wp native support for Coq is deprecated and only activated with Coq.8.12.x (use TIP or Why-3 instead)."
{coq:installed}
]
+
+post-messages: [
+ "Why3 provers setup: rm -r ~/.why3.conf ; why3 config --detect"
+]
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 121ad96facc0f37bf6de65c4c7f03e57953649fb..8a41fe69f4f24827622a3d4d6c56ed638821d3eb 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -109,15 +109,23 @@
let loc_ext d = { extended_node = d; extended_loc = loc () }
- let concat_froms a1 a2 =
- let compare_pair (b1,_) (b2,_) = is_same_lexpr b1 b2 in
+ let filter_from l = function
+ | FromAny ->
+ l, FromAny
+ | From ds ->
+ let f ds d = if List.exists (is_same_lexpr d) ds then ds else d :: ds in
+ l, From(List.(rev (fold_left f [] ds)))
+
+ let concat_froms cura newa =
+ let compare_pair (curb,_) (newb,_) = is_same_lexpr curb newb in
(* NB: the following has an horrible complexity, but the order of
clauses in the input is preserved. *)
- let concat_one acc (_,f2 as p) =
+ let concat_one acc (newloc, newf) =
+ let (newloc, newf) as p = filter_from newloc newf in
try
- let (_,f1) = List.find (compare_pair p) acc
+ let (curloc,curf) = List.find (compare_pair p) acc
in
- match (f1, f2) with
+ match (curf, newf) with
| _,FromAny ->
(* the new fundeps does not give more information than the one
which is already present. Just ignore it.
@@ -130,12 +138,28 @@
that we get the exact same clause if we try to
link the original contract with its pretty-printed version. *)
Extlib.replace compare_pair p acc
- | From _, From _ ->
- (* we keep the two functional dependencies,
- as they have to be proved separately. *)
- acc @ [p]
+ | From curl, From newl ->
+ let incl l lin =
+ List.(for_all (fun e -> exists (is_same_lexpr e) lin) l)
+ in
+ let drop d k =
+ Kernel.warning ~current:false ~wkey:Kernel.wkey_multi_from
+ "Drop '%a' \\from at %a for more precise one at %a"
+ Logic_print.print_lexpr curloc
+ Cil_datatype.Location.pretty d.lexpr_loc
+ Cil_datatype.Location.pretty k.lexpr_loc
+ in
+ if incl curl newl then begin
+ if not (incl newl curl) then drop newloc curloc;
+ acc
+ end
+ else if incl newl curl then begin
+ drop curloc newloc;
+ Extlib.replace compare_pair p acc
+ end
+ else acc @ [p]
with Not_found -> acc @ [p]
- in List.fold_left concat_one a1 a2
+ in List.fold_left concat_one cura newa
let concat_allocation fa1 fa2 =
match fa1,fa2 with
@@ -151,7 +175,7 @@
| Writes [], _ | Writes _, [] ->
raise (
Not_well_formed (loc(),"Mixing \\nothing and a real location"))
- | Writes a1, a2 -> Writes (concat_froms a2 a1)
+ | Writes a1, a2 -> Writes (concat_froms (concat_froms [] a2) a1)
let concat_loop_assigns_allocation annots bhvs2 a2 fa2=
(* NB: this is supposed to merge assigns related to named behaviors, in
diff --git a/src/kernel_internals/parsing/logic_preprocess.mll b/src/kernel_internals/parsing/logic_preprocess.mll
index 34ea01b4d6bda1c8a16eb82d54425fc1b82b90ef..765d158daf4a966e8c609f7a6f0e56426b143a7e 100644
--- a/src/kernel_internals/parsing/logic_preprocess.mll
+++ b/src/kernel_internals/parsing/logic_preprocess.mll
@@ -62,9 +62,30 @@
let backslash = "__ANNOT_BACKSLASH__"
let annot_content = "__ANNOT_CONTENT__"
+ let utf8_prefix = "__FC_UTF8_"
+
+ let encode_utf8 c = utf8_prefix ^ (string_of_int (Char.code c))
let re_backslash = Str.regexp_string backslash
let re_annot_content = Str.regexp_string annot_content
+ let re_utf8 = Str.regexp (utf8_prefix ^ "\\([0-9]+\\)")
+
+ let decode_utf8 s =
+ let res = ref s in
+ let start = ref 0 in
+ try
+ while true do
+ let b = Str.search_forward re_utf8 !res !start in
+ let e = Str.match_end () in
+ let chr = Char.chr (int_of_string (Str.matched_group 1 !res)) in
+ let buf = Bytes.of_string !res in
+ Bytes.set buf b chr;
+ Bytes.blit buf e buf (b+1) (String.length !res - e);
+ res:= Bytes.sub_string buf 0 (String.length !res + 1 + b - e);
+ start := b+1;
+ done;
+ assert false;
+ with Not_found -> !res
(* Delimiters for the various annotations in the preprocessing buffer.
We have one delimiter for the beginning of an annotation (to discard
@@ -115,7 +136,7 @@
ignore_content ();
ignore (input_line file); (* ignore the #line directive *)
let with_nl, content = get_annot true in
- with_nl, replace_backslash content
+ with_nl, decode_utf8 @@ replace_backslash content
with End_of_file ->
Kernel.fatal
"too few annotations in result file while pre-processing annotations"
@@ -184,6 +205,8 @@
add_preprocess_line_info()
}
+let utf8 = ['\128'-'\255']
+
rule main = parse
| ("#define"|"#undef") [' ''\t']* ((['a'-'z''A'-'Z''0'-'9''_'])* as m)
{
@@ -388,6 +411,10 @@ and annot = parse
is_newline:=CHAR;
Buffer.add_char preprocess_buffer '"';
string annot lexbuf }
+ | utf8 as c {
+ Buffer.add_string preprocess_buffer (encode_utf8 c);
+ annot lexbuf
+ }
| _ as c { is_newline := CHAR;
Buffer.add_char preprocess_buffer c;
annot lexbuf }
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 30a1603c6ada298959263b39055535650a6e826c..869bad2794f51fab9519f3f07afd68e57c040442 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -2913,12 +2913,17 @@ class cil_printer () = object (self)
(function (a,_) -> not (Logic_const.is_exit_status a.it_content))
l
in
+ let unique_assigned_locs =
+ let same t1 t2 = Cil_datatype.Term.equal t1.it_content t2.it_content in
+ let f l (a,_) = if List.exists (same a) l then l else a :: l in
+ List.rev (List.fold_left f [] without_result)
+ in
fprintf fmt "@[<h>%t%a@]"
(fun fmt -> if without_result <> [] then
Format.fprintf fmt "%a " self#pp_acsl_keyword kw)
(Pretty_utils.pp_list ~sep:",@ " ~suf:";@]"
- (fun fmt (t, _) -> self#identified_term fmt t))
- without_result
+ (fun fmt t -> self#identified_term fmt t))
+ unique_assigned_locs
method private assigns_deps kw fmt = function
| WritesAny -> ()
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 0ddeab5c75a42c32227c2d5099582104a5a112c4..27e2b1cd3fe12941cac241bd352aad73593f1e89 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -185,6 +185,8 @@ let wkey_no_proto = register_warn_category "typing:no-proto"
let wkey_missing_spec = register_warn_category "annot:missing-spec"
+let wkey_multi_from = register_warn_category "annot:multi-from"
+
let wkey_decimal_float = register_warn_category "parser:decimal-float"
let () = set_warn_status wkey_decimal_float Log.Wonce
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index f62ba3b05e3b0e7eaae81d3e521ffc219007cccf..c6ffe271274d0566b44115791d6a158d672cc056 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -175,6 +175,8 @@ val wkey_no_proto: warn_category
val wkey_missing_spec: warn_category
+val wkey_multi_from: warn_category
+
val wkey_decimal_float: warn_category
val wkey_acsl_extension: warn_category
diff --git a/src/plugins/aorai/tests/Aorai_test.ml b/src/plugins/aorai/tests/Aorai_test.ml
index 7807773dd168dcd111c2c11a09ae6fa1efe817cc..14137309241b0dfdc41801cda0309fc5cb605e1a 100644
--- a/src/plugins/aorai/tests/Aorai_test.ml
+++ b/src/plugins/aorai/tests/Aorai_test.ml
@@ -71,11 +71,17 @@ let extend () =
wp_compute_kf kf
in
run f;
+ let tmpdir = Filename.get_temp_dir_name () in
+ let tmpdir =
+ match Filename.chop_suffix_opt ~suffix:"/" tmpdir with
+ | None -> tmpdir
+ | Some dir -> dir
+ in
let tmpfile =
- Filename.get_temp_dir_name () ^ "/aorai_" ^
- (Filename.chop_extension
- (Filename.basename (List.hd (Kernel.Files.get()):>string))) ^ "_" ^
- (string_of_int (TestNumber.get ())) ^ ".i"
+ tmpdir ^ "/aorai_" ^
+ Filename.(
+ chop_extension (basename (List.hd (Kernel.Files.get()):>string))) ^
+ "_" ^ (string_of_int (TestNumber.get ())) ^ ".i"
in
let () =
Extlib.safe_at_exit
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index ea5ce613a207ef1e95b15c12bf6a9f9a657770de..6f9504e7b02330d52e9a8c8e9612425fc537f3a4 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -359,8 +359,6 @@ EACSL_MANPAGES := \
EACSL_CONTRIB_FILES = \
$(EACSL_DLMALLOC_REL_DIR)/dlmalloc.c
-EACSL_MANUAL_FILES = doc/manuals/*.pdf
-
EACSL_DOC_FILES = \
doc/doxygen/doxygen.cfg.in \
doc/Changelog \
@@ -483,8 +481,6 @@ include $(FRAMAC_SHARE)/Makefile.dynamic
# Install #
###########
-EACSL_INSTALL_MANUAL_FILES=$(wildcard $(addprefix $(EACSL_PLUGIN_DIR)/, $(EACSL_MANUAL_FILES)))
-
EACSL_INSTALL_SCRIPTS=$(addprefix $(E_ACSL_DIR)/,$(EACSL_SCRIPTS))
EACSL_INSTALL_MANPAGES=$(addprefix $(E_ACSL_DIR)/,$(EACSL_MANPAGES))
@@ -499,13 +495,6 @@ install:: clean-install
$(MKDIR) $(FRAMAC_DATADIR)/$$dir && \
$(CP) $(E_ACSL_DIR)/share/$$dir/*.[ch] $(FRAMAC_DATADIR)/$$dir ; \
done
- # manuals are not present in standard distribution.
- # Don't fail because of that.
-ifneq ("$(EACSL_INSTALL_MANUAL_FILES)","")
- $(PRINT_INSTALL) E-ACSL manuals
- $(MKDIR) $(FRAMAC_DATADIR)/manuals
- $(CP) $(EACSL_INSTALL_MANUAL_FILES) $(FRAMAC_DATADIR)/manuals;
-endif
$(PRINT_INSTALL) E-ACSL libraries
$(MKDIR) $(EACSL_INSTALL_LIB_DIR)
$(CP) $(EACSL_LIBDIR)/libeacsl-*.a $(EACSL_INSTALL_LIB_DIR)
@@ -526,8 +515,6 @@ EACSL_INSTALLED_MANPAGES=$(addprefix $(MANDIR)/man1/,$(notdir $(EACSL_MANPAGES))
uninstall::
$(PRINT_RM) E-ACSL share files
$(RM) -r $(FRAMAC_DATADIR)/e-acsl
- $(PRINT_RM) E-ACSL manuals
- $(RM) $(FRAMAC_DATADIR)/manuals/*.pdf
$(PRINT_RM) E-ACSL libraries
$(RM) -r $(EACSL_INSTALL_LIB_DIR)
$(PRINT_RM) E-ACSL scripts
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index bd67f1b6a3afa5b8f5f77727a51daebe5e304e4d..5a7d4b618dba3400398d2be044936114698e65bd 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -32,6 +32,8 @@ Plugin E-ACSL <next-release>
Plugin E-ACSL 22.0 (Titanium)
#############################
+-* E-ACSL [2020-11-16] Fix soundness bug when checking
+ initialization of a chunk of heap memory block.
- E-ACSL [2020-10-14] Add Support for Variadic generated functions in
the AST (frama-c/e-acsl#128).
- E-ACSL [2020-10-06] Add support for the `\separated` predicate.
diff --git a/src/plugins/e-acsl/doc/refman/.gitignore b/src/plugins/e-acsl/doc/refman/.gitignore
index 2c2b06ea7119f0233f24735f396c4f9bf3f4bd1c..af1f84a1f2fe63f47eb92d0d937027e16a6870b6 100644
--- a/src/plugins/e-acsl/doc/refman/.gitignore
+++ b/src/plugins/e-acsl/doc/refman/.gitignore
@@ -1,3 +1,7 @@
+frama-c-book.cls
+frama-c-cover.pdf
+frama-c-left.pdf
+frama-c-right.pdf
e-acsl.pdf
e-acsl-implementation.pdf
eacslversion.tex
diff --git a/src/plugins/e-acsl/doc/refman/Makefile b/src/plugins/e-acsl/doc/refman/Makefile
index 43227e2983888961de1886a8fff14b27601199ce..c71c70b01f0fbbc9d34312330f1a015a144a3c29 100644
--- a/src/plugins/e-acsl/doc/refman/Makefile
+++ b/src/plugins/e-acsl/doc/refman/Makefile
@@ -27,13 +27,13 @@ DEPS_MODERN=macros_modern.tex eacslversion.tex biblio.bib \
e-acsl: e-acsl-implementation.pdf e-acsl.pdf
all: e-acsl
-e-acsl-implementation.pdf: $(DEPS_MODERN)
+e-acsl-implementation.pdf: $(DEPS_MODERN) $(FRAMAC_MODERN)
e-acsl-implementation.tex: $(MAIN).tex Makefile
rm -f $@
sed -e '/PrintRemarks/s/%--//' $^ > $@
chmod a-w $@
-e-acsl.pdf: $(DEPS_MODERN)
+e-acsl.pdf: $(DEPS_MODERN) $(FRAMAC_MODERN)
e-acsl.tex: e-acsl-implementation.tex Makefile
rm -f $@
sed -e '/PrintImplementationRq/s/%--//' \
@@ -43,13 +43,6 @@ e-acsl.tex: e-acsl-implementation.tex Makefile
$(MAIN).pdf: $(DEPS_MODERN)
-DISTRIB_DIR=$(HOME)/frama-c/doc/www/distrib
-install: e-acsl-implementation.pdf e-acsl.pdf
- mkdir -p $(EACSL_DIR)/doc/manuals
- cp -f $^ $(EACSL_DIR)/doc/manuals
-
-include $(EACSL_DIR)/doc/support/MakeLaTeXModern
-
.PHONY: clean
clean:
rm -rf *~ *.aux *.log *.nav *.out *.snm *.toc *.lof *.pp *.bnf \
diff --git a/src/plugins/e-acsl/doc/refman/assertions.tex b/src/plugins/e-acsl/doc/refman/assertions.tex
index cb6a92931a6f11881d2ebff24922c092a30b9a95..9758d44bec67f2d6e22fe5c76d87e16ef81ce862 100644
--- a/src/plugins/e-acsl/doc/refman/assertions.tex
+++ b/src/plugins/e-acsl/doc/refman/assertions.tex
@@ -2,7 +2,7 @@
C-compound-statement ::= "{" declaration* statement* assertion+ "}"
\
C-statement ::= assertion statement \
- assertion-kind ::= "assert" | "check" \
+ assertion-kind ::= "assert" | clause-kind \
assertion ::= "/*@" assertion-kind pred ";" "*/" ;
| { "/*@" "for" id ("," id)* ":" assertion-kind pred ";" "*/" } ;
\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/biblio.bib b/src/plugins/e-acsl/doc/refman/biblio.bib
index ee79515d0c24ac9af512b4ecbd5f71a88be3ac1f..bb7f2f66e7fdac2a5da6eec09708123e29088bd1 100644
--- a/src/plugins/e-acsl/doc/refman/biblio.bib
+++ b/src/plugins/e-acsl/doc/refman/biblio.bib
@@ -2,82 +2,82 @@
@STRING{LNCS = {Lecture Notes in Computer Science}}
-@INPROCEEDINGS{jml,
- author = {Gary T. Leavens and K. Rustan M. Leino and Erik Poll
+@inproceedings{jml,
+ author = {Gary T. Leavens and K. Rustan M. Leino and Erik Poll
and Clyde Ruby and Bart Jacobs},
- title = {{JML}: notations and tools supporting detailed design in {Java}},
+ title = {{JML}: notations and tools supporting detailed design in {Java}},
booktitle = {{OOPSLA} 2000 Companion, Minneapolis, Minnesota},
- pages = {105--106},
- year = 2000
+ pages = {105--106},
+ year = 2000,
}
-@INPROCEEDINGS{chalin07,
- author = {Patrice Chalin},
- title = {A Sound Assertion Semantics for the Dependable Systems Evolution
+@inproceedings{chalin07,
+ author = {Patrice Chalin},
+ title = {A Sound Assertion Semantics for the Dependable Systems Evolution
Verifying Compiler},
booktitle = {Proceedings of the International Conference on Software
Engineering (ICSE'07)},
- pages = {23-33},
- year = 2007,
- address = {Los Alamitos, CA, USA},
- publisher = {IEEE Computer Society}
+ pages = {23-33},
+ year = 2007,
+ address = {Los Alamitos, CA, USA},
+ publisher = {IEEE Computer Society},
}
-@INPROCEEDINGS{chalin05,
- author = {Patrice Chalin},
- title = {Reassessing {JML}'s Logical Foundation},
+@inproceedings{chalin05,
+ author = {Patrice Chalin},
+ title = {Reassessing {JML}'s Logical Foundation},
booktitle = {Proceedings of the 7th Workshop on Formal Techniques for
Java-like Programs (FTfJP'05)},
- year = 2005,
- address = {Glasgow, Scotland},
- month = JUL
+ year = 2005,
+ address = {Glasgow, Scotland},
+ month = JUL,
}
@manual{acsl,
- title = {{ACSL, ANSI/ISO C Specification Language}},
- author = {Patrick Baudin and Pascal Cuoq and Jean-Christophe Filliâtre and
- Claude Marché and Benjamin Monate and Yannick Moy and Virgile Prevosto},
- note = {Vesion 1.12. \url{http://frama-c.com/acsl.html}},
+ title = {{ACSL, ANSI/ISO C Specification Language}},
+ author = {Patrick Baudin and Pascal Cuoq and Jean-Christophe Filliâtre and
+ Claude Marché and Benjamin Monate and Yannick Moy and Virgile Prevosto},
+ note = {\url{https://frama-c.com/html/acsl.html}},
}
@manual{acslimplem,
- title = {{ACSL version 1.12, Implementation in Silicon-20161101}},
- author = {Patrick Baudin and Pascal Cuoq and Jean-Christophe Filliâtre and
- Claude Marché and Benjamin Monate and Yannick Moy and Virgile Prevosto},
- note = {\url{http://frama-c.com/acsl.html}},
+ title = {{ACSL, Implementation in Frama-C}},
+ author = {Patrick Baudin and Pascal Cuoq and Jean-Christophe Filliâtre and
+ Claude Marché and Benjamin Monate and Yannick Moy and Virgile Prevosto},
+ note = {\url{https://frama-c.com/download/frama-c-acsl-implementation.pdf}},
}
@manual{framac,
- title = {Frama-C User Manual},
- author = {Loïc Correnson and Pascal Cuoq and Florent Kirchner and
-André Maroneze and
+ title = {Frama-C User Manual},
+ author = {Loïc Correnson and Pascal Cuoq and Florent Kirchner and
+André Maroneze and
Virgile Prevosto and Armand Puccetti and Julien Signoles and Boris Yakobowski},
- note = {\url{http://frama-c.com}},
+ note = {\url{https://frama-c.com/download/frama-c-user-manual.pdf}},
}
@manual{eacsl-plugin,
- title = {Frama-C's E-ACSL Plug-in},
+ title = {Frama-C's E-ACSL Plug-in},
author = {Julien Signoles and Kostyantyn Vorobyov},
- note = {\url{http://frama-c.com/eacsl.html}},
+ note = {\url{https://frama-c.com/fc-plugins/e-acsl.html}},
}
@manual{value,
- title = {Frama-C's value analysis plug-in},
- author = {Pascal Cuoq and Boris Yakobowski and Matthieu Lemerre and
-André Maroneze and Valentin Perelle and Virgile Prevosto},
- note = {\url{http://frama-c.com/value.html}},
+ title = {Frama-C's Evolved Value Analysis analysis plug-in},
+ author = {Pascal Cuoq and Boris Yakobowski and Matthieu Lemerre and
+André Maroneze and Valentin Perelle and Virgile Prevosto},
+ note = {\url{https://frama-c.com/fc-plugins/eva.html}},
}
-@BOOK{KR88,
- author = {Brian Kernighan and Dennis Ritchie},
- title = {The C Programming Language (2nd Ed.)},
+@book{KR88,
+ author = {Brian Kernighan and Dennis Ritchie},
+ title = {The C Programming Language (2nd Ed.)},
publisher = {Prentice-Hall},
- year = 1988
+ year = 1988,
}
-@MANUAL{standardc99,
- title = {The {ANSI C} standard ({C99})},
+@manual{standardc99,
+ title = {The {ANSI C} standard ({C99})},
organization = {International Organization for Standardization ({ISO})},
- key = {C99},
- note = {\url{http://www.open-std.org/JTC1/SC22/WG14/www/docs/n1124.pdf}}
+ key = {C99},
+ note = {\url{http://www.open-std.org/JTC1/SC22/WG14/www/docs/n1124.pdf}},
}
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index 9e419b0fc1d84c7e97754ddf782071981b44aea8..43abe7595881b43a5c89f9168f0982a7b04e2dd2 100644
--- a/src/plugins/e-acsl/doc/refman/changes_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex
@@ -1,6 +1,29 @@
\section{Changes}
\subsection*{Version \version}
+\begin{itemize}
+ \item Update according to \acsl 1.16
+ \begin{itemize}
+ \item \changeinsection{fn-behavior}{add the \lstinline|check| and
+ \lstinline|admit| clause kinds}
+ \item \changeinsection{assertions}{add the \lstinline|check| and
+ \lstinline|admit| clause kinds}
+ \item \changeinsection{generalized-invariants}{add the \lstinline|check| and
+ \lstinline|admit| clause kinds}
+ \item \changeinsection{loop_annot}{add the \lstinline|check| and
+ \lstinline|admit| clause kinds}
+ \end{itemize}
+\end{itemize}
+
+\subsection*{Version 1.15}
+\begin{itemize}
+\item Update according to \acsl 1.15:
+ \begin{itemize}
+ \item \changeinsection{ghost}{add the \lstinline|\\ghost| qualifier}
+ \end{itemize}
+\end{itemize}
+
+\subsection*{Version 1.14}
\begin{itemize}
\item Update according to \acsl 1.14:
\begin{itemize}
@@ -124,7 +147,7 @@ in \lstinline|\\at|}
{
\section{Changes in \eacsl Implementation}
-\subsection*{Version \eacslpluginversion}
+\subsection*{Version Titanium-22}
\begin{itemize}
\item \changeinsection{expressions}{support of bitwise operations}
diff --git a/src/plugins/e-acsl/doc/refman/fn_behavior.tex b/src/plugins/e-acsl/doc/refman/fn_behavior.tex
index 6db1b9dfa974cf8e773bb668896416f3de2f282f..b97f9d8b9824ba0186852d130b9be6fa0a40fedd 100644
--- a/src/plugins/e-acsl/doc/refman/fn_behavior.tex
+++ b/src/plugins/e-acsl/doc/refman/fn_behavior.tex
@@ -3,7 +3,9 @@
{ decreases-clause? } simple-clause*
named-behavior* completeness-clause*
\
- requires-clause ::= "requires" pred ";"
+ clause-kind ::= "check" | { "admit" }
+ \
+ requires-clause ::= clause-kind? "requires" pred ";"
\
{ decreases-clause } ::= { "decreases" term ("for" id)? ";" }
\
@@ -16,7 +18,7 @@
\
{ location } ::= { tset }
\
- ensures-clause ::= "ensures" pred ";"
+ ensures-clause ::= clause-kind? "ensures" pred ";"
\
named-behavior ::= "behavior" id ":" behavior-body
\
diff --git a/src/plugins/e-acsl/doc/refman/frama-c-book.cls b/src/plugins/e-acsl/doc/refman/frama-c-book.cls
deleted file mode 100644
index 562571271e1660418447e02673f904e42fa8ef00..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/doc/refman/frama-c-book.cls
+++ /dev/null
@@ -1,332 +0,0 @@
-% --------------------------------------------------------------------------
-% --- LaTeX Class for Frama-C Books ---
-% --------------------------------------------------------------------------
-\NeedsTeXFormat{LaTeX2e}
-\ProvidesPackage{frama-c-book}[2009/02/05 LaTeX Class for Frama-C Books]
-% --------------------------------------------------------------------------
-% --- Base Class management ---
-% --------------------------------------------------------------------------
-\LoadClass[a4paper,11pt,twoside,openright]{report}
-\DeclareOption{web}{\PassOptionsToPackage{colorlinks,urlcolor=blue}{hyperref}}
-\DeclareOption{paper}{\PassOptionsToPackage{pdfborder=0 0 0}{hyperref}}
-\ProcessOptions
-\RequirePackage{fullpage}
-\RequirePackage{hevea}
-\RequirePackage{ifthen}
-\RequirePackage[T1]{fontenc}
-\RequirePackage[latin1]{inputenc}
-\RequirePackage[a4paper,pdftex,pdfstartview=FitH]{hyperref}
-\RequirePackage{amssymb}
-\RequirePackage{xcolor}
-\RequirePackage[pdftex]{graphicx}
-\RequirePackage{xspace}
-\RequirePackage{makeidx}
-\RequirePackage[leftbars]{changebar}
-\RequirePackage[english]{babel}
-\RequirePackage{fancyhdr}
-\RequirePackage{titlesec}
-% --------------------------------------------------------------------------
-% --- Page Layout ---
-% --------------------------------------------------------------------------
-\setlength{\voffset}{-6mm}
-\setlength{\headsep}{8mm}
-\setlength{\footskip}{21mm}
-\setlength{\textheight}{238mm}
-\setlength{\topmargin}{0mm}
-\setlength{\textwidth}{155mm}
-\setlength{\oddsidemargin}{2mm}
-\setlength{\evensidemargin}{-2mm}
-\setlength{\changebarsep}{0.5cm}
-\setlength{\headheight}{13.6pt}
-\def\put@bg(#1,#2)#3{\setlength\unitlength{1cm}%
- \begin{picture}(0,0)(#1,#2)
- \put(0,0){\includegraphics{#3}}
- \end{picture}}
-\fancypagestyle{plain}{%
- \fancyfoot{}
- \fancyhead{}
- \fancyhead[LE]{\put@bg(2.4,27.425){frama-c-left.pdf}}
- \fancyhead[LO]{\put@bg(2.7,27.425){frama-c-right.pdf}}
- \fancyhead[CE]{\scriptsize\textsf{\leftmark}}
- \fancyhead[CO]{\scriptsize\textsf{\rightmark}}
- \fancyfoot[C]{\small\textsf{\thepage}}
- \renewcommand{\headrulewidth}{0pt}
- \renewcommand{\footrulewidth}{0pt}
-}
-\fancypagestyle{blank}{%
- \fancyfoot{}
- \fancyhead{}
- \fancyhead[LE]{\put@bg(2.4,27.425){frama-c-left.pdf}}
- \fancyhead[LO]{\put@bg(2.7,27.425){frama-c-right.pdf}}
-}
-%% Redefinition of cleardoublepage for empty page being blank
-\def\cleardoublepagewith#1{\clearpage\if@twoside \ifodd\c@page\else
-\hbox{}
-\thispagestyle{#1}
-\newpage
-\fi\fi}
-\def\cleardoublepage{\cleardoublepagewith{blank}}
-\pagestyle{plain}
-
-% --------------------------------------------------------------------------
-% --- Cover Page ---
-% --------------------------------------------------------------------------
-\newcommand{\coverpage}[1]{%
-\thispagestyle{empty}
-\setlength\unitlength{1cm}
-\begin{picture}(0,0)(3.27,26.75)
-\put(0,0){\includegraphics{frama-c-cover.pdf}}
-\put(2.0,20.5){\makebox[8cm][l]{\fontfamily{phv}\fontseries{m}\fontsize{24}{2}\selectfont #1}}
-\end{picture}
-}
-
-% --------------------------------------------------------------------------
-% --- Title Page ---
-% --------------------------------------------------------------------------
-\renewenvironment{titlepage}%
-{\cleardoublepagewith{empty}\thispagestyle{empty}\begin{center}}%
-{\end{center}}
-\renewcommand{\title}[2]{
-\vspace{20mm}
-{\Huge\bfseries #1}
-
-\bigskip
-
-{\LARGE #2}
-\vspace{20mm}
-}
-\renewcommand{\author}[1]{
-\vspace{20mm}
-
-{#1}
-
-\medskip
-}
-% --------------------------------------------------------------------------
-% --- Sectionning ---
-% --------------------------------------------------------------------------
-\titleformat{\chapter}[display]{\Huge\raggedleft}%
-{\huge\chaptertitlename\,\thechapter}{0.5em}{}
-\titleformat{\section}[hang]{\Large\bfseries}{\thesection}{1em}{}%
-[\vspace{-14pt}\rule{\textwidth}{0.1pt}\vspace{-8pt}]
-\titleformat{\subsubsection}[hang]{\bfseries}{}{}{}%
-[\vspace{-8pt}]
-
-% --------------------------------------------------------------------------
-% --- Main Text Style ---
-% --------------------------------------------------------------------------
-%\raggedright
-\setlength\parindent{0pt}
-\setlength\parskip{1ex plus 0.3ex minus 0.2ex}
-\newenvironment{warning}[1][Warning:]{\small\paragraph{#1}\itshape}{\vspace{\parskip}}
-\def\FramaC{\textsf{Frama-C}\xspace}
-% --------------------------------------------------------------------------
-% --- Listings ---
-% --------------------------------------------------------------------------
-\RequirePackage{listings}
-
-\lstdefinelanguage{ACSL}{%
- morekeywords={assert,assigns,assumes,axiom,axiomatic,behavior,behaviors,
- boolean,breaks,complete,continues,data,decreases,disjoint,ensures,
- exit_behavior,ghost,global,inductive,integer,invariant,lemma,logic,loop,
- model,predicate,reads,real,requires,returns,sizeof,strong,struct,terminates,type,
- union,variant},
-% otherkeywords={\\at,\\base_addr,\\block_length,\\false,\\fresh,\\from,
-% \\initialized,\\lambda,\\let,\\match,\\max,\\nothing,\\null,
-% \\numof,\\old,\\result,\\specified,\\strlen,\\sum,\\true,
-% \\valid,\\valid_range},
- keywordsprefix={\\},
- alsoletter={\\},
- morecomment=[l]{//}
-}
-
-\lstloadlanguages{[ANSI]C,[Objective]Caml,csh,ACSL}
-\definecolor{lstbg}{gray}{0.98}
-\definecolor{lstfg}{gray}{0.10}
-\definecolor{lstrule}{gray}{0.6}
-\definecolor{lstnum}{gray}{0.4}
-\definecolor{lsttxt}{rgb}{0.3,0.2,0.6}
-\definecolor{lstmodule}{rgb}{0.3,0.6,0.2}%{0.6,0.6,0.2}
-\definecolor{lstspecial}{rgb}{0.2,0.6,0.0}
-\definecolor{lstfile}{gray}{0.85}
-\newcommand{\lstbrk}{\mbox{$\color{blue}\scriptstyle\cdots$}}
-\def\lp@basic{\ifmmode\normalfont\mathtt\mdseries\scriptsize\else\normalfont\ttfamily\mdseries\scriptsize\fi}
-\def\lp@inline{\ifmmode\normalfont\mathtt\scriptstyle\else\normalfont\ttfamily\mdseries\small\fi}
-\def\lp@keyword{}
-\def\lp@special{\color{lstfg}}
-\def\lp@comment{\normalfont\ttfamily\mdseries}
-\def\lp@string{\color{lstfg}} \def\lp@ident{}
-\def\lp@number{\rmfamily\tiny\color{lstnum}}
-\lstdefinestyle{frama-c-style}{%
- basicstyle=\lp@inline,%
- identifierstyle=\lp@ident,%
- commentstyle=\lp@comment,%
- keywordstyle={\ifmmode\mathsf\else\sffamily\fi},%
- keywordstyle=[2]\lp@special,%
- stringstyle=\lp@string,%
- emphstyle=\lp@ident\underbar,%
- showstringspaces=false,%
- mathescape=true,%
- numberstyle=\lp@number,%
- xleftmargin=6ex,xrightmargin=2ex,%
- framexleftmargin=1ex,%
- frame=l,%
- framerule=1pt,%
- rulecolor=\color{lstrule},%
- backgroundcolor=\color{lstbg},%
- moredelim={*[s]{/*@}{*/}},%
- moredelim={*[l]{//@}},
- morecomment={[is]{//NOPP-BEGIN}{NOPP-END}},
- mathescape=true,
- escapechar=`
-% breaklines is broken when using a inline and background
-% breaklines,prebreak={\lstbrk},postbreak={\lstbrk},breakindent=5ex %
-}
-
-\lstdefinestyle{c}%
-{language={[ANSI]C},alsolanguage=ACSL,style=frama-c-style}
-\lstdefinestyle{c-basic}%
-{language={[ANSI]C},alsolanguage=ACSL,style=frama-c-style,basicstyle=\lp@basic}
-
-
-% --- C/ACSL Stuff ---------------------------------------------------------
-% Make 'c' the default style
-\lstset{style=c}
-
-\newcommand{\listinginput}[3][1]%
-{\lstinputlisting[style=c-basic,numbers=left,stepnumber=#1,firstnumber=#2]{#3}}
-
-\lstnewenvironment{listing}[2][1]%
-{\lstset{style=c-basic,numbers=left,stepnumber=#1,firstnumber=#2}}{}
-
-\lstnewenvironment{listing-nonumber}%
-{\lstset{style=c,numbers=none,basicstyle=\lp@basic}}{}
-
-% --- Verbatim Stuff -------------------------------------------------------
-\lstdefinelanguage{Shell}[]{csh}%
-{identifierstyle=\lp@basic,mathescape=false,backgroundcolor=,literate={\\\$}{\$}1}
-\lstnewenvironment{shell}[1][]{\lstset{language=Shell,basicstyle=\lp@basic,#1}}{}
-
-% ---- Stdout Stuff --------------------------------------------------------
-\lstdefinelanguage{Logs}[]{csh}%
-{identifierstyle=\lp@basic,backgroundcolor=}
-\lstnewenvironment{logs}[1][]{\lstset{language=Logs,basicstyle=\lp@basic,#1}}{}
-\newcommand{\logsinput}[1]%
-{\lstinputlisting[language=Logs,basicstyle=\lp@basic]{#1}}
-
-% --------------------------------------------------------------------------
-% --- Developer Code Stuff ---
-% --------------------------------------------------------------------------
-
-\newcommand{\listingname}[1]{\colorbox{lstfile}{\footnotesize\sffamily File \bfseries #1}\vspace{-4pt}}
-
-% --- Style ----------------------------------------------------------------
-\lstdefinestyle{framac-code-style}{%
-basicstyle=\lp@inline,%
-numberstyle=\lp@number,%
-keywordstyle=[1]\sffamily\color{lstmodule},%
-keywordstyle=[2]\sffamily\color{lstspecial},%
-keywordstyle=[3]\sffamily\bfseries,%
-identifierstyle=\rmfamily,%
-stringstyle=\ttfamily\color{lstfg},%
-commentstyle=\rmfamily\bfseries\color{lsttxt},%
-}
-\lstdefinestyle{framac-shell-style}{%
-mathescape=false,%
-basicstyle=\lp@basic,%
-numberstyle=\lp@number,%
-keywordstyle=\sffamily\bfseries,%
-keywordstyle=[1]\sffamily\color{lstmodule},%
-keywordstyle=[2]\sffamily\color{lstspecial},%
-keywordstyle=[3]\sffamily\bfseries,%
-identifierstyle=\ttfamily,%
-stringstyle=\ttfamily\color{lstfg},%
-commentstyle=\rmfamily\bfseries\color{lsttxt},%
-literate={\\\$}{\$}1,%
-}
-% --- Configure ------------------------------------------------------------
-\lstdefinelanguage{Configure}[]{csh}{%
-style=framac-shell-style,%
-morekeywords={fi},%
-}
-\lstnewenvironment{configurecode}[1][]%
-{\lstset{language=Configure,#1}}{}
-\newcommand{\configureinput}[1]{\lstinputlisting[language=Configure]{#1}}
-% --- Makefile ------------------------------------------------------------
-\lstdefinelanguage{Makefile}[]{make}{%
-style=framac-shell-style,%
-morekeywords={include},%
-}
-\lstnewenvironment{makefilecode}[1][]%
-{\lstset{language=Makefile,#1}}{}
-\newcommand{\makefileinput}[1]{\lstinputlisting[language=Makefile]{#1}}
-% --- C- for Developer ----------------------------------------------------
-\lstdefinestyle{framac-code}%
- {language={[ANSI]C},alsolanguage=ACSL,style=framac-code-style,basicstyle=\lp@basic}
-\lstnewenvironment{ccode}[1][]%
-{\lstset{language={[ANSI]C},alsolanguage=ACSL,style=framac-code-style,basicstyle=\lp@basic,#1}}{}
-\newcommand{\cinput}[1]%
-{\lstinputlisting[language={[ANSI]C},alsolanguage=ACSL,style=framac-code-style,basicstyle=\lp@basic]{#1}}
-\newcommand{\cinline}[1]%
-{\lstinline[style=framac-code]{#1}}
-% --- Ocaml ----------------------------------------------------------------
-\lstdefinelanguage{Ocaml}[Objective]{Caml}{%
-style=framac-code-style,%
-deletekeywords={when,module,struct,sig,begin,end},%
-morekeywords=[2]{failwith,raise,when},%
-morekeywords=[3]{module,struct,sig,begin,end},%
-literate=%
-{~}{${\scriptstyle\thicksim}$}1%
-{<}{$<$}1%
-{>}{$>$}1%
-{->}{$\rightarrow$}1%
-{<-}{$\leftarrow$}1%
-{:=}{$\leftarrow$}1%
-{<=}{$\leq$}1%
-{>=}{$\geq$}1%
-{==}{$\equiv$}1%
-{!=}{$\not\equiv$}1%
-{<>}{$\neq$}1%
-{'a}{$\alpha$}1%
-{'b}{$\beta$}1%
-{'c}{$\gamma$}1%
-{µ}{`{}}1%
-}
-
-\lstdefinestyle{ocaml-basic}%
-{language=Ocaml,basicstyle=\lp@basic}
-\newcommand{\ocamlinput}[2][]{\lstinputlisting[style=ocaml-basic,#1]{#2}}
-\lstnewenvironment{ocamlcode}[1][]{\lstset{style=ocaml-basic,#1}}{}
-% --------------------------------------------------------------------------
-\lstdefinelanguage{Why}{%
- morekeywords={
- type, logic, axiom, predicate, goal,
- forall, let, in,
- },
- morecomment=[s]{(*}{*)},
- alsoletter={_},
- literate=%
- {->}{$\Rightarrow$}1%
- {forall}{$\forall$}1%
- {not}{$\neg$}1%
- {<>}{$\neq$}1%
- {...}{$\dots$}1%
- %{_}{\_}1%
- %{_}{{\rule[0pt]{1ex}{.2pt}}}1%
- }
-
-\lstdefinestyle{why-style}{%
-language=Why,%
-style=framac-code-style,%
-basicstyle=\lp@basic,%
-}
-
-\lstnewenvironment{whycode}[1][]{\lstset{style=why-style,#1}}{}
-\newcommand{\whyinput}[1]%
-{\lstinputlisting[style=why-style]{#1}}
-\newcommand{\whyinline}[1]%
-{\lstinline[style=why-style]{#1}}
-
-% --------------------------------------------------------------------------
-% --- End. ---
-% --------------------------------------------------------------------------
diff --git a/src/plugins/e-acsl/doc/refman/frama-c-cover.pdf b/src/plugins/e-acsl/doc/refman/frama-c-cover.pdf
deleted file mode 100644
index c0b6101f8a9a665f5ca48783d8d1dfefc765ed4a..0000000000000000000000000000000000000000
Binary files a/src/plugins/e-acsl/doc/refman/frama-c-cover.pdf and /dev/null differ
diff --git a/src/plugins/e-acsl/doc/refman/frama-c-left.pdf b/src/plugins/e-acsl/doc/refman/frama-c-left.pdf
deleted file mode 100644
index 54a64f214ddc0e9dc88eec38303070540962545d..0000000000000000000000000000000000000000
Binary files a/src/plugins/e-acsl/doc/refman/frama-c-left.pdf and /dev/null differ
diff --git a/src/plugins/e-acsl/doc/refman/frama-c-right.pdf b/src/plugins/e-acsl/doc/refman/frama-c-right.pdf
deleted file mode 100644
index 13ba3e3c03fdca91713629b5b115643281f5c109..0000000000000000000000000000000000000000
Binary files a/src/plugins/e-acsl/doc/refman/frama-c-right.pdf and /dev/null differ
diff --git a/src/plugins/e-acsl/doc/refman/generalinvariants.tex b/src/plugins/e-acsl/doc/refman/generalinvariants.tex
index 246a377d67ff92011258af572e78b8bc3ecc0daf..f72665035ec6cdbece7c6aed55c522c8aac1b842 100644
--- a/src/plugins/e-acsl/doc/refman/generalinvariants.tex
+++ b/src/plugins/e-acsl/doc/refman/generalinvariants.tex
@@ -1,4 +1,4 @@
\begin{syntax}
- assertion ::= [ "/*@" "invariant" pred ";" "*/" ] ;
- | [ { "/*@" "for" id ("," id)* ":" "invariant" pred ";" "*/" } ] ;
+ assertion ::= [ "/*@" clause-kind? "invariant" pred ";" "*/" ] ;
+ | [ { "/*@" "for" id ("," id)* ":" clause-kind? "invariant" pred ";" "*/" } ] ;
\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/ghost.tex b/src/plugins/e-acsl/doc/refman/ghost.tex
index 1d6d0e9c9e6bd8ff337f7f0f3e4ba13c4085eda5..6d5cefc68a1abf69dad33a52b5270d8cd7e782cc 100644
--- a/src/plugins/e-acsl/doc/refman/ghost.tex
+++ b/src/plugins/e-acsl/doc/refman/ghost.tex
@@ -1,5 +1,8 @@
\begin{syntax}
+ C-type-qualifier ::= C-type-qualifier ;
+ | { "\ghost" } ; only in ghost
+ \
ghost-type-specifier ::= C-type-specifier ;
| { logic-type } \
declaration ::= C-declaration ;
@@ -16,7 +19,8 @@
"(" C-argument-expression-list? ")";
{"/*@" "ghost"} ;
{ "(" ghost-argument-expression-list ")"};
- { "*/"} ; call with ghosts
+ { "*/"} ; call
+ ; with ghosts
\
statement ::= C-statement ;
| statements-ghost \
diff --git a/src/plugins/e-acsl/doc/refman/loops.tex b/src/plugins/e-acsl/doc/refman/loops.tex
index 5d1fa33003cbcc7674420f0e8f2231c7e12ca625..1de09ce3a638ab6f99d83e5be39edbb0b1cf955e 100644
--- a/src/plugins/e-acsl/doc/refman/loops.tex
+++ b/src/plugins/e-acsl/doc/refman/loops.tex
@@ -16,13 +16,13 @@
loop-clause ::= loop-invariant ;
| { loop-assigns }
\
- [ loop-invariant ] ::= [ "loop" "invariant" pred ";" ] ;
+ [ loop-invariant ] ::= { clause-kind? } [ "loop" "invariant" pred ";" ] ;
\
{ loop-assigns } ::= { "loop" "assigns" locations ";" } ;
\
{ loop-behavior } ::= { "for" id ("," id)* ":" } ;
- { loop-clause* } ; \hspace{-30mm} annotation for behavior $id$
+ { loop-clause* } ; \hspace{-35mm} annotation for behavior $id$
\
{ loop-variant } ::= { "loop" "variant" term ";" } ;
- | { "loop" "variant" term "for" id ";" } ; \hspace{-30mm} variant for relation $id$
+ | { "loop" "variant" term "for" id ";" } ; \hspace{-35mm} variant for relation $id$
\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/macros_modern.tex b/src/plugins/e-acsl/doc/refman/macros_modern.tex
index 86b8cd8244b4805b854fb1d1ea5450ab67ab370e..0034ff0ed628dbc05d558731db395e23dc9d32cd 100644
--- a/src/plugins/e-acsl/doc/refman/macros_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/macros_modern.tex
@@ -1,5 +1,5 @@
-%%% Environnements dont le corps est suprimé, et
-%%% commandes dont la définition est vide,
+%%% Environnements dont le corps est suprimé, et
+%%% commandes dont la définition est vide,
%%% lorsque PrintRemarks=false
\usepackage{comment}
@@ -105,7 +105,7 @@
\ifthenelse{\isundefined{\myrq}}{}{\footnote{\myrq}}\end{changebar}}}%
{\excludecomment{notreviewedenv}}
-%%% Commandes et environnements pour la version relative à l'implementation
+%%% Commandes et environnements pour la version relative à l'implementation
\newcommand{\highlightnotimplemented}{%
\ifthenelse{\boolean{ColorImplementationRq}}{\color{red}}%
{}%
diff --git a/src/plugins/e-acsl/doc/refman/main.tex b/src/plugins/e-acsl/doc/refman/main.tex
index 4b6ad34ce838bdf222b826029e49d259cd757613..f64b135dd8fbdb26c3847218c9196aebe3fd4971 100644
--- a/src/plugins/e-acsl/doc/refman/main.tex
+++ b/src/plugins/e-acsl/doc/refman/main.tex
@@ -24,7 +24,7 @@
\usepackage{alltt}
\makeindex
-\newcommand{\eacsllangversion}{1.14\xspace}
+\newcommand{\eacsllangversion}{1.16\xspace}
\newcommand{\version}{\eacsllangversion\xspace}
\renewcommand{\textfraction}{0.01}
diff --git a/src/plugins/e-acsl/doc/refman/speclang_modern.tex b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
index 261843a39061bc86c85aa25af87979fc41abcb77..a15c8384b4a34fee6955f3a6b4bbfe4bcba1a38a 100644
--- a/src/plugins/e-acsl/doc/refman/speclang_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
@@ -290,11 +290,6 @@ It is not possible to define logic types introduced by the specification writer
\eacsl plug-in.
\end{notimplementedenv}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-\subsection{String literals}
-\nodiff
-
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -385,7 +380,7 @@ set of all integers between 0 and 9 and between 20 and 29.
\begin{notimplementedenv}
Ranges are currently only supported in memory built-ins described in
- Section~\ref{subsec:memory} and~\ref{sec:dangling}.
+ Section~\ref{subsec:memory},~\ref{sec:initialized} and~\ref{sec:dangling}.
\begin{example}
The predicate \lstinline|\valid(&t[0 .. 9])| is supported and denotes that
@@ -484,6 +479,7 @@ loop invariants are not inductive.
\end{example}
\subsubsection{General inductive invariant}
+\label{sec:generalized-invariants}
Syntax of these kinds of invariant is shown Figure~\ref{fig:advancedinvariants}
\begin{figure}[t]
@@ -725,7 +721,7 @@ predicates which are related to memory location.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\subsection{Allocation and deallocation}
+\subsection{Dynamic allocation and deallocation}
\difficultswhy{All these constructs}{the implementation of a memory model}
\label{sec:alloc-dealloc}
\nodiff
@@ -852,13 +848,18 @@ same than the one of \acsl.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\section{Undefined values, dangling pointers}
+\section{Initialization and undefined values}
+\label{sec:initialized}
+\nodiff
+
+\difficultwhy{\lstinline|\\initialized|}{the implementation of a memory model}
+
+\section{Dangling pointers}
\label{sec:dangling}
\nodiff
-\difficultswhy{\lstinline|\\initialized| and
- \notimplemented{\lstinline|\\dangling|}}{the implementation of a memory
- model}
+\difficultwhy{\notimplemented{\lstinline|\\dangling|}}{the implementation of a
+ memory model}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -867,3 +868,17 @@ same than the one of \acsl.
\section{Well-typed pointers}
\label{sec:typedpointers}
\absentexperimental
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Logic attribute annotations}
+\absentexperimental
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Preprocessing for ACSL}
+\nodiff
diff --git a/src/plugins/e-acsl/doc/support/MakeLaTeXModern b/src/plugins/e-acsl/doc/support/MakeLaTeXModern
index d1b204a14b1ea83265f8686f43d31cfa3f116629..bcbb0d6648b70222cf66d404bf30482d813d0efb 100644
--- a/src/plugins/e-acsl/doc/support/MakeLaTeXModern
+++ b/src/plugins/e-acsl/doc/support/MakeLaTeXModern
@@ -1,25 +1,2 @@
-FRAMAC_MODERN=frama-c-book.cls frama-c-cover.pdf frama-c-left.pdf frama-c-right.pdf
-
-frama-c-book.cls: ../frama-c-book.cls
- @rm -f $@
- @cp $< .
- @chmod a-w $@
- @echo "import $<"
-
-frama-c-cover.pdf: ../frama-c-cover.pdf
- @rm -f $@
- @cp $< .
- @chmod a-w $@
- @echo "import $<"
-
-frama-c-right.pdf: ../frama-c-right.pdf
- @rm -f $@
- @cp $< .
- @chmod a-w $@
- @echo "import $<"
-
-frama-c-left.pdf: ../frama-c-left.pdf
- @rm -f $@
- @cp $< .
- @chmod a-w $@
- @echo "import $<"
+FRAMAC_DOC_ROOT_DIR:=../../../../../doc
+include $(FRAMAC_DOC_ROOT_DIR)/MakeLaTeXModern
diff --git a/src/plugins/e-acsl/doc/userman/.gitignore b/src/plugins/e-acsl/doc/userman/.gitignore
index f0de8a3d55fd37efe5d3b79a83031b8ab3c1a1e3..671d4c89b275efe0a0340cb7031bff9ec005da2e 100644
--- a/src/plugins/e-acsl/doc/userman/.gitignore
+++ b/src/plugins/e-acsl/doc/userman/.gitignore
@@ -1 +1,5 @@
+frama-c-book.cls
+frama-c-cover.pdf
+frama-c-left.pdf
+frama-c-right.pdf
main.pdf
diff --git a/src/plugins/e-acsl/doc/userman/Makefile b/src/plugins/e-acsl/doc/userman/Makefile
index 558ae875bed315e79fecefe3aac3ff02c1295a00..8486028efd975dbb02cf54f4540b6aaf3fafa1d7 100644
--- a/src/plugins/e-acsl/doc/userman/Makefile
+++ b/src/plugins/e-acsl/doc/userman/Makefile
@@ -1,8 +1,12 @@
-default: main.pdf
+default: all
-EACSL_DIR=../..
+EACSL_DIR:=../..
include $(EACSL_DIR)/doc/Makefile.common
+##########
+# Inputs #
+##########
+
MAIN=main
C_CODE=$(wildcard examples/*.[ci])
@@ -15,11 +19,19 @@ DEPS_MODERN=eacslversion.tex biblio.bib macros.tex \
$(C_CODE) \
$(VERSION_FILE)
-default: main.pdf
+##############
+# Main rules #
+##############
+
+.PHONY: all main default
+$(MAIN): $(MAIN).pdf
+all: $(MAIN)
-main.pdf: $(DEPS_MODERN)
+$(MAIN).pdf: $(DEPS_MODERN) $(FRAMAC_MODERN)
-DISTRIB_DIR=$(HOME)/frama-c/doc/www/distrib
-install:
- mkdir -p $(EACSL_DIR)/doc/manuals/
- cp -f main.pdf $(EACSL_DIR)/doc/manuals/e-acsl-manual.pdf
+.PHONY: clean
+clean:
+ rm -rf *~ *.aux *.log *.nav *.out *.snm *.toc *.lof *.pp *.bnf \
+ *.haux *.hbbl *.htoc \
+ *.cb *.cm? *.bbl *.blg *.idx *.ind *.ilg \
+ transf trans.ml pp.ml pp
diff --git a/src/plugins/e-acsl/doc/userman/biblio.bib b/src/plugins/e-acsl/doc/userman/biblio.bib
index 63e742e131e03df9a6f38531c3b56c3ad2b18246..dc9980cd64f8211e781542f9231e63b231e237ce 100644
--- a/src/plugins/e-acsl/doc/userman/biblio.bib
+++ b/src/plugins/e-acsl/doc/userman/biblio.bib
@@ -1,119 +1,119 @@
@manual{userman,
title = {Frama-C User Manual},
- author = {Loïc Correnson and Pascal Cuoq and Florent Kirchner and
- André Maroneze and Virgile Prevosto and
+ author = {Loïc Correnson and Pascal Cuoq and Florent Kirchner and
+ André Maroneze and Virgile Prevosto and
Armand Puccetti and Julien Signoles and
Boris Yakobowski},
- note = {\url{http://frama-c.cea.fr/download/user-manual.pdf}}
+ note = {\url{https://frama-c.com/download/frama-c-user-manual.pdf}},
}
@manual{plugin-dev-guide,
- author = {Julien Signoles and Loïc Correnson and Matthieu Lemerre and
+ author = {Julien Signoles and Loïc Correnson and Matthieu Lemerre and
Virgile Prevosto},
title = {{Frama-C Plug-in Development Guide}},
- note = {\newline \url{http://frama-c.cea.fr/download/plugin-developer.pdf}},
+ note = {\newline \url{https://frama-c.com/download/frama-c-plugin-development-guide.pdf}},
}
@manual{eva,
author = {David B\"uhler and Pascal Cuoq and Boris Yakobowski and
- Matthieu Lemerre and André Maroneze and Valentin Perelle and
+ Matthieu Lemerre and André Maroneze and Valentin Perelle and
Virgile Prevosto},
title = {{EVA} -- The Evolved Value Analysis plug-in},
- note = {\mbox{\url{http://frama-c.cea.fr/download/value-analysis.pdf}}},
+ note = {\mbox{\url{https://frama-c.com/download/frama-c-value-analysis.pdf}}},
}
@manual{acsl,
- author = {Baudin, Patrick and Filli\^{a}tre, Jean-Christophe and
+ author = {Baudin, Patrick and Filli\^{a}tre, Jean-Christophe and
March\'{e}, Claude and Monate, Benjamin and Moy, Yannick and
Prevosto, Virgile},
- title = {{ACSL: ANSI/ISO C Specification Language.}},
+ title = {{ACSL: ANSI/ISO C Specification Language.}},
}
@manual{acsl-implem,
- author = {Baudin, Patrick and Pascal Cuoq and Filli\^{a}tre, Jean-Christophe
+ author = {Baudin, Patrick and Pascal Cuoq and Filli\^{a}tre, Jean-Christophe
and March\'{e}, Claude and Monate, Benjamin and Moy, Yannick and
Prevosto, Virgile},
- title = {ACSL: ANSI/ISO C Specification Language. ---
+ title = {ACSL: ANSI/ISO C Specification Language. ---
Frama-C Silicon implementation.},
}
@manual{eacsl,
author = {Julien Signoles},
title = {E-ACSL: Executable ANSI/ISO C Specification Language.},
- note = {\mbox{\url{http://frama-c.com/download/e-acsl/e-acsl.pdf}}}
+ note = {\mbox{\url{http://frama-c.com/download/e-acsl/e-acsl.pdf}}},
}
@manual{eacsl-implem,
author = {Julien Signoles},
title = {E-ACSL. Implementation in Frama-C Plug-in E-ACSL},
- note = {\mbox{\url{http://frama-c.com/download/e-acsl/e-acsl-implementation.pdf}}}
+ note = {\mbox{\url{http://frama-c.com/download/e-acsl/e-acsl-implementation.pdf}}},
}
@habilitation{signoles18hdr,
author = {Signoles, Julien},
- title = {{From Static Analysis to Runtime Verification with Frama-C and E-ACSL}},
- year = 2018,
- month = jul,
+ title = {{From Static Analysis to Runtime Verification with Frama-C and E-ACSL}},
+ year = 2018,
+ month = jul,
school = {Universit\'e Paris-Sud, Orsay, France},
- note = {Habilitation Thesis},
- url = {publis/hdr.pdf}
+ note = {Habilitation Thesis},
+ url = {publis/hdr.pdf},
}
@inproceedings{kosmatov20rv,
- author = {Kosmatov, Nikolai and Maurica, Fonenantsoa and Signoles, Julien},
- title = {{Efficient Runtime Assertion Checking for Properties over
+ author = {Kosmatov, Nikolai and Maurica, Fonenantsoa and Signoles, Julien},
+ title = {{Efficient Runtime Assertion Checking for Properties over
Mathematical Numbers}},
booktitle = {International Conference on Runtime Verification (RV)},
- year = 2020,
- month = oct,
+ year = 2020,
+ month = oct,
}
@inproceedings{ly18hilt,
- author = {Dara Ly and Nikolai Kosmatov and Fr\'ed\'eric Loulergue
+ author = {Dara Ly and Nikolai Kosmatov and Fr\'ed\'eric Loulergue
and Julien Signoles},
- title = {Soundness of a Dataflow Analysis for Memory Monitoring},
+ title = {Soundness of a Dataflow Analysis for Memory Monitoring},
booktitle = {Workshop on Languages and Tools for Ensuring Cyber-Resilience in
Critical Software-Intensive Systems (HILT)},
- year = 2018,
- month = nov,
+ year = 2018,
+ month = nov,
}
@inproceedings{rvcubes17tool,
- author = {Julien Signoles and Nikolai Kosmatov and Kostyantyn Vorobyov},
- title = {{E-ACSL, a Runtime Verification Tool for Safety and Security of C
+ author = {Julien Signoles and Nikolai Kosmatov and Kostyantyn Vorobyov},
+ title = {{E-ACSL, a Runtime Verification Tool for Safety and Security of C
Programs. Tool Paper}},
booktitle = {International Workshop on Competitions, Usability, Benchmarks,
Evaluation, and Standardisation for Runtime Verification Tools (RV-CuBES)},
- year = 2017,
- month = sep,
+ year = 2017,
+ month = sep,
}
@inproceedings{sac13,
- author = {Micka\"{e}l Delahaye and Nikolai Kosmatov and Julien Signoles},
- title = {Common Specification Language for Static and Dynamic Analysis of
+ author = {Micka\"{e}l Delahaye and Nikolai Kosmatov and Julien Signoles},
+ title = {Common Specification Language for Static and Dynamic Analysis of
{C} Programs},
booktitle = {the 28th Annual ACM Symposium on Applied Computing ({SAC})},
publisher = {ACM},
- year = 2013,
- month = mar,
- pages = {1230--1235},
+ year = 2013,
+ month = mar,
+ pages = {1230--1235},
}
@inproceedings{rv13tutorial,
- author = {Nikolaï Kosmatov and Julien Signoles},
- title = {A Lesson on Runtime Assertion Checking with {Frama-C}},
+ author = {Nikolaï Kosmatov and Julien Signoles},
+ title = {A Lesson on Runtime Assertion Checking with {Frama-C}},
booktitle = {International Conference on Runtime Verification ({RV 2013})},
publisher = {Springer},
- series= {LNCS},
- volume= {8174},
- pages= {386--399},
- year = 2013,
- month = sep,
+ series = {LNCS},
+ volume = {8174},
+ pages = {386--399},
+ year = 2013,
+ month = sep,
}
@manual{wp,
- author = {Patrick Baudin and François Bobot and Loïc Correnson
+ author = {Patrick Baudin and François Bobot and Loïc Correnson
and Zaynah Dargaye},
title = {{Frama-C}'s {WP} plug-in},
note = {\mbox{\url{http://frama-c.com/download/frama-c-wp-manual.pdf}}},
@@ -126,68 +126,74 @@ Evaluation, and Standardisation for Runtime Verification Tools (RV-CuBES)},
}
@article{fac15,
-year={2015},
-month={jan},
-journal={Formal Aspects of Computing},
-title={{Frama-C: A Software Analysis Perspective}},
-publisher={Springer},
-keywords={Formal verification; Static analysis; Dynamic analysis; C},
-author={Kirchner, Florent and Kosmatov, Nikolai and Prevosto, Virgile and
+ year = {2015},
+ month = {jan},
+ journal = {Formal Aspects of Computing},
+ title = {{Frama-C: A Software Analysis Perspective}},
+ publisher = {Springer},
+ keywords = {Formal verification; Static analysis; Dynamic analysis; C},
+ author = {Kirchner, Florent and Kosmatov, Nikolai and Prevosto, Virgile and
Signoles, Julien and Yakobowski, Boris},
-pages={1-37},
+ pages = {1-37},
}
@article{runtime-assertion-checking,
- author = {Lori A. Clarke and
+ author = {Lori A. Clarke and
David S. Rosenblum},
- title = {A historical perspective on runtime assertion checking in
+ title = {A historical perspective on runtime assertion checking in
software development},
- journal = {ACM SIGSOFT Software Engineering Notes},
- volume = {31},
- number = {3},
- year = {2006},
- pages = {25-37},
+ journal = {ACM SIGSOFT Software Engineering Notes},
+ volume = {31},
+ number = {3},
+ year = {2006},
+ pages = {25-37},
}
@inproceedings{rv13,
- author = {Nikolaï Kosmatov and Guillaume Petiot and Julien Signoles},
- title = {An Optimized Memory Monitoring for Runtime Assertion Checking of
+ author = {Nikolaï Kosmatov and Guillaume Petiot and Julien Signoles},
+ title = {An Optimized Memory Monitoring for Runtime Assertion Checking of
{C} Programs},
booktitle = {International Conference on
Runtime Verification ({RV 2013})},
publisher = {Springer},
- series = {LNCS},
- volume = {8174},
- pages = {167--182},
- year = 2013,
- month = sep,
+ series = {LNCS},
+ volume = {8174},
+ pages = {167--182},
+ year = 2013,
+ month = sep,
}
@inproceedings{jfla15,
- title = {{Rester statique pour devenir plus rapide, plus pr{\'e}cis et plus mince}},
- author = {Arvid Jakobsson and Nikolai Kosmatov and Julien Signoles},
- booktitle = {Journées Francophones des Langages Applicatifs (JFLA'15)},
- editor = {David Baelde and Jade Alglave},
- year = {2015},
- month = jan,
- note = {In French},
+ title = {{Rester statique pour devenir plus rapide, plus pr{\'e}cis et plus mince}},
+ author = {Arvid Jakobsson and Nikolai Kosmatov and Julien Signoles},
+ booktitle = {Journées Francophones des Langages Applicatifs (JFLA'15)},
+ editor = {David Baelde and Jade Alglave},
+ year = {2015},
+ month = jan,
+ note = {In French},
}
@article{scp16,
- title = {{Fast as a Shadow, Expressive as a Tree: Optimized Memory Monitoring
+ title = {{Fast as a Shadow, Expressive as a Tree: Optimized Memory Monitoring
for C}},
- author = {Arvid Jakobsson and Nikolai Kosmatov and Julien Signoles},
- journal = {Science of Computer Programming},
+ author = {Arvid Jakobsson and Nikolai Kosmatov and Julien Signoles},
+ journal = {Science of Computer Programming},
publisher = {Elsevier},
- pages = {226-246},
- language = {English},
- year = {2016},
- month = oct,
-}
-
-@article{pldi16,
- title = {{Shadow State Encoding for Efficient Monitoring of Block-level
-Properties}},
- author = {Kostyantyn Vorobyov and Julien Signoles and Nikolai Kosmatov},
- note = {Submitted for publication},
+ pages = {226-246},
+ language = {English},
+ year = {2016},
+ month = oct,
+}
+
+@inproceedings{vorobyov17ismm,
+ author = { Vorobyov, Kostyantyn and Signoles, Julien and Kosmatov, Nikolai },
+ booktitle = { International Symposium on Memory Management (ISMM) },
+ title = { Shadow State Encoding for Efficient Monitoring of Block-level Properties },
+ year = { 2017 },
+ month = jun,
+ pages = {47--58},
+ location = { Barcelona, Spain },
+ doi = { 10.1145/3092255 },
+ pdf = {publis/2017_ismm.pdf},
+ publisher = { {ACM} },
}
diff --git a/src/plugins/e-acsl/doc/userman/changes.tex b/src/plugins/e-acsl/doc/userman/changes.tex
index 034766eaca3e2ae51a6764834055cbb5dc55777e..a96a51aa43ba5125e0b05d9c209a6c45ff75909b 100644
--- a/src/plugins/e-acsl/doc/userman/changes.tex
+++ b/src/plugins/e-acsl/doc/userman/changes.tex
@@ -3,9 +3,10 @@
This chapter summarizes the changes in this documentation between each \eacsl
release. First we list changes of the last release.
-\section*{E-ACSL \eacslpluginversion}
+\section*{E-ACSL 22.0 Titanium}
\begin{itemize}
+\item Update every section with changes to \framac and \eacslgcc output
\item \textbf{Simple Example}: Remove option \texttt{-e-acsl-check}
\item \textbf{Combining E-ACSL with Other PLug-ins}: \texttt{-e-acsl-prepare} is
no more necessary.
@@ -30,7 +31,7 @@ release. First we list changes of the last release.
\textbf{-e-acsl-prepare}.
\item \textbf{Known Limitations}: Replace section ``Limitations of E-ACSL
Monitoring Libraries'' by the new section ``Supported Systems''.
-\item \textbf{Known Limitations}: Add limitation about monitoring of variables
+\item \textbf{Known Limitations}: Add limitation about monitoring of variables
with incomplete types.
\end{itemize}
diff --git a/src/plugins/e-acsl/doc/userman/examples/assert_sign.c b/src/plugins/e-acsl/doc/userman/examples/assert_sign.c
index ce2e56c6fb9579df15f0211548e355dfcd5af08d..7d2fb1842f2799b6c9fe34eac9d7d08429086828 100644
--- a/src/plugins/e-acsl/doc/userman/examples/assert_sign.c
+++ b/src/plugins/e-acsl/doc/userman/examples/assert_sign.c
@@ -1,2 +1,2 @@
-void __e_acsl_assert(int pred, char *kind,
- char *func_name, char *pred_text, int line);
+void __e_acsl_assert(int pred, const char *kind, const char *func_name,
+ const char *pred_txt, const char * file, int line);
diff --git a/src/plugins/e-acsl/doc/userman/examples/instrumented_first.c b/src/plugins/e-acsl/doc/userman/examples/instrumented_first.c
index a940f8c891f99d03379b2ab99afd8c0164958126..54948acabb34603ad326da9f69746e4e096e980f 100644
--- a/src/plugins/e-acsl/doc/userman/examples/instrumented_first.c
+++ b/src/plugins/e-acsl/doc/userman/examples/instrumented_first.c
@@ -1,13 +1,14 @@
\begin{shell}
\$ frama-c -e-acsl first.i -then-last -print
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing first.i (no preprocessing)
[e-acsl] beginning translation.
+[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[e-acsl] translation done in project "e-acsl".
/* Generated by Frama-C */
+#include "stddef.h"
#include "stdio.h"
-#include "stdlib.h"
+struct __e_acsl_contract_t;
+typedef struct __e_acsl_contract_t __attribute__((__FC_BUILTIN__)) __e_acsl_contract_t;
struct __e_acsl_mpz_struct {
int _mp_alloc ;
int _mp_size ;
@@ -15,39 +16,56 @@ struct __e_acsl_mpz_struct {
};
typedef struct __e_acsl_mpz_struct __e_acsl_mpz_struct;
typedef __e_acsl_mpz_struct ( __attribute__((__FC_BUILTIN__)) __e_acsl_mpz_t)[1];
-/*@ ghost extern int __e_acsl_init; */
-
+struct __e_acsl_mpq_struct {
+ __e_acsl_mpz_struct _mp_num ;
+ __e_acsl_mpz_struct _mp_den ;
+};
+typedef struct __e_acsl_mpq_struct __e_acsl_mpq_struct;
+typedef __e_acsl_mpq_struct ( __attribute__((__FC_BUILTIN__)) __e_acsl_mpq_t)[1];
+typedef unsigned long __e_acsl_mp_bitcnt_t;
/*@ requires pred != 0;
assigns \nothing; */
- __attribute__((__FC_BUILTIN__)) void __e_acsl_assert(int pred, char *kind,
- char *fct,
- char *pred_txt,
+ __attribute__((__FC_BUILTIN__)) void __e_acsl_assert(int pred,
+ char const *kind,
+ char const *fct,
+ char const *pred_txt,
+ char const *file,
int line);
-/*@ assigns \nothing; */
- __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_init(int *argc_ref,
- char ***argv,
- size_t ptr_size);
-
extern size_t __e_acsl_heap_allocation_size;
-/*@
-predicate diffSize{L1, L2}(integer i) =
- \at(__e_acsl_heap_allocation_size,L1) -
- \at(__e_acsl_heap_allocation_size,L2) == i;
+extern size_t __e_acsl_heap_allocated_blocks;
+
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
+
+/*@ ghost extern int __e_acsl_init; */
+
+long valid_nstring(char *s, long n, int wrtbl);
+
+long valid_nwstring(wchar_t *s, long n, int wrtbl);
+
+__inline static long valid_string__fc_inline(char *s, int wrtbl)
+{
+ long tmp;
+ tmp = valid_nstring(s,(long)(-1),wrtbl);
+ return tmp;
+}
+
+__inline static long valid_wstring__fc_inline(wchar_t *s, int wrtbl)
+{
+ long tmp;
+ tmp = valid_nwstring(s,(long)(-1),wrtbl);
+ return tmp;
+}
-*/
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)4);
int x = 0;
- /*@ assert x == 0; */
- __e_acsl_assert(x == 0,(char *)"Assertion",(char *)"main",(char *)"x == 0",
- 3);
- /*@ assert x == 1; */
- __e_acsl_assert(x == 1,(char *)"Assertion",(char *)"main",(char *)"x == 1",
- 4);
+ __e_acsl_assert(x == 0,"Assertion","main","x == 0","first.i",3);
+ /*@ assert x == 0; */ ;
+ __e_acsl_assert(x == 1,"Assertion","main","x == 1","first.i",4);
+ /*@ assert x == 1; */ ;
__retres = 0;
return __retres;
}
diff --git a/src/plugins/e-acsl/doc/userman/examples/my_assert.c b/src/plugins/e-acsl/doc/userman/examples/my_assert.c
index c006779bc5b5b68796681f65c9055cf766483785..d6f42e6db325c3b424a3d7f3e3e6f81ada680633 100644
--- a/src/plugins/e-acsl/doc/userman/examples/my_assert.c
+++ b/src/plugins/e-acsl/doc/userman/examples/my_assert.c
@@ -2,14 +2,15 @@
extern int __e_acsl_sound_verdict;
-void __e_acsl_assert(int pred, char *kind,
- char *func_name, char *pred_text, int line) {
- printf("%s at line %d in function %s is %s (%s).\n\
+void __e_acsl_assert(int pred, const char *kind, const char *func_name,
+ const char *pred_text, const char *file, int line) {
+ printf("%s in file %s at line %d in function %s is %s (%s).\n\
The verified predicate was: `%s'.\n",
kind,
+ file,
line,
func_name,
pred ? "valid" : "invalid",
- __e_acsl_sound_verdict ? "trustable" : "UNTRUSTABLE",
+ __e_acsl_sound_verdict ? "trustworthy" : "UNTRUSTWORTHY",
pred_text);
}
diff --git a/src/plugins/e-acsl/doc/userman/frama-c-book.cls b/src/plugins/e-acsl/doc/userman/frama-c-book.cls
deleted file mode 100644
index 47463e1cc216eb43d7a224547eac4fef99aed78b..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/doc/userman/frama-c-book.cls
+++ /dev/null
@@ -1,332 +0,0 @@
-% --------------------------------------------------------------------------
-% --- LaTeX Class for Frama-C Books ---
-% --------------------------------------------------------------------------
-\NeedsTeXFormat{LaTeX2e}
-\ProvidesPackage{frama-c-book}[2009/02/05 LaTeX Class for Frama-C Books]
-% --------------------------------------------------------------------------
-% --- Base Class management ---
-% --------------------------------------------------------------------------
-\LoadClass[a4paper,11pt,twoside,openright]{report}
-\DeclareOption{web}{\PassOptionsToPackage{colorlinks,urlcolor=blue}{hyperref}}
-\DeclareOption{paper}{\PassOptionsToPackage{pdfborder=0 0 0}{hyperref}}
-\ProcessOptions
-\RequirePackage{fullpage}
-\RequirePackage{hevea}
-\RequirePackage{ifthen}
-\RequirePackage[T1]{fontenc}
-\RequirePackage[latin1]{inputenc}
-\RequirePackage[a4paper,pdftex,pdfstartview=FitH]{hyperref}
-\RequirePackage{amssymb}
-\RequirePackage{xcolor}
-\RequirePackage[pdftex]{graphicx}
-\RequirePackage{xspace}
-\RequirePackage{makeidx}
-\RequirePackage[leftbars]{changebar}
-\RequirePackage[english]{babel}
-\RequirePackage{fancyhdr}
-\RequirePackage{titlesec}
-% --------------------------------------------------------------------------
-% --- Page Layout ---
-% --------------------------------------------------------------------------
-\setlength{\voffset}{-6mm}
-\setlength{\headsep}{8mm}
-\setlength{\footskip}{21mm}
-\setlength{\textheight}{238mm}
-\setlength{\topmargin}{0mm}
-\setlength{\textwidth}{155mm}
-\setlength{\oddsidemargin}{2mm}
-\setlength{\evensidemargin}{-2mm}
-\setlength{\changebarsep}{0.5cm}
-\setlength{\headheight}{13.6pt}
-\def\put@bg(#1,#2,#3)#4{\setlength\unitlength{1cm}%
- \begin{picture}(0,0)(#1,#2)
- \put(0,0){\includegraphics[width=#3cm]{#4}}
- \end{picture}}
-\fancypagestyle{plain}{%
- \fancyfoot{}
- \fancyhead{}
- \fancyhead[LE]{\put@bg(2.4,27.425,21){frama-c-left.pdf}}
- \fancyhead[LO]{\put@bg(2.7,27.425,21){frama-c-right.pdf}}
- \fancyhead[CE]{\scriptsize\textsf{\leftmark}}
- \fancyhead[CO]{\scriptsize\textsf{\rightmark}}
- \fancyfoot[C]{\small\textsf{\thepage}}
- \renewcommand{\headrulewidth}{0pt}
- \renewcommand{\footrulewidth}{0pt}
-}
-\fancypagestyle{blank}{%
- \fancyfoot{}
- \fancyhead{}
- \fancyhead[LE]{\put@bg(2.4,27.425,21){frama-c-left.pdf}}
- \fancyhead[LO]{\put@bg(2.7,27.425,21){frama-c-right.pdf}}
-}
-%% Redefinition of cleardoublepage for empty page being blank
-\def\cleardoublepagewith#1{\clearpage\if@twoside \ifodd\c@page\else
-\hbox{}
-\thispagestyle{#1}
-\newpage
-\fi\fi}
-\def\cleardoublepage{\cleardoublepagewith{blank}}
-\pagestyle{plain}
-
-% --------------------------------------------------------------------------
-% --- Cover Page ---
-% --------------------------------------------------------------------------
-\newcommand{\coverpage}[1]{%
-\thispagestyle{empty}
-\setlength\unitlength{1cm}
-\begin{picture}(0,0)(3.27,26.75)
-\put(0.58,0.70){\includegraphics[width=20.9cm]{frama-c-cover.pdf}}
-\put(2.0,20.5){\makebox[8cm][l]{\fontfamily{phv}\fontseries{m}\fontsize{24}{2}\selectfont #1}}
-\end{picture}
-}
-
-% --------------------------------------------------------------------------
-% --- Title Page ---
-% --------------------------------------------------------------------------
-\renewenvironment{titlepage}%
-{\cleardoublepagewith{empty}\thispagestyle{empty}\begin{center}}%
-{\end{center}}
-\renewcommand{\title}[2]{
-\vspace{20mm}
-{\Huge\bfseries #1}
-
-\bigskip
-
-{\LARGE #2}
-\vspace{20mm}
-}
-\renewcommand{\author}[1]{
-\vspace{20mm}
-
-{#1}
-
-\medskip
-}
-% --------------------------------------------------------------------------
-% --- Sectionning ---
-% --------------------------------------------------------------------------
-\titleformat{\chapter}[display]{\Huge\raggedleft}%
-{\huge\chaptertitlename\,\thechapter}{0.5em}{}
-\titleformat{\section}[hang]{\Large\bfseries}{\thesection}{1em}{}%
-[\vspace{-14pt}\rule{\textwidth}{0.1pt}\vspace{-8pt}]
-\titleformat{\subsubsection}[hang]{\bfseries}{}{}{}%
-[\vspace{-8pt}]
-
-% --------------------------------------------------------------------------
-% --- Main Text Style ---
-% --------------------------------------------------------------------------
-%\raggedright
-\setlength\parindent{0pt}
-\setlength\parskip{1ex plus 0.3ex minus 0.2ex}
-\newenvironment{warning}[1][Warning:]{\small\paragraph{#1}\itshape}{\vspace{\parskip}}
-\def\FramaC{\textsf{Frama-C}\xspace}
-% --------------------------------------------------------------------------
-% --- Listings ---
-% --------------------------------------------------------------------------
-\RequirePackage{listings}
-
-\lstdefinelanguage{ACSL}{%
- morekeywords={allocates,assert,assigns,assumes,axiom,axiomatic,behavior,behaviors,
- boolean,breaks,complete,continues,data,decreases,disjoint,ensures,
- exit_behavior,frees,ghost,global,inductive,integer,invariant,lemma,logic,loop,
- model,predicate,reads,real,requires,returns,sizeof,strong,struct,terminates,type,
- union,variant},
- keywordsprefix={\\},
- alsoletter={\\},
- morecomment=[l]{//}
-}
-
-\lstloadlanguages{[ANSI]C,[Objective]Caml,csh,ACSL}
-\definecolor{lstbg}{gray}{0.98}
-\definecolor{lstfg}{gray}{0.10}
-\definecolor{lstrule}{gray}{0.6}
-\definecolor{lstnum}{gray}{0.4}
-\definecolor{lsttxt}{rgb}{0.3,0.2,0.6}
-\definecolor{lstmodule}{rgb}{0.3,0.6,0.2}%{0.6,0.6,0.2}
-\definecolor{lstspecial}{rgb}{0.2,0.6,0.0}
-\definecolor{lstfile}{gray}{0.85}
-\newcommand{\lstbrk}{\mbox{$\color{blue}\scriptstyle\cdots$}}
-\def\lp@basic{\ifmmode\normalfont\mathtt\mdseries\scriptsize\else\normalfont\ttfamily\mdseries\scriptsize\fi}
-\def\lp@inline{\ifmmode\normalfont\mathtt\scriptstyle\else\normalfont\ttfamily\mdseries\small\fi}
-\def\lp@keyword{}
-\def\lp@special{\color{lstfg}}
-\def\lp@comment{\normalfont\ttfamily\mdseries}
-\def\lp@string{\color{lstfg}} \def\lp@ident{}
-\def\lp@number{\rmfamily\tiny\color{lstnum}}
-\lstdefinestyle{frama-c-style}{%
- basicstyle=\lp@inline,%
- identifierstyle=\lp@ident,%
- commentstyle=\lp@comment,%
- keywordstyle={\ifmmode\mathsf\else\sffamily\fi},%
- keywordstyle=[2]\lp@special,%
- stringstyle=\lp@string,%
- emphstyle=\lp@ident\underbar,%
- showstringspaces=false,%
- mathescape=true,%
- numberstyle=\lp@number,%
- xleftmargin=6ex,xrightmargin=2ex,%
- framexleftmargin=1ex,%
- frame=l,%
- framerule=1pt,%
- rulecolor=\color{lstrule},%
- backgroundcolor=\color{lstbg},%
- moredelim={*[s]{/*@}{*/}},%
- moredelim={*[l]{//@}},%
- morecomment={[il]{//NOPP-LINE}},% invisible comment until end of line
- morecomment={[is]{//NOPP-BEGIN}{NOPP-END\^^M}},% no space after NOPP-END
- mathescape=true,
- escapechar=`
-% breaklines is broken when using a inline and background
-% breaklines,prebreak={\lstbrk},postbreak={\lstbrk},breakindent=5ex %
-}
-
-\lstdefinestyle{c}%
-{language={[ANSI]C},alsolanguage=ACSL,style=frama-c-style}
-\lstdefinestyle{c-basic}%
-{language={[ANSI]C},alsolanguage=ACSL,style=frama-c-style,basicstyle=\lp@basic}
-
-
-% --- C/ACSL Stuff ---------------------------------------------------------
-% Make 'c' the default style
-\lstset{style=c}
-
-\newcommand{\listinginput}[3][1]%
-{\lstinputlisting[style=c-basic,numbers=left,stepnumber=#1,firstnumber=#2]{#3}}
-
-\newcommand{\listinginputcaption}[4][1]%
-{\lstinputlisting[style=c-basic,numbers=left,stepnumber=#1,firstnumber=#2,title=#3]{#4}}
-
-\lstnewenvironment{listing}[2][1]%
-{\lstset{style=c-basic,numbers=left,stepnumber=#1,firstnumber=#2}}{}
-
-\lstnewenvironment{listing-nonumber}%
-{\lstset{style=c,numbers=none,basicstyle=\lp@basic}}{}
-
-% --- Verbatim Stuff -------------------------------------------------------
-\lstdefinelanguage{Shell}[]{csh}%
-{identifierstyle=\lp@basic,mathescape=false,backgroundcolor=,literate={\\\$}{\$}1}
-\lstnewenvironment{shell}[1][]{\lstset{language=Shell,basicstyle=\lp@basic,#1}}{}
-
-% ---- Stdout Stuff --------------------------------------------------------
-\lstdefinelanguage{Logs}[]{csh}%
-{identifierstyle=\lp@basic,backgroundcolor=}
-\lstnewenvironment{logs}[1][]{\lstset{language=Logs,basicstyle=\lp@basic,#1}}{}
-\newcommand{\logsinput}[1]%
-{\lstinputlisting[language=Logs,basicstyle=\lp@basic]{#1}}
-
-% --------------------------------------------------------------------------
-% --- Developer Code Stuff ---
-% --------------------------------------------------------------------------
-
-\newcommand{\listingname}[1]{\colorbox{lstfile}{\footnotesize\sffamily File \bfseries #1}\vspace{-4pt}}
-
-% --- Style ----------------------------------------------------------------
-\lstdefinestyle{framac-code-style}{%
-basicstyle=\lp@inline,%
-numberstyle=\lp@number,%
-keywordstyle=[1]\sffamily\color{lstmodule},%
-keywordstyle=[2]\sffamily\color{lstspecial},%
-keywordstyle=[3]\sffamily\bfseries,%
-identifierstyle=\rmfamily,%
-stringstyle=\ttfamily\color{lstfg},%
-commentstyle=\rmfamily\bfseries\color{lsttxt},%
-}
-\lstdefinestyle{framac-shell-style}{%
-mathescape=false,%
-basicstyle=\lp@basic,%
-numberstyle=\lp@number,%
-keywordstyle=\sffamily\bfseries,%
-keywordstyle=[1]\sffamily\color{lstmodule},%
-keywordstyle=[2]\sffamily\color{lstspecial},%
-keywordstyle=[3]\sffamily\bfseries,%
-identifierstyle=\ttfamily,%
-stringstyle=\ttfamily\color{lstfg},%
-commentstyle=\rmfamily\bfseries\color{lsttxt},%
-literate={\\\$}{\$}1,%
-}
-% --- Configure ------------------------------------------------------------
-\lstdefinelanguage{Configure}[]{csh}{%
-style=framac-shell-style,%
-morekeywords={fi},%
-}
-\lstnewenvironment{configurecode}[1][]%
-{\lstset{language=Configure,#1}}{}
-\newcommand{\configureinput}[1]{\lstinputlisting[language=Configure]{#1}}
-% --- Makefile ------------------------------------------------------------
-\lstdefinelanguage{Makefile}[]{make}{%
-style=framac-shell-style,%
-morekeywords={include},%
-}
-\lstnewenvironment{makefilecode}[1][]%
-{\lstset{language=Makefile,#1}}{}
-\newcommand{\makefileinput}[1]{\lstinputlisting[language=Makefile]{#1}}
-% --- C- for Developer ----------------------------------------------------
-\lstdefinestyle{framac-code}%
- {language={[ANSI]C},alsolanguage=ACSL,style=framac-code-style,basicstyle=\lp@basic}
-\lstnewenvironment{ccode}[1][]%
-{\lstset{language={[ANSI]C},alsolanguage=ACSL,style=framac-code-style,basicstyle=\lp@basic,#1}}{}
-\newcommand{\cinput}[1]%
-{\lstinputlisting[language={[ANSI]C},alsolanguage=ACSL,style=framac-code-style,basicstyle=\lp@basic]{#1}}
-\newcommand{\cinline}[1]%
-{\lstinline[style=framac-code]{#1}}
-% --- Ocaml ----------------------------------------------------------------
-\lstdefinelanguage{Ocaml}[Objective]{Caml}{%
-style=framac-code-style,%
-deletekeywords={when,module,struct,sig,begin,end},%
-morekeywords=[2]{failwith,raise,when},%
-morekeywords=[3]{module,struct,sig,begin,end},%
-literate=%
-{~}{${\scriptstyle\thicksim}$}1%
-{<}{$<$}1%
-{>}{$>$}1%
-{->}{$\rightarrow$}1%
-{<-}{$\leftarrow$}1%
-{:=}{$\leftarrow$}1%
-{<=}{$\leq$}1%
-{>=}{$\geq$}1%
-{==}{$\equiv$}1%
-{!=}{$\not\equiv$}1%
-{<>}{$\neq$}1%
-{'a}{$\alpha$}1%
-{'b}{$\beta$}1%
-{'c}{$\gamma$}1%
-{µ}{`{}}1%
-}
-
-\lstdefinestyle{ocaml-basic}%
-{language=Ocaml,basicstyle=\lp@basic}
-\newcommand{\ocamlinput}[2][]{\lstinputlisting[style=ocaml-basic,#1]{#2}}
-\lstnewenvironment{ocamlcode}[1][]{\lstset{style=ocaml-basic,#1}}{}
-% --------------------------------------------------------------------------
-\lstdefinelanguage{Why}{%
- morekeywords={
- type, logic, axiom, predicate, goal,
- forall, let, in,
- },
- morecomment=[s]{(*}{*)},
- alsoletter={_},
- literate=%
- {->}{$\Rightarrow$}1%
- {forall}{$\forall$}1%
- {not}{$\neg$}1%
- {<>}{$\neq$}1%
- {...}{$\dots$}1%
- %{_}{\_}1%
- %{_}{{\rule[0pt]{1ex}{.2pt}}}1%
- }
-
-\lstdefinestyle{why-style}{%
-language=Why,%
-style=framac-code-style,%
-basicstyle=\lp@inline,%
-}
-
-\lstnewenvironment{whycode}[1][]{\lstset{style=why-style,#1}}{}
-\newcommand{\whyinput}[1]%
-{\lstinputlisting[style=why-style,basicstyle=\lp@basic]{#1}}
-\newcommand{\whyinline}[1]%
-{\lstinline[style=why-style]{#1}}
-
-% --------------------------------------------------------------------------
-% --- End. ---
-% --------------------------------------------------------------------------
diff --git a/src/plugins/e-acsl/doc/userman/frama-c-cover.pdf b/src/plugins/e-acsl/doc/userman/frama-c-cover.pdf
deleted file mode 100644
index 4e14243c8064ca92d696fd354476dcdb31092895..0000000000000000000000000000000000000000
Binary files a/src/plugins/e-acsl/doc/userman/frama-c-cover.pdf and /dev/null differ
diff --git a/src/plugins/e-acsl/doc/userman/frama-c-left.pdf b/src/plugins/e-acsl/doc/userman/frama-c-left.pdf
deleted file mode 100644
index ddf8888d292539177ab81c1b33d6411edf51c820..0000000000000000000000000000000000000000
Binary files a/src/plugins/e-acsl/doc/userman/frama-c-left.pdf and /dev/null differ
diff --git a/src/plugins/e-acsl/doc/userman/frama-c-right.pdf b/src/plugins/e-acsl/doc/userman/frama-c-right.pdf
deleted file mode 100644
index db9b236dfdb19d9a6631ec55eee63f431f8d6f0d..0000000000000000000000000000000000000000
Binary files a/src/plugins/e-acsl/doc/userman/frama-c-right.pdf and /dev/null differ
diff --git a/src/plugins/e-acsl/doc/userman/introduction.tex b/src/plugins/e-acsl/doc/userman/introduction.tex
index 08956a9c61a38d24453af8840b7fb9f146a23c35..dd28d602b2827650750e45e4e4f9c4e35b196509 100644
--- a/src/plugins/e-acsl/doc/userman/introduction.tex
+++ b/src/plugins/e-acsl/doc/userman/introduction.tex
@@ -15,7 +15,7 @@ program.
checking''~\cite{runtime-assertion-checking}\footnote{In our context, ``runtime
annotation checking'' would be more precise.}. This is the primary goal of
\eacsl. Indirectly, in combination with the \rte plug-in~\cite{rte} of \framac,
-this
+this
usage allows the user to detect undefined behaviors in its \C code. Second, it
allows to combine \framac and its existing analyzers with other \C analyzers
that do not natively understand the \acsl specification language. Third, the
@@ -38,10 +38,12 @@ previous paragraph. Using \eacsl this way is therefore a fully automatic
process. Many usages, including automatic usages, are described in companion
research papers~\cite{rv13tutorial,rvcubes17tool,signoles18hdr}.
-This manual does \emph{not} explain how to install the \eacsl plug-in. For
-installation instructions please refer to the \texttt{INSTALL} file in the
-\eacsl distribution. \index{Installation} Furthermore, even though this manual
-provides examples, it is \emph{not} a full comprehensive tutorial on
+The \eacsl plug-in is installed with \framac, but this manual does \emph{not}
+explain how to install \framac. For installation instructions please refer to
+the \texttt{INSTALL}\footnote{
+ \url{https://git.frama-c.com/pub/frama-c/blob/master/INSTALL.md}}
+file in the \framac distribution. \index{Installation} Furthermore, even though
+this manual provides examples, it is \emph{not} a full comprehensive tutorial on
\framac or \eacsl.
% You can still refer to any external
% tutorial~\cite{rv13tutorial} for additional examples.
diff --git a/src/plugins/e-acsl/doc/userman/limitations.tex b/src/plugins/e-acsl/doc/userman/limitations.tex
index 45caa5d91dc753ea7b10f85f37b2c7ed3b01dae8..1a20cd3d97cc68c063e915f3819b1d27b1404a4c 100644
--- a/src/plugins/e-acsl/doc/userman/limitations.tex
+++ b/src/plugins/e-acsl/doc/userman/limitations.tex
@@ -5,12 +5,13 @@ reference manual~\cite{eacsl} is not yet fully supported. Which annotations can
already be translated into \C code and which cannot is defined in a separate
document~\cite{eacsl-implem}. Second, even though we do our best to avoid them,
bugs may exist. If you find a new one, please report it on the bug tracking
-system\footnote{\url{http://bts.frama-c.com}} (see Chapter 10 of the \framac
-User Manual~\cite{userman}). Third, there
-are some additional known limitations, which could be annoying for the user in
-some cases, but are tedious to lift. Please contact us if you are interested in
-lifting these limitations\footnote{Read \url{http://frama-c.com/support.html}
- for additional details.}.
+system\footnote{\url{https://git.frama-c.com/pub/frama-c/-/issues}} (see Chapter
+10 of the \framac User Manual~\cite{userman}). Third, there are some additional
+known limitations, which could be annoying for the user in some cases, but are
+tedious to lift. Please contact us if you are interested in lifting these
+limitations\footnote{Read
+ \url{https://git.frama-c.com/pub/frama-c/blob/master/CONTRIBUTING.md} for
+ additional details.}.
\section{Supported Systems}
@@ -53,8 +54,8 @@ may get no runtime error depending on your \C compiler, but the behavior is
actually undefined because the assertion reads the uninitialized variable
\lstinline|x|. You should be caught by the \eacsl plug-in, but that is not
the case yet.
-\begin{shell}
+\begin{shell}
\$ e-acsl-gcc.sh uninitialized.i -c -Omonitored_uninitialized
monitored_uninitialized.i: In function 'main':
monitored_uninitialized.i:44:16: warning: 'x' is used uninitialized in this function
@@ -98,22 +99,26 @@ Consider the following example.
You can generate the instrumented program as follows.
\begin{shell}
-\$ e-acsl-gcc.sh -ML -omonitored_valid_no_main.i valid_no_main.c
-<skip preprocessing commands>
+\$ e-acsl-gcc.sh -M -omonitored_valid_no_main.i valid_no_main.c
+[kernel] Parsing valid_no_main.c (with preprocessing)
[e-acsl] beginning translation.
-<skip warnings about annotations from the Frama-C libc
- which cannot be translated>
-[kernel] warning: no entry point specified:
- you must call function `__e_acsl_memory_init' by yourself.
+[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
+[kernel] Warning: no entry point specified:
+ you must call functions `__e_acsl_globals_init', `__e_acsl_globals_clean',
+ `__e_acsl_memory_init' and `__e_acsl_memory_clean' by yourself.
[e-acsl] translation done in project "e-acsl".
\end{shell}
The last warning states an important point: if this program is linked against
another file containing \texttt{main} function, then this main function must
-be modified to insert a call to the function \texttt{\_\_e\_acsl\_memory\_init}
+be modified to insert a calls to the functions
+\texttt{\_\_e\_acsl\_globals\_init}
+\index{e\_acsl\_globals\_init@\texttt{\_\_e\_acsl\_globals\_init}} and
+\texttt{\_\_e\_acsl\_memory\_init}
\index{e\_acsl\_memory\_init@\texttt{\_\_e\_acsl\_memory\_init}} at the very
-beginning. This function plays a very important role: it initializes metadata
-storage used for tracking of memory blocks. Unless this call is inserted the
+beginning. These functions play a very important role: the latter initializes
+metadata storage used for tracking of memory blocks while the former initializes
+tracking of global variables and constants. Unless these calls are inserted the
run of a modified program is likely to fail.
While it is possible to add such intrumentation manually we recommend using
@@ -125,7 +130,7 @@ While it is possible to add such intrumentation manually we recommend using
Then just compile and run it as explained in Section~\ref{sec:memory}.
\begin{shell}
-\$ e-acsl-gcc.sh -M -omonitored_modified_main.i modified_main.c
+\$ e-acsl-gcc.sh -M -omonitored_modified_main.i modified_main.c
\$ e-acsl-gcc.sh -C -Ovalid_no_main monitored_modified_main.i monitored_valid_no_main.i
\$ ./valid_no_main.e-acsl
Assertion failed at line 11 in function f.
@@ -192,7 +197,7 @@ functions.
\subsection{\eacsl Namespace}
While \eacsl uses source-to-source transformations and not binary
-instrumentations it is important that the source code provided at input does
+instrumentations it is important that the source code provided as input does
not contain any variables or functions prefixed \T{\_\_e\_acsl\_}. \eacsl
reserves this namespace for its transformations, and therefore an input program
containing such symbols beforehand may fail to be instrumented or compiled.
diff --git a/src/plugins/e-acsl/doc/userman/macros.tex b/src/plugins/e-acsl/doc/userman/macros.tex
index fd7bfa93e0321a07884ee12b0dc1c3b2853d3955..513101b9c92ffb8c0f8d08c3d0b9c41e1dd2c58f 100644
--- a/src/plugins/e-acsl/doc/userman/macros.tex
+++ b/src/plugins/e-acsl/doc/userman/macros.tex
@@ -1,5 +1,5 @@
-%%% Environnements dont le corps est suprimé, et
-%%% commandes dont la définition est vide,
+%%% Environnements dont le corps est suprimé, et
+%%% commandes dont la définition est vide,
%%% lorsque PrintRemarks=false
\usepackage{comment}
@@ -114,7 +114,7 @@ evolve in the future and/or not work as expected.}}
\ifthenelse{\isundefined{\myrq}}{}{\footnote{\myrq}}\end{changebar}}}%
{\excludecomment{notreviewedenv}}
-%%% Commandes et environnements pour la version relative à l'implementation
+%%% Commandes et environnements pour la version relative à l'implementation
\newcommand{\highlightnotimplemented}{%
\ifthenelse{\boolean{ColorImplementationRq}}{\color{red}}%
{\ul}%
diff --git a/src/plugins/e-acsl/doc/userman/main.tex b/src/plugins/e-acsl/doc/userman/main.tex
index f2f73c8229cab00bfd68472c81be15710c4f45ae..3e3ce0bed39c979dc76141f7ab804793b492fd88 100644
--- a/src/plugins/e-acsl/doc/userman/main.tex
+++ b/src/plugins/e-acsl/doc/userman/main.tex
@@ -20,7 +20,7 @@
\title{\eacsl Plug-in}{Release \eacslpluginversion
\ifthenelse{\equal{\eacslpluginversion}{\fcversion}}{}{%
\\[1em] compatible with \framac \fcversion}}
-\author{Julien Signoles and Kostyantyn Vorobyov}
+\author{Julien Signoles, Basile Desloges and Kostyantyn Vorobyov}
\begin{center}
CEA LIST\\ Software Reliability \& Security Laboratory
\end{center}
@@ -41,8 +41,8 @@ CEA LIST\\ Software Reliability \& Security Laboratory
\addcontentsline{toc}{chapter}{Foreword}
This is the user manual of the \framac plug-in
-\eacsl\footnote{\url{https://frama-c.com/eacsl.html}}. The contents of this
-document correspond to its version \eacslpluginversion compatible with
+\eacsl\footnote{\url{https://frama-c.com/fc-plugins/e-acsl.html}}. The contents
+of this document correspond to its version \eacslpluginversion compatible with
\fcversion version of \framac~\cite{userman,fac15}. The development of
the \eacsl plug-in is still ongoing. Features described by this document may
evolve in the future.
@@ -50,9 +50,8 @@ evolve in the future.
\section*{Acknowledgements}
We gratefully thank the people who contributed to this document:
-Basile Desloges, Pierre-Lo\"ic Garoche, Jens Gerlach, Florent Kirchner,
-Nikola\"i Kosmatov, Andr\'e Oliveira Maroneze, Fonenantsoa Maurica, and
-Guillaume Petiot.
+Pierre-Lo\"ic Garoche, Jens Gerlach, Florent Kirchner, Nikola\"i Kosmatov,
+Andr\'e Oliveira Maroneze, Fonenantsoa Maurica, and Guillaume Petiot.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/src/plugins/e-acsl/doc/userman/provides.tex b/src/plugins/e-acsl/doc/userman/provides.tex
index f9dedfdf86881ca09adbaa043b83b45d4bb5087a..f393932c92ffcd66ac781425ac4f6380ad53e955 100644
--- a/src/plugins/e-acsl/doc/userman/provides.tex
+++ b/src/plugins/e-acsl/doc/userman/provides.tex
@@ -44,13 +44,9 @@ Running \eacsl on \texttt{first.i} consists of adding \shortopt{e-acsl} option
to the \framac command line:
\begin{shell}
\$ frama-c -e-acsl first.i
-[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h (with preprocessing)
[kernel] Parsing first.i (no preprocessing)
[e-acsl] beginning translation.
-<skip a warning when translating the Frama-C libc>
+[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[e-acsl] translation done in project "e-acsl".
\end{shell}
@@ -58,8 +54,8 @@ Even though \texttt{first.i} has already been pre-processed, \eacsl first asks
the \framac kernel to process and combine it against several header files
provided by the \eacsl plug-in. Further \eacsl translates the annotated code
into a new \framac project named \texttt{e-acsl}\footnote{The notion of
-\emph{project} is explained in Section 8.1 of the \framac user
-manual~\cite{userman}.}. By default, the option \shortopt{e-acsl} does nothing
+ \emph{project} is explained in Section 8.1 of the \framac user
+ manual~\cite{userman}.}. By default, the option \shortopt{e-acsl} does nothing
more. It is however possible to have a look at the generated code in the
\framac GUI. This is also possible through the command line thanks to the
kernel options \shortopt{then-last} and \shortopt{print}. The former
@@ -72,15 +68,15 @@ As you can see, the generated code contains additional type declarations,
constant declarations and global \acsl annotations not present in the initial
file \texttt{first.i}. They are part of the \eacsl monitoring library. You can
safely ignore them for now. The translated \texttt{main} function of
-\texttt{first.i} is displayed at the end. After each \eacsl annotation,
+\texttt{first.i} is displayed at the end. Before each \eacsl annotation,
a call to \texttt{\_\_e\_acsl\_assert}\codeidx{e\_acsl\_assert} has been added.
\begin{minipage}{\linewidth}
\begin{ccode}
- /*@ assert x == 0; */
- __e_acsl_assert(x == 0,(char *)"Assertion",(char *)"main",(char *)"x == 0",3);
- /*@ assert x == 1; */
- __e_acsl_assert(x == 1,(char *)"Assertion",(char *)"main",(char *)"x == 1",4);
+ __e_acsl_assert(x == 0,"Assertion","main","x == 0","first.i",3);
+ /*@ assert x == 0; */ ;
+ __e_acsl_assert(x == 1,"Assertion","main","x == 1","first.i",4);
+ /*@ assert x == 1; */ ;
\end{ccode}
\end{minipage}
@@ -117,15 +113,15 @@ corresponding to your compiler and your system. For instance, in a 64-bit
machine you should also pass
\shortopt{machdep} \texttt{x86\_64} option as follows:
\begin{shell}
- \$ frama-c -machdep x86_64 -e-acsl first.i -then-last \
- -print -ocode monitored_first.c
+\$ frama-c -machdep x86_64 -e-acsl first.i -then-last \
+ -print -ocode monitored_first.c
\end{shell}
This file can be compile with a \C compiler (for instance \gcc), as follows:
\lstset{escapechar=£}
\begin{shell}
-\$ gcc -c -Wno-attributes monitored_first.c
+\$ gcc -c -Wno-attributes monitored_first.c
\end{shell}
However, creating an executable through a proper invokation to \gcc is painful
@@ -154,7 +150,7 @@ The default behaviour of \eacslgcc is to instrument an annotated C program
with runtime assertions via a run of \framac.
\begin{shell}
- \$ e-acsl-gcc.sh -omonitored_first.i first.i
+\$ e-acsl-gcc.sh -omonitored_first.i first.i
\end{shell}
The above command instruments \texttt{first.i} with runtime assertions and
@@ -167,7 +163,7 @@ Compilation and Linking of the original and the instrumented sources
is enabled using the \shortopt{c} option. For instance, command
\begin{shell}
- \$ e-acsl-gcc.sh -c -omonitored_first.i first.i
+\$ e-acsl-gcc.sh -c -omonitored_first.i first.i
\end{shell}
instruments the code in \texttt{first.i}, outputs it to
@@ -180,18 +176,19 @@ You can execute the generate binaries, in particular \texttt{a.out.e-acsl} which
detects at runtime the incorrect annotation.
\begin{shell}
\$ ./a.out.e-acsl
-Assertion failed at line 4 in function main.
-The failing predicate is:
-x == 1.
-Aborted
+first.i: In function 'main'
+first.i:4: Error: Assertion failed:
+ The failing predicate is:
+ x == 1.
+Aborted (core dumped)
\$ echo \$?
134
\end{shell}
The execution aborts with a non-zero exit code (134) and an error message
-indicating \eacsl annotation that has been violated. There is no output for the
-valid \eacsl annotation. That is, the run of an executable generated from the
-instrumented source file (i.e., \texttt{monitored\_first.i}) detects that the
-second annotation in the initial program is invalid, whereas the first
+indicating an \eacsl annotation that has been violated. There is no output for
+the valid \eacsl annotation. That is, the run of an executable generated from
+the instrumented source file (i.e., \texttt{monitored\_first.i}) detects that
+the second annotation in the initial program is invalid, whereas the first
annotation holds for this execution.
Named executables can be created using the \shortopt{O} option. This is such
@@ -201,7 +198,7 @@ generated from the original program and the executable generated from the
For example, command
\begin{shell}
- \$ e-acsl-gcc.sh -c -omonitored_first.i -Omonitored_first first.i
+\$ e-acsl-gcc.sh -c -omonitored_first.i -Omonitored_first first.i
\end{shell}
names the executables generated from \texttt{first.i} and
\texttt{monitored\_first.i}: \texttt{monitored\_first} and
@@ -213,7 +210,7 @@ plug-in. This option is useful if one makes changes to an already
instrumented source file by hand and only wants to recompile it.
\begin{shell}
- \$ e-acsl-gcc.sh -C -Omonitored_first monitored_first.i
+\$ e-acsl-gcc.sh -C -Omonitored_first monitored_first.i
\end{shell}
The above command generates a single executable named
@@ -230,16 +227,16 @@ also be passed using \shortopt{I} and \shortopt{G} options
respectively, for instance as follows:
\begin{shell}
- \$ e-acsl-gcc.sh -I/usr/local/bin/frama-c -G/usr/bin/gcc6 foo.c
+\$ e-acsl-gcc.sh -I/usr/local/bin/frama-c -G/usr/bin/gcc6 foo.c
\end{shell}
Runs of \framac and \gcc issued by \eacslgcc can further be customized by using
additional flags. \framac flags can be passed using the \shortopt{F} option,
-while \shortopt{l} and \shortopt{e} options allow for passing additional
+while \shortopt{e} and \shortopt{l} options allow for passing additional
pre-processor and linker flags during \gcc invocations. For example, command
\begin{shell}
- \$ e-acsl-gcc.sh -c -F"-unicode" -e"-I/bar -I/baz" foo.c
+\$ e-acsl-gcc.sh -c -F"-unicode" -e"-I/bar -I/baz" foo.c
\end{shell}
yields an instrumented program \texttt{a.out.frama.c} where ACSL formulas
@@ -264,7 +261,7 @@ the \framac kernel while instrumenting \texttt{foo.c} one can use the following
command:
\begin{shell}
- \$ e-acsl-gcc.sh -v5 -F"-kernel-verbose 0" foo.c
+\$ e-acsl-gcc.sh -v5 -F"-kernel-verbose 0" foo.c
\end{shell}
Verbosity of the \eacslgcc output can also be reduced using the \shortopt{q}
@@ -277,7 +274,7 @@ output during instrumentation and compilation of \texttt{foo.c} to the
file named \texttt{/tmp/log}.
\begin{shell}
- \$ e-acsl-gcc.sh -c -s/tmp/log foo.c
+\$ e-acsl-gcc.sh -c -s/tmp/log foo.c
\end{shell}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -304,6 +301,7 @@ One of the benefits of using the wrapper script is that it makes sure that
further passed \shortopt{m64} or \shortopt{m32} options to generate code using
64-bit or 32-bit ABI respectively.
+
At the present stage of implementation \eacsl does not support generating
executables with ABI different to the default one.
@@ -313,13 +311,13 @@ executables with ABI different to the default one.
For full up-to-date documentation of \eacslgcc see its man page:
\begin{shell}
- \$ man e-acsl-gcc.sh
+\$ man e-acsl-gcc.sh
\end{shell}
Alternatively, you can also use the \shortopt{h} option of \eacslgcc:
\begin{shell}
- \$ man e-acsl-gcc.sh -h
+\$ e-acsl-gcc.sh -h
\end{shell}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -347,8 +345,8 @@ is undefined if $e$ leads to a runtime error and, consequently, the semantics of
any term $t$ (resp. predicate $p$) containing such a construct $c$ is
undefined as soon as $e$ has to be evaluated in order to evaluate $t$
(resp. $p$). The \eacsl Reference Manual also states that \emph{``it is the
-responsibility of each tool which interprets \eacsl to ensure that an
-undefined term is never evaluated''}~\cite{eacsl}.
+ responsibility of each tool which interprets \eacsl to ensure that an
+ undefined term is never evaluated''}~\cite{eacsl}.
Accordingly, the \eacsl plug-in prevents an undefined term from being
evaluated. If an annotation contains such a term, \eacsl will report a proper
@@ -390,20 +388,20 @@ line.
It might be particularly useful in one of the following contexts:
\begin{itemize}
-\item several libc functions used by the analyzed program are still not defined
- in the \framac libc; or
-\item your system libc and the \framac libc mismatch about several function
- types (for instance, your system libc is not 100\% POSIX compliant); or
-\item several \framac lib functions get a contract and you are not interested in
- verifying them (for instance, only checking undefine behaviors matters).
+ \item several libc functions used by the analyzed program are still not defined
+ in the \framac libc; or
+ \item your system libc and the \framac libc mismatch about several function
+ types (for instance, your system libc is not 100\% POSIX compliant); or
+ \item several \framac lib functions get a contract and you are not interested in
+ verifying them (for instance, only checking undefine behaviors matters).
\end{itemize}
\begin{important}
-Notably, \eacslgcc disables \framac libc by default. This is because most of
-its functions are annotated with \eacsl contracts and generating code for
-these contracts results in additional runtime overheads. To enforce default
-\framac contracts with \eacslgcc you can pass \shortopt{L} option to the wrapper
-script.
+ Notably, \eacslgcc disables \framac libc by default. This is because most of
+ its functions are annotated with \eacsl contracts and generating code for
+ these contracts results in additional runtime overheads. To enforce default
+ \framac contracts with \eacslgcc you can pass \shortopt{L} option to the wrapper
+ script.
\end{important}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -464,10 +462,11 @@ reports the violation of the second annotation:
\begin{shell}
\$ e-acsl-gcc.sh -c -Ovalid valid.c
\$ ./valid.e-acsl
-Assertion failed at line 11 in function main.
-The failing predicate is:
-freed: \valid(x).
-Aborted
+valid.c: In function 'main'
+valid.c:11: Error: Assertion failed:
+ The failing predicate is:
+ freed: \valid(x).
+Aborted (core dumped)
\end{shell}
To check memory-related predicates (such as \lstinline|\valid|) \eacsl tracks
@@ -494,11 +493,10 @@ location \T{x} as belonging unallocated memory space.
Memory tracking implemented by the \eacsl library comes in two flavours dubbed
\I{bittree-based} and \I{segment-based} memory models. With the bittree-based
model meta-storage is implemented as a compact prefix trie called Patricia
-trie~\cite{rv13}, whereas segment-based memory model
-\footnote{Segment-based model of \eacsl has not yet appeared in the literature.}
-is based on shadow memory~\cite{pldi16}. The functionality of the provided
-memory models is equivalent, however they differ in performance. We further
-discuss performance considerations.
+trie~\cite{rv13}, whereas segment-based memory model is based on shadow
+memory~\cite{vorobyov17ismm}. The functionality of the provided memory models is
+equivalent, however they differ in performance. We further discuss performance
+considerations.
The \eacsl models allocate heap memory using a customized version of the
\dlmalloc\footnote{\url{http://dlmalloc.net/}} memory allocator replacing
@@ -537,7 +535,7 @@ performance. The bittree-based model uses compact memory representation of
metadata. The segment-based model on the other hand uses significantly more
memory. You can expect over 2x times memory overheads when using it. However It
is often an order of magnitude faster than the bittree-based
-model~\cite{pldi16}.
+model~\cite{vorobyov17ismm}.
%[Need ref here with comparison of the performance. Ideally a reference to the PLDI paper].
@@ -553,9 +551,9 @@ feature can be enabled using the \shortopt{M} switch of \eacslgcc or
\shortopt{e-acsl-full-mtracking} option of the \eacsl plug-in.
\begin{important}
-The above-mentioned static analysis is probably the less robust part of \eacsl
-for the time being. When handling a large piece of code, it might be necessary
-to deactivate it and systematically instrument the code as explained above.
+ The above-mentioned static analysis is probably the less robust part of \eacsl
+ for the time being. When handling a large piece of code, it might be necessary
+ to deactivate it and systematically instrument the code as explained above.
\end{important}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -636,7 +634,7 @@ that uses \texttt{exit(CODE)} instead of \texttt{abort}.
For instance, the program generated using the following command
exits with code \texttt{5} on a predicate violation.
\begin{shell}
- \$ e-acsl-gcc.sh -c --fail-with-code=5 foo.c
+\$ e-acsl-gcc.sh -c --fail-with-code=5 foo.c
\end{shell}
Forceful termination of a monitored program can be disabled using
@@ -657,7 +655,7 @@ following signature:
Additionally, it may depends on the global variable
\texttt{\_\_e\_acsl\_sound\_verdict}\codeidxdef{e\_acsl\_sound\_verdict}. This
variable of type \texttt{int} is set to \texttt{0} as soon as the verdict
-provided by \eacsl is not trustable anymore (see
+provided by \eacsl is not trustworthy anymore (see
Section~\ref{sec:partial-instrumentation}).
Below is an example which prints the validity status of each property but never
@@ -675,9 +673,9 @@ with the customized one specified in \texttt{my\_assert.c}
\begin{shell}
\$ e-acsl-gcc.sh -c -X first.i -Ofirst --external-assert=my_assert.c
\$ ./first.e-acsl
-Assertion at line 3 in function main is valid (trustable).
+Assertion in file first.i at line 3 in function main is valid (trustworthy).
The verified predicate was: `x == 0'.
-Assertion at line 4 in function main is invalid (trustable).
+Assertion in file first.i at line 4 in function main is invalid (trustworthy).
The verified predicate was: `x == 1'.
\end{shell}
@@ -716,16 +714,16 @@ Abort
Whenever option \longopt{libc-replacements} of \eacslgcc is set, \eacsl is
able to detect incorrect usage of the following libc functions:
\begin{itemize}
-\item \texttt{memcmp}
-\item \texttt{memcpy}
-\item \texttt{memmove}
-\item \texttt{memset}
-\item \texttt{strcat}
-\item \texttt{strncat}
-\item \texttt{strcmp}
-\item \texttt{strcpy}
-\item \texttt{strncpy}
-\item \texttt{strlen}
+ \item \texttt{memcmp}
+ \item \texttt{memcpy}
+ \item \texttt{memmove}
+ \item \texttt{memset}
+ \item \texttt{strcat}
+ \item \texttt{strncat}
+ \item \texttt{strcmp}
+ \item \texttt{strcpy}
+ \item \texttt{strncpy}
+ \item \texttt{strlen}
\end{itemize}
For instance, the program below incorrectly uses \texttt{strcpy} because the
@@ -774,12 +772,13 @@ The instrumented code is generated as usual, even though you get an additional
warning.
\begin{shell}
\$ e-acsl-gcc.sh no_main.i -omonitored_no_main.i
-<skip preprocessing command line>
+[kernel] Parsing no_main.i (no preprocessing)
[e-acsl] beginning translation.
-[e-acsl] warning: cannot find entry point `main'.
- Please use option `-main' for specifying a valid entry point.
- The generated program may miss memory instrumentation.
- if there are memory-related annotations.
+[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
+[e-acsl] Warning: cannot find entry point `main'.
+ Please use option `-main' for specifying a valid entry point.
+ The generated program may miss memory instrumentation
+ if there are memory-related annotations.
[e-acsl] translation done in project "e-acsl".
\end{shell}
@@ -817,12 +816,12 @@ The instrumented code is generated as usual, even though you get an additional
warning.
\begin{shell}
\$ e-acsl-gcc.sh -omonitored_no_code.i no_code.c
+[kernel] Parsing no_code.c (with preprocessing)
[e-acsl] beginning translation.
-[e-acsl] warning: annotating undefined function `my_pow':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-no_code.c:9:[kernel] warning: No code nor implicit assigns clause for function my_pow,
-generating default assigns from the prototype
+[e-acsl] Warning: annotating undefined function `my_pow':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[e-acsl] translation done in project "e-acsl".
\end{shell}
@@ -840,10 +839,11 @@ executable by providing definition of \T{my\_pow}.
\begin{shell}
\$ e-acsl-gcc.sh -C -Ono_code pow.i monitored_no_code.i
\$ ./no_code.e-acsl
-Postcondition failed at line 5 in function my_pow.
-The failing predicate is:
-\old(n % 2 == 0) ==> \result >= 1.
-Aborted
+no_code.c: In function 'my_pow'
+no_code.c:5: Error: Postcondition failed:
+ The failing predicate is:
+ even: \result >= 1.
+Aborted (core dumped)
\end{shell}
The execution of the corresponding binary fails at runtime: actually, our
@@ -896,21 +896,23 @@ One can ask to not instrument function \texttt{g} (\emph{i.e.} to instrument
only functions \texttt{f} and \texttt{main}) through the following command.
\begin{shell}
\$ e-acsl-gcc.sh \
- -c --oexec-e-acsl partial.out \
- --e-acsl-extra="-e-acsl-instrument=+@all,-g"' \
- partial.i
+ -c --oexec-e-acsl partial.out \
+ --e-acsl-extra="-e-acsl-instrument=+@all,-g" \
+ partial.i
\end{shell}
Therefore, running the generated executable \texttt{partial.out} leads to the
following verdicts.
\begin{shell}
\$ ./partial.out
-warning: no sound verdict (guess: ok) at line 16 (function main).
-The considered predicate is:
-\initialized(&t[1]).
-warning: no sound verdict (guess: FAIL) at line 17 (function main).
-The considered predicate is:
-\initialized(&t[2]).
+partial.i: In function 'main'
+partial.i:16: Warning: no sound verdict for Assertion (guess: ok).
+ the considered predicate is:
+ \initialized(&t[1])
+partial.i: In function 'main'
+partial.i:17: Warning: no sound verdict for Assertion (guess: FAIL).
+ the considered predicate is:
+ \initialized(&t[2])
\end{shell}
First, there is no message for the first assertion about the initialization of
@@ -919,7 +921,7 @@ First, there is no message for the first assertion about the initialization of
the complete instrumentation of functions \texttt{f} and \texttt{main}.
Second, since function \texttt{g} was not instrumented, no sound verdict may be
-provided after executing it. It leads to the printed warnings for the two last
+provided after executing it. It leads to the printed warnings for the last two
assertions. The indicated guesses (\texttt{ok} for the first assertion and
\texttt{FAIL} for the second one) are the verdicts computed by \eacsl. They can
be trusted if and only if the \eacsl instrumentation is not necessary for
@@ -957,15 +959,15 @@ are potential overflows in this case), just do:
\begin{shell}
\$ frama-c -rte combine.i -then -e-acsl -then-last -print
- -ocode monitored_combine.i
-\$ e-acsl-gcc.sh -C -Ocombine monitored_combine.i
-\$ ./combine.
+ -ocode monitored_combine.c
+\$ e-acsl-gcc.sh -C -Ocombine monitored_combine.c
+\$ ./combine.e-acsl
\end{shell}
Automatic assertion generation can also be enabled via \eacslgcc directly via
the following command:
\begin{shell}
-\$ e-acsl-gcc.sh -c -Ocombine -omonitored_combine.i --rte=all
+\$ e-acsl-gcc.sh -c -Ocombine -omonitored_combine.i --rte=all combine.i
\end{shell}
Note the use of \eacslgcc \longopt{rte} option which asks \framac to combine
@@ -987,13 +989,13 @@ prove that there is no potential overflow in the previous program, so the \eacsl
plug-in does not generate additional code for checking them if you run the
following command.
\begin{shell}
-\$ frama-c -rte combine.i -then -val -then -e-acsl \
- -then-last -print -ocode monitored_combine.i
+\$ frama-c -rte combine.i -then -eva -then -e-acsl \
+ -then-last -print -ocode monitored_combine.i
\end{shell}
The additional code will be generated with the two following command.
\begin{shell}
-\$ frama-c -rte combine.i -then -val -then -e-acsl \
- -e-acsl-valid -then-last -print -ocode monitored_combine.i
+\$ frama-c -rte combine.i -then -eva -then -e-acsl \
+ -e-acsl-valid -then-last -print -ocode monitored_combine.i
\end{shell}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -1014,10 +1016,9 @@ you can pass it using \shortopt{F} switch:
\begin{shell}
\$ e-acsl-gcc.sh -F"-e-acsl-project foobar" check.i
-<skip preprocessing commands>
+[kernel] Parsing check.i (no preprocessing)
[e-acsl] beginning translation.
-check.i:4:[e-acsl] warning: E-ACSL construct `right shift' is not yet supported.
- Ignoring annotation.
+[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[e-acsl] translation done in project "foobar".
\end{shell}
@@ -1047,21 +1048,21 @@ which information is displayed according to the verbosing level. The level $n$
also displays the information of all the lower levels.
\begin{center}
-\begin{tabular}{|l|l|}
-\hline
-\shortopt{e-acsl-verbose 0}& only warnings and errors\\
-\hline
-\shortopt{e-acsl-verbose 1}& beginning and ending of the translation\\
-\hline
-\shortopt{e-acsl-verbose 2}& different parts of the translation and
- functions-related information\\
-\hline
-\shortopt{e-acsl-verbose 3}& predicates- and statements-related information\\
-\hline
-\shortopt{e-acsl-verbose 4}& terms- and expressions-related information
-\\
-\hline
-\end{tabular}
+ \begin{tabular}{|l|l|}
+ \hline
+ \shortopt{e-acsl-verbose 0} & only warnings and errors \\
+ \hline
+ \shortopt{e-acsl-verbose 1} & beginning and ending of the translation \\
+ \hline
+ \shortopt{e-acsl-verbose 2} & different parts of the translation and
+ functions-related information \\
+ \hline
+ \shortopt{e-acsl-verbose 3} & predicates- and statements-related information \\
+ \hline
+ \shortopt{e-acsl-verbose 4} & terms- and expressions-related information
+ \\
+ \hline
+ \end{tabular}
\end{center}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -1074,19 +1075,19 @@ The kind of information to display is settable by the option
parts of the translation, as detailed below.
\begin{center}
-\begin{tabular}{|l|l|}
-\hline
-analysis & minimization of the instrumentation for memory-related annotation
-(section~\ref{sec:memory}) \\
-\hline
-duplication & duplication of functions with contracts
-(section~\ref{sec:no-code}) \\
-\hline
-translation & translation of an annotation into \C code\\
-\hline
-typing & minimization of the instrumentation for integers
-(section~\ref{sec:integers}) \\
-\hline
-\end{tabular}
+ \begin{tabular}{|l|l|}
+ \hline
+ analysis & minimization of the instrumentation for memory-related annotation
+ (section~\ref{sec:memory}) \\
+ \hline
+ preparation & duplication of functions with contracts
+ (section~\ref{sec:no-code}) \\
+ \hline
+ translation & translation of an annotation into \C code \\
+ \hline
+ typing & minimization of the instrumentation for integers
+ (section~\ref{sec:integers}) \\
+ \hline
+ \end{tabular}
\end{center}
% >>>
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c
index 083d015a3016899debff7f46273890665e035425..852f1447084e3b2569b4c28eb681abfe3f7bb06b 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c
@@ -744,19 +744,76 @@ void* realloc(void *ptr, size_t size) {
* shadow block to the size of the new allocation */
if (old_size > size) {
clearbits_right(
- old_alloc_size - size,
- old_init_shadow + old_alloc_size/8);
+ old_alloc_size - size, // size in bits
+ old_init_shadow + old_alloc_size/8); // end of the old init shadow
}
- /* Now init shadow can be moved (if needed), keep in mind that
- * segment base addresses are aligned at a boundary of something
- * divisible by 8, so instead of moving actual bits here the
- * segments are moved to avoid dealing with bit-level operations
- * on incomplete bytes. */
+ /* Keep in mind that there is a ratio of 8 between the actual heap
+ * memory and the init shadow memory. So a byte in the actual memory
+ * corresponds to a bit in the shadow memory.
+ */
+
+ /* We need to keep the status of the init shadow up to `old_size` bits
+ * (or `size` if `size < old_size`), and we need to make sure that the
+ * bits of the init shadow correspondings to the bytes between
+ * `old_size` and `size` are set to zero if `size > old_size`. */
+
+ /* First of all, determine the number of bits in the init shadow that
+ * must be kept */
+ size_t keep_bits = (size < old_size) ? size : old_size;
+
+ /* To avoid doing too much bitwise operations, separate this size in
+ * the amount of bytes of init shadow that must be kept including any
+ * incomplete byte, and the number of bits that must be kept in the last
+ * byte if it is incomplete */
+ size_t rem_keep_bits = keep_bits%8;
+ size_t keep_bytes = keep_bits/8 + (rem_keep_bits > 0 ? 1 : 0);
+
+ /* If the pointer has been moved, then we need to copy `keep_bytes`
+ * from the old shadow to the new shadow to carry over all the needed
+ * information. Then the old init shadow can be reset. */
if (res != ptr) {
- size_t copy_size = (old_size > size) ? alloc_size : old_alloc_size;
- memcpy(new_init_shadow, old_init_shadow, copy_size);
- memset(old_init_shadow, 0, copy_size);
+ DVASSERT(keep_bytes <= alloc_size/8 && keep_bytes < old_alloc_size/8,
+ "Attempt to access out of bound init shadow. Accessing %lu bytes, \
+ old init shadow size: %lu bytes, new init shadow size: %lu bytes.",
+ keep_bytes, old_alloc_size/8, alloc_size/8);
+ memcpy(new_init_shadow, old_init_shadow, keep_bytes);
+ memset(old_init_shadow, 0, old_alloc_size/8);
+ }
+
+ if (size > old_size) {
+ // Last kept byte index
+ size_t idx = keep_bytes - 1; // idx < init_shadow_size by construction
+
+ /* If the new size is greater than the old size and the last kept byte
+ * is incomplete (`rem_keep_bits > 0`), then reset the unkept bits of
+ * the last byte in the new init shadow */
+ if (rem_keep_bits > 0) {
+ DVASSERT(idx < alloc_size/8,
+ "Attempt to access out of bound init shadow. Accessing index %lu \
+ with init shadow of size %lu bytes.", idx, alloc_size/8);
+ unsigned char mask = 0;
+ setbits64(rem_keep_bits, mask);
+ *(new_init_shadow + idx) &= mask;
+ }
+
+ /* Finally, if the new size is greater than the old size and the
+ * pointer hasn't been moved, then we need to make sure that the
+ * remaining bits of the init shadow corresponding to the memory
+ * between `old_size` and `size` are set to zero. */
+ if (res == ptr) {
+ // Index of the byte after the last kept byte
+ ++idx;
+ // Number of bytes between the index and the end of the init
+ // shadow corresponding to the new allocated memory
+ size_t count = size/8 - idx;
+
+ DVASSERT((idx+count) <= alloc_size/8,
+ "Attempt to access out of bound init shadow. Accessing %lu bytes \
+ from index %lu with init shadow of size %lu bytes.",
+ count, idx, alloc_size/8);
+ memset(new_init_shadow+idx, 0, count);
+ }
}
}
} else {
@@ -895,7 +952,7 @@ int heap_initialized(uintptr_t addr, long len) {
unsigned char mask = 0;
setbits64_skip(set,mask,skip);
- if (*shadow != mask)
+ if ((*shadow & mask) != mask)
return 0;
}
if (len > 0)
diff --git a/src/plugins/e-acsl/tests/memory/initialized.c b/src/plugins/e-acsl/tests/memory/initialized.c
index 4af4918caa2b7445e02f84fe3e115ef369e3f150..34f53edb19e059c2a8ff498d9e54d9c052536f36 100644
--- a/src/plugins/e-acsl/tests/memory/initialized.c
+++ b/src/plugins/e-acsl/tests/memory/initialized.c
@@ -84,6 +84,52 @@ int main(void) {
/*@assert ! \initialized(p); */
/*@assert ! \initialized(q); */
+ /* Specially crafted calloc and realloc calls to check corner cases of
+ * initialization */
+ q = calloc(3, sizeof(int));
+ /*@ assert \initialized(&q[0..2]); */
+ q = realloc(q, 6 * sizeof(int));
+ /*@ assert \initialized(&q[0..2]); */
+ /*@ assert ! \initialized(&q[3]); */
+ /*@ assert ! \initialized(&q[4]); */
+ /*@ assert ! \initialized(&q[5]); */
+ free(q);
+ q = calloc(7, sizeof(int));
+ /*@ assert \initialized(&q[0..6]); */
+ q = realloc(q, 8 * sizeof(int));
+ /*@ assert \initialized(&q[0..6]); */
+ /*@ assert ! \initialized(&q[7]); */
+ q = realloc(q, 10 * sizeof(int));
+ /*@ assert \initialized(&q[0..6]); */
+ /*@ assert ! \initialized(&q[7]); */
+ /*@ assert ! \initialized(&q[8]); */
+ /*@ assert ! \initialized(&q[9]); */
+ free(q);
+ q = calloc(2, sizeof(int));
+ /*@ assert \initialized(&q[0..1]); */
+ q = realloc(q, 4 * sizeof(int));
+ /*@ assert \initialized(&q[0..1]); */
+ /*@ assert ! \initialized(&q[2]); */
+ /*@ assert ! \initialized(&q[3]); */
+ free(q);
+ q = calloc(6, sizeof(int));
+ /*@ assert \initialized(&q[0..5]); */
+ q = realloc(q, 3 * sizeof(int));
+ /*@ assert \initialized(&q[0..2]); */
+ free(q);
+ q = malloc(6 * sizeof(int));
+ /*@ assert ! \initialized(&q[0]); */
+ /*@ assert ! \initialized(&q[1]); */
+ /*@ assert ! \initialized(&q[2]); */
+ /*@ assert ! \initialized(&q[3]); */
+ /*@ assert ! \initialized(&q[4]); */
+ /*@ assert ! \initialized(&q[5]); */
+ q = realloc(q, 3 * sizeof(int));
+ /*@ assert ! \initialized(&q[0]); */
+ /*@ assert ! \initialized(&q[1]); */
+ /*@ assert ! \initialized(&q[2]); */
+ free(q);
+
/* Spoofing access to a non-existing stack address */
q = (int*)(&q - 1024*5);
/*assert ! \initialized(q); */
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c
index 2fc7f4ff02452f9cf5ec262dc1a11a7dff556df0..dec94db6533f1ddb8db1ab53e6913dab01393817 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c
@@ -319,23 +319,329 @@ int main(void)
}
/*@ assert ¬\initialized(q); */ ;
__e_acsl_full_init((void *)(& q));
+ q = (int *)calloc((unsigned long)3,sizeof(int));
+ {
+ int __gen_e_acsl_size;
+ int __gen_e_acsl_if;
+ int __gen_e_acsl_initialized_32;
+ __gen_e_acsl_size = 4 * ((2 - 0) + 1);
+ if (__gen_e_acsl_size <= 0) __gen_e_acsl_if = 0;
+ else __gen_e_acsl_if = __gen_e_acsl_size;
+ __gen_e_acsl_initialized_32 = __e_acsl_initialized((void *)((char *)q +
+ 4 * 0),
+ (size_t)__gen_e_acsl_if);
+ __e_acsl_assert(__gen_e_acsl_initialized_32,"Assertion","main",
+ "\\initialized(q + (0 .. 2))",
+ "tests/memory/initialized.c",90);
+ }
+ /*@ assert \initialized(q + (0 .. 2)); */ ;
+ __e_acsl_full_init((void *)(& q));
+ q = (int *)realloc((void *)q,(unsigned long)6 * sizeof(int));
+ {
+ int __gen_e_acsl_size_2;
+ int __gen_e_acsl_if_2;
+ int __gen_e_acsl_initialized_33;
+ __gen_e_acsl_size_2 = 4 * ((2 - 0) + 1);
+ if (__gen_e_acsl_size_2 <= 0) __gen_e_acsl_if_2 = 0;
+ else __gen_e_acsl_if_2 = __gen_e_acsl_size_2;
+ __gen_e_acsl_initialized_33 = __e_acsl_initialized((void *)((char *)q +
+ 4 * 0),
+ (size_t)__gen_e_acsl_if_2);
+ __e_acsl_assert(__gen_e_acsl_initialized_33,"Assertion","main",
+ "\\initialized(q + (0 .. 2))",
+ "tests/memory/initialized.c",92);
+ }
+ /*@ assert \initialized(q + (0 .. 2)); */ ;
+ {
+ int __gen_e_acsl_initialized_34;
+ __gen_e_acsl_initialized_34 = __e_acsl_initialized((void *)(q + 3),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_34,"Assertion","main",
+ "!\\initialized(q + 3)","tests/memory/initialized.c",93);
+ }
+ /*@ assert ¬\initialized(q + 3); */ ;
+ {
+ int __gen_e_acsl_initialized_35;
+ __gen_e_acsl_initialized_35 = __e_acsl_initialized((void *)(q + 4),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_35,"Assertion","main",
+ "!\\initialized(q + 4)","tests/memory/initialized.c",94);
+ }
+ /*@ assert ¬\initialized(q + 4); */ ;
+ {
+ int __gen_e_acsl_initialized_36;
+ __gen_e_acsl_initialized_36 = __e_acsl_initialized((void *)(q + 5),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_36,"Assertion","main",
+ "!\\initialized(q + 5)","tests/memory/initialized.c",95);
+ }
+ /*@ assert ¬\initialized(q + 5); */ ;
+ free((void *)q);
+ __e_acsl_full_init((void *)(& q));
+ q = (int *)calloc((unsigned long)7,sizeof(int));
+ {
+ int __gen_e_acsl_size_3;
+ int __gen_e_acsl_if_3;
+ int __gen_e_acsl_initialized_37;
+ __gen_e_acsl_size_3 = 4 * ((6 - 0) + 1);
+ if (__gen_e_acsl_size_3 <= 0) __gen_e_acsl_if_3 = 0;
+ else __gen_e_acsl_if_3 = __gen_e_acsl_size_3;
+ __gen_e_acsl_initialized_37 = __e_acsl_initialized((void *)((char *)q +
+ 4 * 0),
+ (size_t)__gen_e_acsl_if_3);
+ __e_acsl_assert(__gen_e_acsl_initialized_37,"Assertion","main",
+ "\\initialized(q + (0 .. 6))",
+ "tests/memory/initialized.c",98);
+ }
+ /*@ assert \initialized(q + (0 .. 6)); */ ;
+ __e_acsl_full_init((void *)(& q));
+ q = (int *)realloc((void *)q,(unsigned long)8 * sizeof(int));
+ {
+ int __gen_e_acsl_size_4;
+ int __gen_e_acsl_if_4;
+ int __gen_e_acsl_initialized_38;
+ __gen_e_acsl_size_4 = 4 * ((6 - 0) + 1);
+ if (__gen_e_acsl_size_4 <= 0) __gen_e_acsl_if_4 = 0;
+ else __gen_e_acsl_if_4 = __gen_e_acsl_size_4;
+ __gen_e_acsl_initialized_38 = __e_acsl_initialized((void *)((char *)q +
+ 4 * 0),
+ (size_t)__gen_e_acsl_if_4);
+ __e_acsl_assert(__gen_e_acsl_initialized_38,"Assertion","main",
+ "\\initialized(q + (0 .. 6))",
+ "tests/memory/initialized.c",100);
+ }
+ /*@ assert \initialized(q + (0 .. 6)); */ ;
+ {
+ int __gen_e_acsl_initialized_39;
+ __gen_e_acsl_initialized_39 = __e_acsl_initialized((void *)(q + 7),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_39,"Assertion","main",
+ "!\\initialized(q + 7)","tests/memory/initialized.c",101);
+ }
+ /*@ assert ¬\initialized(q + 7); */ ;
+ __e_acsl_full_init((void *)(& q));
+ q = (int *)realloc((void *)q,(unsigned long)10 * sizeof(int));
+ {
+ int __gen_e_acsl_size_5;
+ int __gen_e_acsl_if_5;
+ int __gen_e_acsl_initialized_40;
+ __gen_e_acsl_size_5 = 4 * ((6 - 0) + 1);
+ if (__gen_e_acsl_size_5 <= 0) __gen_e_acsl_if_5 = 0;
+ else __gen_e_acsl_if_5 = __gen_e_acsl_size_5;
+ __gen_e_acsl_initialized_40 = __e_acsl_initialized((void *)((char *)q +
+ 4 * 0),
+ (size_t)__gen_e_acsl_if_5);
+ __e_acsl_assert(__gen_e_acsl_initialized_40,"Assertion","main",
+ "\\initialized(q + (0 .. 6))",
+ "tests/memory/initialized.c",103);
+ }
+ /*@ assert \initialized(q + (0 .. 6)); */ ;
+ {
+ int __gen_e_acsl_initialized_41;
+ __gen_e_acsl_initialized_41 = __e_acsl_initialized((void *)(q + 7),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_41,"Assertion","main",
+ "!\\initialized(q + 7)","tests/memory/initialized.c",104);
+ }
+ /*@ assert ¬\initialized(q + 7); */ ;
+ {
+ int __gen_e_acsl_initialized_42;
+ __gen_e_acsl_initialized_42 = __e_acsl_initialized((void *)(q + 8),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_42,"Assertion","main",
+ "!\\initialized(q + 8)","tests/memory/initialized.c",105);
+ }
+ /*@ assert ¬\initialized(q + 8); */ ;
+ {
+ int __gen_e_acsl_initialized_43;
+ __gen_e_acsl_initialized_43 = __e_acsl_initialized((void *)(q + 9),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_43,"Assertion","main",
+ "!\\initialized(q + 9)","tests/memory/initialized.c",106);
+ }
+ /*@ assert ¬\initialized(q + 9); */ ;
+ free((void *)q);
+ __e_acsl_full_init((void *)(& q));
+ q = (int *)calloc((unsigned long)2,sizeof(int));
+ {
+ int __gen_e_acsl_size_6;
+ int __gen_e_acsl_if_6;
+ int __gen_e_acsl_initialized_44;
+ __gen_e_acsl_size_6 = 4 * ((1 - 0) + 1);
+ if (__gen_e_acsl_size_6 <= 0) __gen_e_acsl_if_6 = 0;
+ else __gen_e_acsl_if_6 = __gen_e_acsl_size_6;
+ __gen_e_acsl_initialized_44 = __e_acsl_initialized((void *)((char *)q +
+ 4 * 0),
+ (size_t)__gen_e_acsl_if_6);
+ __e_acsl_assert(__gen_e_acsl_initialized_44,"Assertion","main",
+ "\\initialized(q + (0 .. 1))",
+ "tests/memory/initialized.c",109);
+ }
+ /*@ assert \initialized(q + (0 .. 1)); */ ;
+ __e_acsl_full_init((void *)(& q));
+ q = (int *)realloc((void *)q,(unsigned long)4 * sizeof(int));
+ {
+ int __gen_e_acsl_size_7;
+ int __gen_e_acsl_if_7;
+ int __gen_e_acsl_initialized_45;
+ __gen_e_acsl_size_7 = 4 * ((1 - 0) + 1);
+ if (__gen_e_acsl_size_7 <= 0) __gen_e_acsl_if_7 = 0;
+ else __gen_e_acsl_if_7 = __gen_e_acsl_size_7;
+ __gen_e_acsl_initialized_45 = __e_acsl_initialized((void *)((char *)q +
+ 4 * 0),
+ (size_t)__gen_e_acsl_if_7);
+ __e_acsl_assert(__gen_e_acsl_initialized_45,"Assertion","main",
+ "\\initialized(q + (0 .. 1))",
+ "tests/memory/initialized.c",111);
+ }
+ /*@ assert \initialized(q + (0 .. 1)); */ ;
+ {
+ int __gen_e_acsl_initialized_46;
+ __gen_e_acsl_initialized_46 = __e_acsl_initialized((void *)(q + 2),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_46,"Assertion","main",
+ "!\\initialized(q + 2)","tests/memory/initialized.c",112);
+ }
+ /*@ assert ¬\initialized(q + 2); */ ;
+ {
+ int __gen_e_acsl_initialized_47;
+ __gen_e_acsl_initialized_47 = __e_acsl_initialized((void *)(q + 3),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_47,"Assertion","main",
+ "!\\initialized(q + 3)","tests/memory/initialized.c",113);
+ }
+ /*@ assert ¬\initialized(q + 3); */ ;
+ free((void *)q);
+ __e_acsl_full_init((void *)(& q));
+ q = (int *)calloc((unsigned long)6,sizeof(int));
+ {
+ int __gen_e_acsl_size_8;
+ int __gen_e_acsl_if_8;
+ int __gen_e_acsl_initialized_48;
+ __gen_e_acsl_size_8 = 4 * ((5 - 0) + 1);
+ if (__gen_e_acsl_size_8 <= 0) __gen_e_acsl_if_8 = 0;
+ else __gen_e_acsl_if_8 = __gen_e_acsl_size_8;
+ __gen_e_acsl_initialized_48 = __e_acsl_initialized((void *)((char *)q +
+ 4 * 0),
+ (size_t)__gen_e_acsl_if_8);
+ __e_acsl_assert(__gen_e_acsl_initialized_48,"Assertion","main",
+ "\\initialized(q + (0 .. 5))",
+ "tests/memory/initialized.c",116);
+ }
+ /*@ assert \initialized(q + (0 .. 5)); */ ;
+ __e_acsl_full_init((void *)(& q));
+ q = (int *)realloc((void *)q,(unsigned long)3 * sizeof(int));
+ {
+ int __gen_e_acsl_size_9;
+ int __gen_e_acsl_if_9;
+ int __gen_e_acsl_initialized_49;
+ __gen_e_acsl_size_9 = 4 * ((2 - 0) + 1);
+ if (__gen_e_acsl_size_9 <= 0) __gen_e_acsl_if_9 = 0;
+ else __gen_e_acsl_if_9 = __gen_e_acsl_size_9;
+ __gen_e_acsl_initialized_49 = __e_acsl_initialized((void *)((char *)q +
+ 4 * 0),
+ (size_t)__gen_e_acsl_if_9);
+ __e_acsl_assert(__gen_e_acsl_initialized_49,"Assertion","main",
+ "\\initialized(q + (0 .. 2))",
+ "tests/memory/initialized.c",118);
+ }
+ /*@ assert \initialized(q + (0 .. 2)); */ ;
+ free((void *)q);
+ __e_acsl_full_init((void *)(& q));
+ q = (int *)malloc((unsigned long)6 * sizeof(int));
+ {
+ int __gen_e_acsl_initialized_50;
+ __gen_e_acsl_initialized_50 = __e_acsl_initialized((void *)(q + 0),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_50,"Assertion","main",
+ "!\\initialized(q + 0)","tests/memory/initialized.c",121);
+ }
+ /*@ assert ¬\initialized(q + 0); */ ;
+ {
+ int __gen_e_acsl_initialized_51;
+ __gen_e_acsl_initialized_51 = __e_acsl_initialized((void *)(q + 1),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_51,"Assertion","main",
+ "!\\initialized(q + 1)","tests/memory/initialized.c",122);
+ }
+ /*@ assert ¬\initialized(q + 1); */ ;
+ {
+ int __gen_e_acsl_initialized_52;
+ __gen_e_acsl_initialized_52 = __e_acsl_initialized((void *)(q + 2),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_52,"Assertion","main",
+ "!\\initialized(q + 2)","tests/memory/initialized.c",123);
+ }
+ /*@ assert ¬\initialized(q + 2); */ ;
+ {
+ int __gen_e_acsl_initialized_53;
+ __gen_e_acsl_initialized_53 = __e_acsl_initialized((void *)(q + 3),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_53,"Assertion","main",
+ "!\\initialized(q + 3)","tests/memory/initialized.c",124);
+ }
+ /*@ assert ¬\initialized(q + 3); */ ;
+ {
+ int __gen_e_acsl_initialized_54;
+ __gen_e_acsl_initialized_54 = __e_acsl_initialized((void *)(q + 4),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_54,"Assertion","main",
+ "!\\initialized(q + 4)","tests/memory/initialized.c",125);
+ }
+ /*@ assert ¬\initialized(q + 4); */ ;
+ {
+ int __gen_e_acsl_initialized_55;
+ __gen_e_acsl_initialized_55 = __e_acsl_initialized((void *)(q + 5),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_55,"Assertion","main",
+ "!\\initialized(q + 5)","tests/memory/initialized.c",126);
+ }
+ /*@ assert ¬\initialized(q + 5); */ ;
+ __e_acsl_full_init((void *)(& q));
+ q = (int *)realloc((void *)q,(unsigned long)3 * sizeof(int));
+ {
+ int __gen_e_acsl_initialized_56;
+ __gen_e_acsl_initialized_56 = __e_acsl_initialized((void *)(q + 0),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_56,"Assertion","main",
+ "!\\initialized(q + 0)","tests/memory/initialized.c",128);
+ }
+ /*@ assert ¬\initialized(q + 0); */ ;
+ {
+ int __gen_e_acsl_initialized_57;
+ __gen_e_acsl_initialized_57 = __e_acsl_initialized((void *)(q + 1),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_57,"Assertion","main",
+ "!\\initialized(q + 1)","tests/memory/initialized.c",129);
+ }
+ /*@ assert ¬\initialized(q + 1); */ ;
+ {
+ int __gen_e_acsl_initialized_58;
+ __gen_e_acsl_initialized_58 = __e_acsl_initialized((void *)(q + 2),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_58,"Assertion","main",
+ "!\\initialized(q + 2)","tests/memory/initialized.c",130);
+ }
+ /*@ assert ¬\initialized(q + 2); */ ;
+ free((void *)q);
+ __e_acsl_full_init((void *)(& q));
q = (int *)(& q - 1024 * 5);
__e_acsl_full_init((void *)(& q));
q = (int *)128;
{
- int __gen_e_acsl_initialized_32;
- __gen_e_acsl_initialized_32 = __e_acsl_initialized((void *)q,sizeof(int));
- __e_acsl_assert(! __gen_e_acsl_initialized_32,"Assertion","main",
- "!\\initialized(q)","tests/memory/initialized.c",93);
+ int __gen_e_acsl_initialized_59;
+ __gen_e_acsl_initialized_59 = __e_acsl_initialized((void *)q,sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_59,"Assertion","main",
+ "!\\initialized(q)","tests/memory/initialized.c",139);
}
/*@ assert ¬\initialized(q); */ ;
__e_acsl_full_init((void *)(& p));
p = (int *)0;
{
- int __gen_e_acsl_initialized_33;
- __gen_e_acsl_initialized_33 = __e_acsl_initialized((void *)p,sizeof(int));
- __e_acsl_assert(! __gen_e_acsl_initialized_33,"Assertion","main",
- "!\\initialized(p)","tests/memory/initialized.c",96);
+ int __gen_e_acsl_initialized_60;
+ __gen_e_acsl_initialized_60 = __e_acsl_initialized((void *)p,sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_60,"Assertion","main",
+ "!\\initialized(p)","tests/memory/initialized.c",142);
}
/*@ assert ¬\initialized(p); */ ;
int size = 100;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_struct_initialized.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_struct_initialized.c
new file mode 100644
index 0000000000000000000000000000000000000000..1e1047dc8b47a51c32345364e5bcb7c37dcf6ee8
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_struct_initialized.c
@@ -0,0 +1,147 @@
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdint.h"
+#include "stdio.h"
+#include "stdlib.h"
+struct __anonstruct_int32_pair_t_1 {
+ int32_t a ;
+ int32_t b ;
+};
+typedef struct __anonstruct_int32_pair_t_1 int32_pair_t;
+int main(void)
+{
+ int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ {
+ int32_pair_t static_pair;
+ __e_acsl_store_block((void *)(& static_pair),(size_t)8);
+ {
+ int __gen_e_acsl_initialized;
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& static_pair.a),
+ sizeof(int32_t));
+ __e_acsl_assert(! __gen_e_acsl_initialized,"Assertion","main",
+ "!\\initialized(&static_pair.a)",
+ "tests/memory/struct_initialized.c",13);
+ }
+ /*@ assert ¬\initialized(&static_pair.a); */ ;
+ {
+ int __gen_e_acsl_initialized_2;
+ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& static_pair.b),
+ sizeof(int32_t));
+ __e_acsl_assert(! __gen_e_acsl_initialized_2,"Assertion","main",
+ "!\\initialized(&static_pair.b)",
+ "tests/memory/struct_initialized.c",14);
+ }
+ /*@ assert ¬\initialized(&static_pair.b); */ ;
+ __e_acsl_initialize((void *)(& static_pair.a),sizeof(int32_t));
+ static_pair.a = 1;
+ {
+ int __gen_e_acsl_initialized_3;
+ __gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)(& static_pair.a),
+ sizeof(int32_t));
+ __e_acsl_assert(__gen_e_acsl_initialized_3,"Assertion","main",
+ "\\initialized(&static_pair.a)",
+ "tests/memory/struct_initialized.c",16);
+ }
+ /*@ assert \initialized(&static_pair.a); */ ;
+ {
+ int __gen_e_acsl_initialized_4;
+ __gen_e_acsl_initialized_4 = __e_acsl_initialized((void *)(& static_pair.b),
+ sizeof(int32_t));
+ __e_acsl_assert(! __gen_e_acsl_initialized_4,"Assertion","main",
+ "!\\initialized(&static_pair.b)",
+ "tests/memory/struct_initialized.c",17);
+ }
+ /*@ assert ¬\initialized(&static_pair.b); */ ;
+ __e_acsl_initialize((void *)(& static_pair.b),sizeof(int32_t));
+ static_pair.b = 2;
+ {
+ int __gen_e_acsl_initialized_5;
+ __gen_e_acsl_initialized_5 = __e_acsl_initialized((void *)(& static_pair.a),
+ sizeof(int32_t));
+ __e_acsl_assert(__gen_e_acsl_initialized_5,"Assertion","main",
+ "\\initialized(&static_pair.a)",
+ "tests/memory/struct_initialized.c",19);
+ }
+ /*@ assert \initialized(&static_pair.a); */ ;
+ {
+ int __gen_e_acsl_initialized_6;
+ __gen_e_acsl_initialized_6 = __e_acsl_initialized((void *)(& static_pair.b),
+ sizeof(int32_t));
+ __e_acsl_assert(__gen_e_acsl_initialized_6,"Assertion","main",
+ "\\initialized(&static_pair.b)",
+ "tests/memory/struct_initialized.c",20);
+ }
+ /*@ assert \initialized(&static_pair.b); */ ;
+ __e_acsl_delete_block((void *)(& static_pair));
+ }
+ {
+ int32_pair_t *heap_pair = malloc(sizeof(int32_pair_t));
+ __e_acsl_store_block((void *)(& heap_pair),(size_t)8);
+ __e_acsl_full_init((void *)(& heap_pair));
+ {
+ int __gen_e_acsl_initialized_7;
+ __gen_e_acsl_initialized_7 = __e_acsl_initialized((void *)(& heap_pair->a),
+ sizeof(int32_t));
+ __e_acsl_assert(! __gen_e_acsl_initialized_7,"Assertion","main",
+ "!\\initialized(&heap_pair->a)",
+ "tests/memory/struct_initialized.c",26);
+ }
+ /*@ assert ¬\initialized(&heap_pair->a); */ ;
+ {
+ int __gen_e_acsl_initialized_8;
+ __gen_e_acsl_initialized_8 = __e_acsl_initialized((void *)(& heap_pair->b),
+ sizeof(int32_t));
+ __e_acsl_assert(! __gen_e_acsl_initialized_8,"Assertion","main",
+ "!\\initialized(&heap_pair->b)",
+ "tests/memory/struct_initialized.c",27);
+ }
+ /*@ assert ¬\initialized(&heap_pair->b); */ ;
+ __e_acsl_initialize((void *)(& heap_pair->a),sizeof(int32_t));
+ heap_pair->a = 3;
+ {
+ int __gen_e_acsl_initialized_9;
+ __gen_e_acsl_initialized_9 = __e_acsl_initialized((void *)(& heap_pair->a),
+ sizeof(int32_t));
+ __e_acsl_assert(__gen_e_acsl_initialized_9,"Assertion","main",
+ "\\initialized(&heap_pair->a)",
+ "tests/memory/struct_initialized.c",29);
+ }
+ /*@ assert \initialized(&heap_pair->a); */ ;
+ {
+ int __gen_e_acsl_initialized_10;
+ __gen_e_acsl_initialized_10 = __e_acsl_initialized((void *)(& heap_pair->b),
+ sizeof(int32_t));
+ __e_acsl_assert(! __gen_e_acsl_initialized_10,"Assertion","main",
+ "!\\initialized(&heap_pair->b)",
+ "tests/memory/struct_initialized.c",30);
+ }
+ /*@ assert ¬\initialized(&heap_pair->b); */ ;
+ __e_acsl_initialize((void *)(& heap_pair->b),sizeof(int32_t));
+ heap_pair->b = 4;
+ {
+ int __gen_e_acsl_initialized_11;
+ __gen_e_acsl_initialized_11 = __e_acsl_initialized((void *)(& heap_pair->a),
+ sizeof(int32_t));
+ __e_acsl_assert(__gen_e_acsl_initialized_11,"Assertion","main",
+ "\\initialized(&heap_pair->a)",
+ "tests/memory/struct_initialized.c",32);
+ }
+ /*@ assert \initialized(&heap_pair->a); */ ;
+ {
+ int __gen_e_acsl_initialized_12;
+ __gen_e_acsl_initialized_12 = __e_acsl_initialized((void *)(& heap_pair->b),
+ sizeof(int32_t));
+ __e_acsl_assert(__gen_e_acsl_initialized_12,"Assertion","main",
+ "\\initialized(&heap_pair->b)",
+ "tests/memory/struct_initialized.c",33);
+ }
+ /*@ assert \initialized(&heap_pair->b); */ ;
+ __e_acsl_delete_block((void *)(& heap_pair));
+ }
+ __retres = 0;
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/struct_initialized.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/struct_initialized.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..efd026311297e55d8fefb674326118e6ece88624
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/struct_initialized.res.oracle
@@ -0,0 +1,2 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/struct_initialized.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/struct_initialized.e-acsl.err.log
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/memory/struct_initialized.c b/src/plugins/e-acsl/tests/memory/struct_initialized.c
new file mode 100644
index 0000000000000000000000000000000000000000..87ee96337d2ebfbddd575f46715f31fbd7b338d3
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/struct_initialized.c
@@ -0,0 +1,35 @@
+#include <stdint.h>
+#include <stdlib.h>
+
+typedef struct {
+ int32_t a;
+ int32_t b;
+} int32_pair_t;
+
+int main() {
+ // Static alloc
+ {
+ int32_pair_t static_pair;
+ //@ assert !\initialized(&static_pair.a);
+ //@ assert !\initialized(&static_pair.b);
+ static_pair.a = 1;
+ //@ assert \initialized(&static_pair.a);
+ //@ assert !\initialized(&static_pair.b);
+ static_pair.b = 2;
+ //@ assert \initialized(&static_pair.a);
+ //@ assert \initialized(&static_pair.b);
+ }
+
+ // Dynamic alloc
+ {
+ int32_pair_t * heap_pair = malloc(sizeof(int32_pair_t));
+ //@ assert !\initialized(&heap_pair->a);
+ //@ assert !\initialized(&heap_pair->b);
+ heap_pair->a = 3;
+ //@ assert \initialized(&heap_pair->a);
+ //@ assert !\initialized(&heap_pair->b);
+ heap_pair->b = 4;
+ //@ assert \initialized(&heap_pair->a);
+ //@ assert \initialized(&heap_pair->b);
+ }
+}
diff --git a/src/plugins/value/engine/transfer_specification.ml b/src/plugins/value/engine/transfer_specification.ml
index 4521648ffbbe9efce1e5e6a20a06226aba7309fb..0ddcbfb9a4a5772b0cce3b101da14533eb592f2a 100644
--- a/src/plugins/value/engine/transfer_specification.ml
+++ b/src/plugins/value/engine/transfer_specification.ml
@@ -291,7 +291,7 @@ module Make
Value_parameters.warning ~current:true ~once:true
~wkey:Value_parameters.wkey_garbled_mix
"The specification of function %a has generated a garbled mix \
- for assigns clause %a."
+ for %a."
Kernel_function.pretty kf pp_assign_free_alloc assign
end
in
diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml
index 3c9a5f797a62fa1879dab6209297e3bda177d835..19e8070cf06d110febdbf0a04f7c5aa471445f94 100644
--- a/src/plugins/wp/Why3Provers.ml
+++ b/src/plugins/wp/Why3Provers.ml
@@ -64,7 +64,6 @@ let find_opt s =
try
let config = Lazy.force cfg in
let filter = Why3.Whyconf.parse_filter_prover s in
- let filter = Why3.Whyconf.filter_prover_with_shortcut config filter in
Some ((Why3.Whyconf.filter_one_prover config filter).Why3.Whyconf.prover)
with
| Why3.Whyconf.ProverNotFound _
@@ -78,14 +77,18 @@ let find_fallback name =
match find_opt name with
| Some prv -> Exact prv
| None ->
- match String.split_on_char ',' name with
- | shortname :: _ :: _ ->
- begin
- match find_opt (String.lowercase_ascii shortname) with
- | Some prv -> Fallback prv
- | None -> NotFound
- end
- | _ -> NotFound
+ (* Why3 should deal with this intermediate case *)
+ match find_opt (String.lowercase_ascii name) with
+ | Some prv -> Exact prv
+ | None ->
+ match String.split_on_char ',' name with
+ | shortname :: _ :: _ ->
+ begin
+ match find_opt (String.lowercase_ascii shortname) with
+ | Some prv -> Fallback prv
+ | None -> NotFound
+ end
+ | _ -> NotFound
let print_why3 = Why3.Whyconf.prover_parseable_format
let print_wp s =
diff --git a/src/plugins/wp/configure.ac b/src/plugins/wp/configure.ac
index 052fd1617d8adadc08240f26a10416921815c5c1..fd5332ac5852ace356de9d2701ff32bd9af1c0c6 100644
--- a/src/plugins/wp/configure.ac
+++ b/src/plugins/wp/configure.ac
@@ -85,16 +85,14 @@ if test "$ENABLE_WP" != "no"; then
if test "$COQC" = "yes" ; then
COQVERSION=`coqc -v | sed -n -e 's|.*version* *\([[^ ]]*\) .*$|\1|p' `
case $COQVERSION in
- 8.7*|8.8*|8.9*|8.10*|8.11.*|8.12.*|trunk)
+ 8.12.*|trunk)
AC_MSG_RESULT(coqc version $COQVERSION found)
;;
*)
- AC_MSG_RESULT(unsupported coqc version $COQVERSION)
+ AC_MSG_RESULT(unsupported coqc version $COQVERSION for - deprecated - native backend)
COQC="no"
;;
esac
- else
- AC_MSG_NOTICE(rerun configure to make wp using coq 8.7.2 or higher)
fi
else
COQC="no"
diff --git a/src/plugins/wp/doc/manual/wp.tex b/src/plugins/wp/doc/manual/wp.tex
index 205dddf92337c035f079f0e4411752894f3f2bec..b80b0af7ed8433e30119fb309e4cb68f21cc2283 100644
--- a/src/plugins/wp/doc/manual/wp.tex
+++ b/src/plugins/wp/doc/manual/wp.tex
@@ -21,7 +21,7 @@
\vfill
\title{WP Plug-in Manual}%
{\tt Frama-C \FCVERSION}
-\author{Patrick Baudin, François Bobot, Loïc Correnson, Zaynah Dargaye}
+\author{Patrick Baudin, François Bobot, Loïc Correnson, Zaynah Dargaye, Allan Blanchard}
\begin{center}
CEA LIST, Software Safety Laboratory
\end{center}
diff --git a/src/plugins/wp/doc/manual/wp_logic.tex b/src/plugins/wp/doc/manual/wp_logic.tex
index 83218a58bcd0beba00723c50f67ee54e7cab2308..0bb2a2b6fc0def05c324711e4fe0bc4ffa00f7a1 100644
--- a/src/plugins/wp/doc/manual/wp_logic.tex
+++ b/src/plugins/wp/doc/manual/wp_logic.tex
@@ -188,8 +188,9 @@ the separation and validity hypotheses associated to the choice that
it make of dispatching each pointer and variable either to the
\lstinline{Hoare} or to the model $\cal{M}$ used for the heap.
-Thus, in addition to user-defined function \lstinline{requires}, WP
-also states as \lstinline{requires} that:
+Consequently, in addition to user-defined function \lstinline{requires},
+WP also assumes, and thus states as \lstinline{requires} for the function
+caller, that:
\begin{itemize}
\item \lstinline{Hoare} variables are separated from each other,
@@ -203,10 +204,10 @@ also states as \lstinline{requires} that:
Furthermore, the function must ensure that:
\begin{itemize}
-\item locations assigned via a pointer (including returned value when
+\item locations assigned via a pointer (including the returned value when
it is a pointer) are separated from \lstinline{Hoare} variables whose address
is not taken by the function (including via its contract),
-\item pointers assigned by the function (including returned value when
+\item pointers assigned by the function (including the returned value when
it is a pointer) are separated from function parameters and \lstinline{Hoare}
variables whose address is not taken by the function (including via
its contract).
@@ -216,9 +217,9 @@ In order to precisely generate these hypotheses, WP needs precise
\lstinline{assigns} specification. In particular each function under
verification and all its callees needs an \lstinline{assigns} specification.
Furthermore, if the function assigns or returns a pointer, WP needs
-a correct \lstinline{\from} specification. If the specification is
-incomplete, a warning \lstinline{wp:pedantic-assigns} is triggered.
-Note that WP does not verify that the \lstinline{\from} is correct.
+a correct \lstinline{\from} specification for those pointers. If the
+specification is incomplete, a warning \lstinline{wp:pedantic-assigns} is
+triggered. Note that WP does not verify that the \lstinline{\from} is correct.
The hypotheses are displayed when the option
\lstinline{-wp-warn-memory-model} is enable (it is enabled by default).
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index aaf0e60480d3adc4ea3bf6eeafe3eff30a0d0fd8..2b8883193da78ee750e872a9c73aa84695972f98 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -414,6 +414,29 @@ to apply the theorems. Such a strategy is \emph{not} complete in general.
Typically, $\mathtt{land}(x,y) < 38$ is true whenever both $x$ and $y$ are in range $0\ldots 31$, but this is also true
in other cases.
+\paragraph{Bit-Test Range} Tighten bounds with respect to bits \\
+The \lstinline{bit_test(a,b)} function is predefined in \textsf{WP} and is equivalent
+to the \textsf{ACSL} expression \lstinline{(a & (1 << k)) != 0}. The
+\textsf{Qed}Â engine has many simplification rules that applies to
+such patterns.
+
+The user selects an expression $\mathtt{bit\_test}(n,k)$ with $k$
+a \emph{constant} integer value greater or equal to 0 and lower than
+128. The tactic uses this test to thighten the bounds of $n$.
+
+$$\TACTIC{\Delta\models\,G}{%
+\begin{array}[t]{ll}
+\Delta,T &\models G \\
+\Delta,F &\models G
+\end{array}} $$
+
+with
+$$\begin{array}[t]{rlcll}
+ T \equiv & \mathtt{bit\_test}(n,k) & \wedge & (0 \leq n & \Rightarrow 2^{k} \leq n) \\
+ F \equiv & \neg \mathtt{bit\_test}(n,k) & \wedge & (0 \leq n < 2^{k+1} & \Rightarrow n < 2^{k})
+ \end{array}
+$$
+
\paragraph{Bitwise} Decompose equalities over $N$-bits\\
The use selects an integer equality and a number of bits.
Providing the two members of the equality are in range $0..2^N-1$,
@@ -431,11 +454,6 @@ where $\sigma$ is the following subsitution:
\right]
\]
-The \lstinline{bit_test(a,b)} function is predefined in \textsf{WP} and is equivalent
-to the \textsf{ACSL} expression \lstinline{(a & (1 << k)) != 0}. The
-\textsf{Qed}Â engine has many simplification rules that applies to
-such patterns, and the a tactic is good way to reason over bits.
-
\paragraph{Congruence} Simplify Divisions and Products \\
This tactic rewrites integer comparisons involving products and divisions.
The tactic applies one of the following theorems to the current goal.
@@ -578,6 +596,11 @@ Rule for unroll sum:
\end{array}
}\]
+\paragraph{Validity} Unfold validity and range definitions\\
+The user selects a validity expression (\lstinline{valid_rd},
+\lstinline{valid_rw}, \lstinline{invalid} or \lstinline{included}).
+The expression is unfolded to a \textsf{Qed} term.
+
\subsection{Custom Tactics and Strategies}
\label{wp-custom-tactics}
@@ -940,14 +963,37 @@ weakest precondition calculus.
and it can generates a large number of verifications for structures
with many (nested) fields (defaults to \texttt{no}).
\item[\tt -wp-(no)-dynamic] handles calls \textit{via} function pointers
- thanks to the dedicated \verb+@calls f1,...,fn+ code annotation.
- For each call to a function pointer \texttt{fp}
- in the instruction or block under the annotation,
- \texttt{fp} is required to belongs to the set \texttt{f1,\ldots,fn} and
- a case analysis is performed with the contract of each provided function
- (default is: \texttt{yes}).
+ thanks to the dedicated \verb+@calls f1,...,fn+ code annotation (default is: \texttt{yes}).
\end{description}
+\subsubsection{ACSL extension \texttt{@calls}}
+
+The handling of functions pointers is done via the ACSL code annotation
+extension \verb+@calls+. For each call to a function pointer \verb+fp+
+in the instruction or block under the annotation \verb+calls f1,\ldots,fn+,
+\verb+fp+ is required to belongs to the set \verb+f1,\ldots,fn+ and
+a case analysis is performed with the contract of each provided function.
+
+For example:
+
+\begin{lstlisting}[language=c, alsolanguage=acsl]
+/*@ ensures \result == x ; */
+int f1(int x);
+/*@ ensures \result == x+1 ; */
+int f2(int x);
+
+/*@ requires fp == &f1 || fp == &f2 ;
+ ensures POST: \result == 4 || \result == 5; */
+int caller(int (*fp)(int)){
+ //@ calls f1, f2 ;
+ return (*fp)(4);
+}
+\end{lstlisting}
+
+These annotations split post-conditions to the dynamic call into two sub-goals: one for call to \verb+f1+ and
+a second for the call to \verb+f2+. A last goal is generated at the call
+site: one must prove that \verb+fp+ is either \verb+f1+ or \verb+f2+.
+
\subsection{Smoke Tests}
During modular deductive verification, inconsistencies in function requirements
diff --git a/src/plugins/wp/tests/wp_acsl/generalized_checks.i b/src/plugins/wp/tests/wp_acsl/generalized_checks.i
index 3b34ced34e21bad22ab97aaefd60da416ce909d5..88b32e9f49a4bfc1c00b532287fa1563153e592e 100644
--- a/src/plugins/wp/tests/wp_acsl/generalized_checks.i
+++ b/src/plugins/wp/tests/wp_acsl/generalized_checks.i
@@ -64,3 +64,17 @@ int caller(int x)
{
return job(x); // CA2 is not proved
}
+
+void loop () {
+ int j = 0;
+ /*@ check loop invariant false_but_preserved: j == 10;
+ loop assigns i;
+ */
+ for (int i = 0; i< 10; i++);
+ /*@ check implied_by_false_invariant: j == 10; */
+ l: /*@ check invariant \true; */ ;
+ if (j >= 10) goto l1;
+ j++;
+ goto l;
+ l1 : ;
+}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle
index 233aa076c4f47f9a17aefdc2159597328de1ab61..d3f8259be9d299489b8ec49ccfac1bf68ef51b21 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle
@@ -1,7 +1,13 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/generalized_checks.i (no preprocessing)
[wp] Running WP plugin...
+[wp] tests/wp_acsl/generalized_checks.i:68: Warning:
+ Unsupported generalized invariant, use loop invariant instead.
+ Ignored invariant
+ check invariant \true;
[wp] Warning: Missing RTE guards
+[wp] tests/wp_acsl/generalized_checks.i:75: Warning:
+ Missing assigns clause (assigns 'everything' instead)
------------------------------------------------------------
Axiomatic 'Th'
------------------------------------------------------------
@@ -136,3 +142,28 @@ Call Result at line 52
Prove: true.
------------------------------------------------------------
+------------------------------------------------------------
+ Function loop
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'false_but_preserved' (file tests/wp_acsl/generalized_checks.i, line 70):
+Assume { Type: is_sint32(i). (* Then *) Have: i <= 9. }
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'false_but_preserved' (file tests/wp_acsl/generalized_checks.i, line 70):
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Check 'implied_by_false_invariant' (file tests/wp_acsl/generalized_checks.i, line 74):
+Assume { Type: is_sint32(i). (* Else *) Have: 10 <= i. }
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/generalized_checks.i, line 71):
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle
index ee38ba7972748686bc43809b5174f8930279ea0e..5ab67d884fd17c3d2e9f352df274bc25ae478da1 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle
@@ -1,8 +1,14 @@
# frama-c -wp -wp-timeout 1 [...]
[kernel] Parsing tests/wp_acsl/generalized_checks.i (no preprocessing)
[wp] Running WP plugin...
+[wp] tests/wp_acsl/generalized_checks.i:68: Warning:
+ Unsupported generalized invariant, use loop invariant instead.
+ Ignored invariant
+ check invariant \true;
[wp] Warning: Missing RTE guards
-[wp] 17 goals scheduled
+[wp] tests/wp_acsl/generalized_checks.i:75: Warning:
+ Missing assigns clause (assigns 'everything' instead)
+[wp] 21 goals scheduled
[wp] [Alt-Ergo] Goal typed_check_lemma_C_ko : Unsuccess
[wp] [Alt-Ergo] Goal typed_lemma_L_ko : Unsuccess
[wp] [Alt-Ergo] Goal typed_job_ensures_B : Valid
@@ -20,9 +26,13 @@
[wp] [Qed] Goal typed_caller_call_job_requires_A : Valid
[wp] [Qed] Goal typed_caller_call_job_check_requires_CA1 : Valid
[wp] [Alt-Ergo] Goal typed_caller_call_job_check_requires_CA2_ko : Unsuccess
-[wp] Proved goals: 11 / 17
- Qed: 9
- Alt-Ergo: 2 (unsuccess: 6)
+[wp] [Alt-Ergo] Goal typed_loop_check_loop_invariant_false_but_preserved_preserved : Unsuccess
+[wp] [Alt-Ergo] Goal typed_loop_check_loop_invariant_false_but_preserved_established : Unsuccess
+[wp] [Alt-Ergo] Goal typed_loop_check_implied_by_false_invariant : Unsuccess
+[wp] [Qed] Goal typed_loop_loop_assigns : Valid
+[wp] Proved goals: 12 / 21
+ Qed: 10
+ Alt-Ergo: 2 (unsuccess: 9)
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Axiomatic Th - - 2 0.0%
@@ -30,4 +40,5 @@
Functions WP Alt-Ergo Total Success
job 3 2 6 83.3%
caller 6 - 9 66.7%
+ loop 1 - 4 25.0%
------------------------------------------------------------
diff --git a/src/plugins/wp/wpStrategy.ml b/src/plugins/wp/wpStrategy.ml
index 96f589da256b9329369a41a49b171e172f687230..7026d2402035f301bee12cf740d9b92663f712f0 100644
--- a/src/plugins/wp/wpStrategy.ml
+++ b/src/plugins/wp/wpStrategy.ml
@@ -318,6 +318,11 @@ let add_prop_dead_call kf stmt acc_posts acc_exits =
(* -------------------------------------------------------------------------- *)
+let from_has_deps = function _, FromAny -> false | _, From _ -> true
+let assigns_has_deps = function
+ | WritesAny -> false
+ | Writes l -> List.exists from_has_deps l
+
let add_assigns acc kind id a_desc =
let take_assigns () =
debug "take %a %a" WpPropId.pp_propid id WpPropId.pp_assigns_desc a_desc;
@@ -334,6 +339,11 @@ let add_assigns acc kind id a_desc =
| Agoal -> true, {info with a_goal = take_assigns ()}
| _ -> Wp_parameters.fatal "Assigns prop can only be Hyp or Goal"
in let acc = { acc with info = info } in
+ if goal && assigns_has_deps a_desc.a_assigns then
+ Wp_parameters.warning
+ ~once: true ~current:false ~wkey:AssignsCompleteness.wkey_pedantic
+ "WP uses \\from to generate precise hypotheses, however their proof is \
+ not supported yet" ;
if goal then { acc with has_asgn_goal = true} else acc
let add_assigns_any acc kind asgn =
diff --git a/tests/libc/math_h.c b/tests/libc/math_h.c
index 95ded2bf103805d967ffae4a1525e5a4bc828ae6..1f732635d7643caa9b9bb02bdaae0d3950fbcff7 100644
--- a/tests/libc/math_h.c
+++ b/tests/libc/math_h.c
@@ -1,4 +1,5 @@
/* run.config
+ FILTER: sed -E -e '/atanf_/ s/([0-9][.][0-9]{6})[0-9]+/\1/g'
STDOPT: #"-warn-special-float none" #"-cpp-extra-args=\"-DNONFINITE\""
*/
#include <math.h>
@@ -29,7 +30,6 @@ const double fp_ilogb0 = FP_ILOGB0;
const double fp_ilogbnan = FP_ILOGBNAN;
#define TEST_VAL(type,f,c) type f##_##c = f(c)
-
#define TEST_FUN(type,f,prefix) \
TEST_VAL(type,f,prefix##pi); \
TEST_VAL(type,f,prefix##half_pi); \
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 1c7f3e7c9488445e723a1e84af235443d579c607..ea25b25f657c75f8ceeeaed060cf712e5c7268bb 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -3994,7 +3994,7 @@ extern size_t strcspn(char const *s, char const *reject);
/*@ requires valid_string_s: valid_read_string(s);
requires valid_string_accept: valid_read_string(accept);
ensures result_bounded: 0 ≤ \result ≤ strlen(\old(s));
- assigns \result, \result;
+ assigns \result;
assigns \result \from *(s + (0 ..)), *(accept + (0 ..));
assigns \result
\from (indirect: *(s + (0 ..))), (indirect: *(accept + (0 ..)));
diff --git a/tests/libc/oracle/math_h.res.oracle b/tests/libc/oracle/math_h.res.oracle
index 9f997874c0f244b3e9afeb9b62afb588a606109d..5c82e6d555400766e3b3344eb6978de25494ce5f 100644
--- a/tests/libc/oracle/math_h.res.oracle
+++ b/tests/libc/oracle/math_h.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/libc/math_h.c (with preprocessing)
-[kernel:parser:decimal-float] tests/libc/math_h.c:5: Warning:
+[kernel:parser:decimal-float] tests/libc/math_h.c:6: Warning:
Floating-point constant 3.14159265358979323846264338327950288 is not represented exactly. Will use 0x1.921fb54442d18p1.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[eva] Analyzing a complete application starting at main
@@ -280,15 +280,15 @@
atan_minus_one ∈ {-0.785398163397}
atan_large ∈ {1.57079632679}
atan_top ∈ [-1.57079632679 .. 1.57079632679] ∪ {NaN}
- atanf_f_pi ∈ {1.262627244}
- atanf_f_half_pi ∈ {1.00388479233}
- atanf_f_e ∈ {1.218282938}
+ atanf_f_pi ∈ {1.262627}
+ atanf_f_half_pi ∈ {1.003884}
+ atanf_f_e ∈ {1.218282}
atanf_zero ∈ {0}
atanf_minus_zero ∈ {-0.}
- atanf_one ∈ {0.785398185253}
- atanf_minus_one ∈ {-0.785398185253}
- atanf_large ∈ {1.57079637051}
- atanf_f_top ∈ [-1.57079637051 .. 1.57079637051] ∪ {NaN}
+ atanf_one ∈ {0.785398}
+ atanf_minus_one ∈ {-0.785398}
+ atanf_large ∈ {1.570796}
+ atanf_f_top ∈ [-1.570796 .. 1.570796] ∪ {NaN}
atanl_ld_pi ∈ [-inf .. inf]
atanl_ld_half_pi ∈ [-inf .. inf]
atanl_ld_e ∈ [-inf .. inf]
diff --git a/tests/rte/oracle/assign4.res.oracle b/tests/rte/oracle/assign4.res.oracle
index e835835a444036c29505eac0bde563c5fcc12dce..143f1a6b3fcb116c94c4f1f3e00b27372d1e075d 100644
--- a/tests/rte/oracle/assign4.res.oracle
+++ b/tests/rte/oracle/assign4.res.oracle
@@ -5,10 +5,8 @@
assigns \result \from min, max; */
int choose1(int min, int max);
-/*@ assigns \result, \result;
- assigns \result \from min, max, min, max;
- assigns \result \from min, max, min, max;
- */
+/*@ assigns \result;
+ assigns \result \from min, max; */
int choose2(int min, int max);
int main(void)
diff --git a/tests/rte/oracle/assign5.res.oracle b/tests/rte/oracle/assign5.res.oracle
index 7240925afa98a9cc66e358cbd24e22615203e5b6..52d1def1f07ac9c260c9f52025366357dfa448a3 100644
--- a/tests/rte/oracle/assign5.res.oracle
+++ b/tests/rte/oracle/assign5.res.oracle
@@ -1,14 +1,16 @@
[kernel] Parsing tests/rte/assign5.c (with preprocessing)
+[kernel:annot:multi-from] Warning:
+ Drop '*p' \from at tests/rte/assign5.c:9 for more precise one at tests/rte/assign5.c:10
+[kernel:annot:multi-from] Warning:
+ Drop '*p' \from at tests/rte/assign5.c:19 for more precise one at tests/rte/assign5.c:18
[rte] annotating function main
/* Generated by Frama-C */
-/*@ assigns *p, *p;
- assigns *p \from x;
+/*@ assigns *p;
assigns *p \from \nothing; */
int f(int *p, int x);
-/*@ assigns *p, *p;
- assigns *p \from \nothing;
- assigns *p \from x; */
+/*@ assigns *p;
+ assigns *p \from \nothing; */
int g(int *p, int x);
int main(void)
diff --git a/tests/spec/generalized_check.i b/tests/spec/generalized_check.i
index baf66eaa6b7c65976cc5218477b20cb503d4d012..06f74139cfb7854ec517df292b9ca720dbd9ceed 100644
--- a/tests/spec/generalized_check.i
+++ b/tests/spec/generalized_check.i
@@ -1,8 +1,8 @@
/* run.config
-OPT: -wp -wp-prover qed -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive
OPT: -eva -eva-use-spec f
OPT: -print
*/
+
/*@ check lemma easy_proof: \false; */ // should not be put in any environment
/*@ check requires f_valid_x: \valid(x);
diff --git a/tests/spec/oracle/generalized_check.0.res.oracle b/tests/spec/oracle/generalized_check.0.res.oracle
index 391634ac903d7d727471bf1b9ed212817085093b..f93e7228b403b708b01b4386186ab29d200d1a5a 100644
--- a/tests/spec/oracle/generalized_check.0.res.oracle
+++ b/tests/spec/oracle/generalized_check.0.res.oracle
@@ -1,24 +1,47 @@
-# frama-c -wp [...]
[kernel] Parsing tests/spec/generalized_check.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] tests/spec/generalized_check.i:30: Warning:
- Unsupported generalized invariant, use loop invariant instead.
- Ignored invariant
- check invariant \true;
-[wp] Warning: Missing RTE guards
-[wp] tests/spec/generalized_check.i:37: Warning:
- Missing assigns clause (assigns 'everything' instead)
-[wp] 11 goals scheduled
-[wp] [Qed] Goal typed_f_assigns : Valid
-[wp] [Failed] Goal typed_f_check_f_valid_ko
-[wp] [Qed] Goal typed_f_check_ensures_f_init_x : Valid
-[wp] [Failed] Goal typed_check_lemma_easy_proof
-[wp] [Qed] Goal typed_loop_loop_assigns : Valid
-[wp] [Failed] Goal typed_loop_check_implied_by_false_invariant
-[wp] [Failed] Goal typed_loop_check_loop_invariant_false_but_preserved_established
-[wp] [Failed] Goal typed_loop_check_loop_invariant_false_but_preserved_preserved
-[wp] [Failed] Goal typed_main_call_f_check_requires_f_valid_x
-[wp] [Failed] Goal typed_main_check_main_p_content_ko
-[wp] [Failed] Goal typed_main_check_main_valid_ko
-[wp] Proved goals: 3 / 11
- Qed: 3
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+
+[eva:alarm] tests/spec/generalized_check.i:23: Warning:
+ accessing uninitialized left-value. assert \initialized(&c);
+[eva] using specification for function f
+[eva:alarm] tests/spec/generalized_check.i:24: Warning:
+ function f: precondition 'f_valid_x' got status unknown.
+[eva] tests/spec/generalized_check.i:9: Warning:
+ no \from part for clause 'assigns *x;'
+[eva:alarm] tests/spec/generalized_check.i:25: Warning:
+ check 'main_valid_ko' got status unknown.
+[eva:alarm] tests/spec/generalized_check.i:26: Warning:
+ check 'main_p_content_ko' got status unknown.
+[eva:alarm] tests/spec/generalized_check.i:32: Warning:
+ loop invariant 'false_but_preserved' got status invalid.
+[eva] tests/spec/generalized_check.i:35: starting to merge loop iterations
+[eva:alarm] tests/spec/generalized_check.i:36: Warning:
+ check 'implied_by_false_invariant' got status invalid.
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function loop:
+ j ∈ {10}
+[eva:final-states] Values at end of function main:
+ a ∈ [--..--]
+ p ∈ {{ NULL ; &a }}
+ __retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 3 functions analyzed (out of 3): 100% coverage.
+ In these functions, 25 statements reached (out of 28): 89% coverage.
+ ----------------------------------------------------------------------------
+ Some errors and warnings have been raised during the analysis:
+ by the Eva analyzer: 0 errors 1 warning
+ by the Frama-C kernel: 0 errors 0 warnings
+ ----------------------------------------------------------------------------
+ 1 alarm generated by the analysis:
+ 1 access to uninitialized left-values
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 0 valid 2 unknown 2 invalid 4 total
+ Preconditions 0 valid 1 unknown 0 invalid 1 total
+ 0% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
diff --git a/tests/spec/oracle/generalized_check.1.res.oracle b/tests/spec/oracle/generalized_check.1.res.oracle
index f93e7228b403b708b01b4386186ab29d200d1a5a..dd870d5dc009e1cf2c1e19963f7f6d1bbae27bfb 100644
--- a/tests/spec/oracle/generalized_check.1.res.oracle
+++ b/tests/spec/oracle/generalized_check.1.res.oracle
@@ -1,47 +1,51 @@
[kernel] Parsing tests/spec/generalized_check.i (no preprocessing)
-[eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
-
-[eva:alarm] tests/spec/generalized_check.i:23: Warning:
- accessing uninitialized left-value. assert \initialized(&c);
-[eva] using specification for function f
-[eva:alarm] tests/spec/generalized_check.i:24: Warning:
- function f: precondition 'f_valid_x' got status unknown.
-[eva] tests/spec/generalized_check.i:9: Warning:
- no \from part for clause 'assigns *x;'
-[eva:alarm] tests/spec/generalized_check.i:25: Warning:
- check 'main_valid_ko' got status unknown.
-[eva:alarm] tests/spec/generalized_check.i:26: Warning:
- check 'main_p_content_ko' got status unknown.
-[eva:alarm] tests/spec/generalized_check.i:32: Warning:
- loop invariant 'false_but_preserved' got status invalid.
-[eva] tests/spec/generalized_check.i:35: starting to merge loop iterations
-[eva:alarm] tests/spec/generalized_check.i:36: Warning:
- check 'implied_by_false_invariant' got status invalid.
-[eva] done for function main
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function loop:
- j ∈ {10}
-[eva:final-states] Values at end of function main:
- a ∈ [--..--]
- p ∈ {{ NULL ; &a }}
- __retres ∈ {0}
-[eva:summary] ====== ANALYSIS SUMMARY ======
- ----------------------------------------------------------------------------
- 3 functions analyzed (out of 3): 100% coverage.
- In these functions, 25 statements reached (out of 28): 89% coverage.
- ----------------------------------------------------------------------------
- Some errors and warnings have been raised during the analysis:
- by the Eva analyzer: 0 errors 1 warning
- by the Frama-C kernel: 0 errors 0 warnings
- ----------------------------------------------------------------------------
- 1 alarm generated by the analysis:
- 1 access to uninitialized left-values
- ----------------------------------------------------------------------------
- Evaluation of the logical properties reached by the analysis:
- Assertions 0 valid 2 unknown 2 invalid 4 total
- Preconditions 0 valid 1 unknown 0 invalid 1 total
- 0% of the logical properties reached have been proven.
- ----------------------------------------------------------------------------
+/* Generated by Frama-C */
+/*@ check lemma easy_proof: \false;
+ */
+/*@ check requires f_valid_x: \valid(x);
+ check ensures f_init_x: *\old(x) ≡ 0;
+ assigns *x;
+ */
+void f(int *x)
+{
+ /*@ check f_valid_ko: \valid(x); */ ;
+ *x = 0;
+ return;
+}
+
+void loop(void);
+
+int main(void)
+{
+ int __retres;
+ int volatile c;
+ int a = 4;
+ int *p = (int *)0;
+ if (c) p = & a;
+ f(p);
+ /*@ check main_valid_ko: \valid(p); */ ;
+ /*@ check main_p_content_ko: *p ≡ 0; */ ;
+ loop();
+ __retres = 0;
+ return __retres;
+}
+
+void loop(void)
+{
+ int j = 0;
+ {
+ int i = 0;
+ /*@ check loop invariant false_but_preserved: j ≡ 10;
+ loop assigns i; */
+ while (i < 10) i ++;
+ }
+ /*@ check implied_by_false_invariant: j ≡ 10; */ ;
+ l: /*@ check invariant \true; */ ;
+ if (j >= 10) goto l1;
+ j ++;
+ goto l;
+ l1: ;
+ return;
+}
+
+
diff --git a/tests/spec/oracle/generalized_check.2.res.oracle b/tests/spec/oracle/generalized_check.2.res.oracle
deleted file mode 100644
index dd870d5dc009e1cf2c1e19963f7f6d1bbae27bfb..0000000000000000000000000000000000000000
--- a/tests/spec/oracle/generalized_check.2.res.oracle
+++ /dev/null
@@ -1,51 +0,0 @@
-[kernel] Parsing tests/spec/generalized_check.i (no preprocessing)
-/* Generated by Frama-C */
-/*@ check lemma easy_proof: \false;
- */
-/*@ check requires f_valid_x: \valid(x);
- check ensures f_init_x: *\old(x) ≡ 0;
- assigns *x;
- */
-void f(int *x)
-{
- /*@ check f_valid_ko: \valid(x); */ ;
- *x = 0;
- return;
-}
-
-void loop(void);
-
-int main(void)
-{
- int __retres;
- int volatile c;
- int a = 4;
- int *p = (int *)0;
- if (c) p = & a;
- f(p);
- /*@ check main_valid_ko: \valid(p); */ ;
- /*@ check main_p_content_ko: *p ≡ 0; */ ;
- loop();
- __retres = 0;
- return __retres;
-}
-
-void loop(void)
-{
- int j = 0;
- {
- int i = 0;
- /*@ check loop invariant false_but_preserved: j ≡ 10;
- loop assigns i; */
- while (i < 10) i ++;
- }
- /*@ check implied_by_false_invariant: j ≡ 10; */ ;
- l: /*@ check invariant \true; */ ;
- if (j >= 10) goto l1;
- j ++;
- goto l;
- l1: ;
- return;
-}
-
-
diff --git a/tests/syntax/cpp-command.c b/tests/syntax/cpp-command.c
index 8032aac2c727b39fde918c2e425095ad179846ad..3b58590a2b848a63236b09b0726c1579ed783d6e 100644
--- a/tests/syntax/cpp-command.c
+++ b/tests/syntax/cpp-command.c
@@ -1,8 +1,8 @@
/* run.config*
- FILTER: sed "s:/\(tmp\|var\|build\)/[^ ]*\.i:/tmp/FILE.i:g; s:$PWD/::"
+ FILTER: sed "s:/[^ ]*/cpp-command\.[^ ]*\.i:TMPDIR/FILE.i:g; s:$PWD/::"
OPT: -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "echo [\$(basename '%1') \$(basename '%1') \$(basename '%i') \$(basename '%input')] ['%2' '%2' '%o' '%output'] ['%args']"
OPT: -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "echo %%1 = \$(basename '%1') %%2 = '%2' %%args = '%args'"
- OPT: -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "printf \"%s\" \"using \\% has no effect : \$(basename \"\%input\")\""
+ OPT: -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "printf \"%s\n\" \"using \\% has no effect : \$(basename \"\%input\")\""
OPT: -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "echo %var is not an interpreted placeholder"
OPT: -no-autoload-plugins -print-cpp-commands
*/
diff --git a/tests/syntax/multiple_assigns.i b/tests/syntax/multiple_assigns.i
new file mode 100644
index 0000000000000000000000000000000000000000..d20a1dfcda46f0720ce70523677b4472dd709f80
--- /dev/null
+++ b/tests/syntax/multiple_assigns.i
@@ -0,0 +1,10 @@
+int z;
+
+/*@ assigns z, z;
+ assigns z \from z;
+ assigns z, z;
+ */
+void function(void)
+{
+ return;
+}
diff --git a/tests/syntax/multiple_froms.i b/tests/syntax/multiple_froms.i
new file mode 100644
index 0000000000000000000000000000000000000000..6a0a25687f9e2960e533cbec4ac5dbc0dc21e286
--- /dev/null
+++ b/tests/syntax/multiple_froms.i
@@ -0,0 +1,17 @@
+int a, b, c, d, e;
+
+// Reminder: assigns are visited in reverse
+
+/*@ assigns a;
+ assigns a \from a, a, b, c, c; // more precise so replace the next one
+ assigns a \from c, b, d, e, a;
+ assigns a;
+ assigns b \from a, e, b, d, c; // is ignored because the next one is more precise
+ assigns b \from a, e;
+ assigns c \from c, c, c, c, c; // both are kept (no inclusion)
+ assigns c \from d;
+ */
+void function(void)
+{
+ return;
+}
diff --git a/tests/syntax/oracle/cpp-command.0.res.oracle b/tests/syntax/oracle/cpp-command.0.res.oracle
index fc23c714129d2c32197c9503789ee598314cda8d..258383ae1d9324df215d1b7e536121dc85cb1df4 100644
--- a/tests/syntax/oracle/cpp-command.0.res.oracle
+++ b/tests/syntax/oracle/cpp-command.0.res.oracle
@@ -1,2 +1,2 @@
[kernel] Parsing tests/syntax/cpp-command.c (with preprocessing)
-[cpp-command.c cpp-command.c cpp-command.c cpp-command.c] [/tmp/FILE.i /tmp/FILE.i /tmp/FILE.i /tmp/FILE.i] [ -I./share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32]
+[cpp-command.c cpp-command.c cpp-command.c cpp-command.c] [TMPDIR/FILE.i TMPDIR/FILE.i TMPDIR/FILE.i TMPDIR/FILE.i] [ -I./share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32]
diff --git a/tests/syntax/oracle/cpp-command.1.res.oracle b/tests/syntax/oracle/cpp-command.1.res.oracle
index 77384bd05dea795728316f9424b13a64e67b57c6..c53f5fd858da79bc60cec61107394ce6282bd87d 100644
--- a/tests/syntax/oracle/cpp-command.1.res.oracle
+++ b/tests/syntax/oracle/cpp-command.1.res.oracle
@@ -1,2 +1,2 @@
[kernel] Parsing tests/syntax/cpp-command.c (with preprocessing)
-%1 = cpp-command.c %2 = /tmp/FILE.i %args = -I./share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32
+%1 = cpp-command.c %2 = TMPDIR/FILE.i %args = -I./share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32
diff --git a/tests/syntax/oracle/cpp-command.2.res.oracle b/tests/syntax/oracle/cpp-command.2.res.oracle
index 8a609225250a5c1f8b5a46a8847a8b7d09fb0df1..c56a2bbecb3f71ae5f1ef92ba4105dc539e3bc2a 100644
--- a/tests/syntax/oracle/cpp-command.2.res.oracle
+++ b/tests/syntax/oracle/cpp-command.2.res.oracle
@@ -1,2 +1,2 @@
[kernel] Parsing tests/syntax/cpp-command.c (with preprocessing)
-using \% has no effect : cpp-command.c'
\ No newline at end of file
+using \% has no effect : cpp-command.c'
diff --git a/tests/syntax/oracle/cpp-command.4.res.oracle b/tests/syntax/oracle/cpp-command.4.res.oracle
index bce7863f91059c3146bb69d762b5317a1cc86cea..db826509fc1ab6b600f12a1f0c7e9964e6f6aefa 100644
--- a/tests/syntax/oracle/cpp-command.4.res.oracle
+++ b/tests/syntax/oracle/cpp-command.4.res.oracle
@@ -1,2 +1,2 @@
[kernel] Preprocessing command:
- gcc -E -C -I. -I./share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32 'tests/syntax/cpp-command.c' -o '/tmp/FILE.i'
+ gcc -E -C -I. -I./share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32 'tests/syntax/cpp-command.c' -o 'TMPDIR/FILE.i'
diff --git a/tests/syntax/oracle/multiple_assigns.res.oracle b/tests/syntax/oracle/multiple_assigns.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..0cda603d543618256b3d8bc527983157bf1538ed
--- /dev/null
+++ b/tests/syntax/oracle/multiple_assigns.res.oracle
@@ -0,0 +1,11 @@
+[kernel] Parsing tests/syntax/multiple_assigns.i (no preprocessing)
+/* Generated by Frama-C */
+int z;
+/*@ assigns z;
+ assigns z \from z; */
+void function(void)
+{
+ return;
+}
+
+
diff --git a/tests/syntax/oracle/multiple_froms.res.oracle b/tests/syntax/oracle/multiple_froms.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..b90f4dc55f6e2c31b6f7656f8f8cc0ecfa6cf03d
--- /dev/null
+++ b/tests/syntax/oracle/multiple_froms.res.oracle
@@ -0,0 +1,23 @@
+[kernel] Parsing tests/syntax/multiple_froms.i (no preprocessing)
+[kernel:annot:multi-from] Warning:
+ Drop 'b' \from at tests/syntax/multiple_froms.i:9 for more precise one at tests/syntax/multiple_froms.i:10
+[kernel:annot:multi-from] Warning:
+ Drop 'a' \from at tests/syntax/multiple_froms.i:7 for more precise one at tests/syntax/multiple_froms.i:6
+/* Generated by Frama-C */
+int a;
+int b;
+int c;
+int d;
+int e;
+/*@ assigns a, b, c;
+ assigns a \from a, b, c;
+ assigns b \from a, e;
+ assigns c \from c;
+ assigns c \from d;
+ */
+void function(void)
+{
+ return;
+}
+
+