diff --git a/src/plugins/e-acsl/.gitignore b/src/plugins/e-acsl/.gitignore
index 5660f5616e42f642d962af21324bd1963a59b467..75d11316c614844c36c6193fd864d1a6175b8938 100644
--- a/src/plugins/e-acsl/.gitignore
+++ b/src/plugins/e-acsl/.gitignore
@@ -73,6 +73,5 @@ top/
doc/doxygen/doxygen.cfg
doc/doxygen/html
doc/doxygen/warn.log
-benchmarking/tools/fc-time
lib/libgmp-e-acsl.a
lib/libjemalloc-e-acsl.a
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 3304fb156df2159ced2cce9204ab31280f6c5880..b9f74b3d5b7b2ec3f2315a6b4d015fb3925c4c0d 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -77,19 +77,8 @@ PLUGIN_DISTRIB_BIN:=no
###############
# Local Flags #
###############
-
-# Enable -warn-error in development mode, but not in distribution mode
# Do not edit the line below: it is automatically set by 'make e-acsl-distrib'
IS_DISTRIBUTED:=no
-ifneq ($(IS_DISTRIBUTED),yes)
-ifeq ($(EACSL_HAS_OCAML312),yes)
-EACSL_DEV_FLAGS=-warn-error +a
-else
-EACSL_DEV_FLAGS=-warn-error A
-endif
-endif
-PLUGIN_BFLAGS:=$(EACSL_DEV_FLAGS)
-PLUGIN_OFLAGS:=$(EACSL_DEV_FLAGS)
#######################
# Local configuration #
@@ -129,25 +118,6 @@ clean::
endif
-######################
-# Benchmarking tools #
-######################
-
-EACSL_BM_SOURCES = $(wildcard $(PLUGIN_DIR)/benchmarking/tools/*.c)
-EACSL_BM_BINARIES = $(patsubst %.c,%, $(EACSL_BM_SOURCES))
-
-CFLAGS = -g3 -O2 -std=c11 -pedantic -Wall -Wno-unused-result
-
-$(EACSL_BM_BINARIES): % : %.c
- $(PRINT_CC) $@
- $(CC) $(CFLAGS) -o $@ $^
-
-all:: $(EACSL_BM_BINARIES)
-
-clean::
- $(PRINT_RM) benchmarking tools
- $(RM) $(EACSL_BM_BINARIES)
-
################################################
# E-ACSL C Libs: libjemalloc, libgmp #
################################################
diff --git a/src/plugins/e-acsl/benchmarking/examples/plotting/dat/barplot.dat b/src/plugins/e-acsl/benchmarking/examples/plotting/dat/barplot.dat
deleted file mode 100644
index 725d4337c6b42ce4b561875ef24fc4ba47802600..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/benchmarking/examples/plotting/dat/barplot.dat
+++ /dev/null
@@ -1,4 +0,0 @@
-Benchmark No-model Segment-model Bittree-model
-grep 2 4.4 18
-sed 3 9 16
-diff 4 9.3 7.3
diff --git a/src/plugins/e-acsl/benchmarking/examples/plotting/dat/lineplot.dat b/src/plugins/e-acsl/benchmarking/examples/plotting/dat/lineplot.dat
deleted file mode 100644
index c8851c9a5beff4d6885904e4ed60fc73ef1e1865..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/benchmarking/examples/plotting/dat/lineplot.dat
+++ /dev/null
@@ -1,11 +0,0 @@
-RUNS No-model Segment-model Bittree-model
-1 1.1 4.6 8.6
-2 2.3 9.2 13.8
-3 1.0 9.9 11.2
-4 1.9 4.3 6.9
-5 3.4 6.9 12.5
-6 5.4 20.4 33.4
-7 8.1 21.8 36.7
-8 11.6 23.7 16.2
-9 16.6 40.8 22.7
-10 1.15 7.4 8.1
diff --git a/src/plugins/e-acsl/benchmarking/examples/plotting/sample-plot.sh b/src/plugins/e-acsl/benchmarking/examples/plotting/sample-plot.sh
deleted file mode 100755
index 56f3dd52eb0e386769462deda79ce8b25a849cce..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/benchmarking/examples/plotting/sample-plot.sh
+++ /dev/null
@@ -1,32 +0,0 @@
-#!/bin/sh
-
-# Sample script showing usage of `bm.gnuplot` script
-
-# Path to gnuplot script
-BM_GNUPLOT="../../tools/bm.gnuplot"
-
-# Build a line plot using lineplot.dat data file
-gnuplot \
- -e "BaseFile='dat/lineplot'" \
- -e "Style='lines'" \
- -e "WithOverheads=1" \
- -e "PlotTitle='Sample line plot title'" \
- -e "XLabel='Sample line plot label of X axis'" \
- -e "YLabel='Sample line plot label of Y axis'" \
- -e "OutputDir='.'" \
- -e "WithOverheads='1'" \
- $BM_GNUPLOT
-
-# Build a histogram using barplot.dat data file
-gnuplot \
- -e "BaseFile='dat/barplot'" \
- -e "Style='histogram'" \
- -e "WithOverheads=1" \
- -e "PlotTitle='Sample histogram title'" \
- -e "XLabel='Sample histogram label of X axis'" \
- -e "YLabel='Sample histogram label of Y axis'" \
- -e "OutputDir='.'" \
- -e "WithOverheads='1'" \
- $BM_GNUPLOT
-
-exit 0
diff --git a/src/plugins/e-acsl/benchmarking/tools/bm.gnuplot b/src/plugins/e-acsl/benchmarking/tools/bm.gnuplot
deleted file mode 100755
index 59fce6cb7f7bbf8a87018cd4358c994ca07d2080..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/benchmarking/tools/bm.gnuplot
+++ /dev/null
@@ -1,180 +0,0 @@
-#!/usr/bin/env gnuplot
-
-##########################################################################
-# #
-# This file is part of the Frama-C's E-ACSL plug-in. #
-# #
-# Copyright (C) 2012-2016 #
-# CEA (Commissariat à l'énergie atomique et aux énergies #
-# alternatives) #
-# #
-# you can redistribute it and/or modify it under the terms of the GNU #
-# Lesser General Public License as published by the Free Software #
-# Foundation, version 2.1. #
-# #
-# It is distributed in the hope that it will be useful, #
-# but WITHOUT ANY WARRANTY; without even the implied warranty of #
-# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
-# GNU Lesser General Public License for more details. #
-# #
-# See the GNU Lesser General Public License version 2.1 #
-# for more details (enclosed in the file license/LGPLv2.1). #
-# #
-##########################################################################
-
-# Usage information of a script
-#
-# Gnuplot script for building line graphs and histograps
-#
-# The script should be invoked as follows:
-# gnuplot \
-# -e "BaseFile='<Base name of .dat file>' \
-# -e "Style='<lines|histogram>' \
-# -e "PlotTitle='<Optional: Plot title: [BaseFile]>'"
-# -e "XLabel='<Optional: X-axis label: [""]>'"
-# -e "YLabel='<Optional: Y-axis label: ["1st column title"]>'"
-# -e "OutputDir='<Optional: directory where to place output files>'"
-# -e "WithOverheads='<ANY>'"
-# data.plot
-#
-# Arguments:
-# - BaseName - base name of a data file with data to plot. This script expects
-# BaseName.dat to exist and contain data. E.g., if the provided value is
-# 'foo/bar', then foo/bar.dat file should exist
-# - Style - a compulsory argument indicating the type of a plot to be constructed.
-# Allowed values are 'histogram' or 'lines'. If 'lines' value is given then
-# this script builds a line plot expecting the data file be of the form:
-# YLabel XLabel1 XLabel2 ...
-# YValue XValue1 XValue2 ...
-# ...
-# If 'histogram' argument is specified a data file is expected to be of the form:
-# GroupLabel Label2 Label3 Label4
-# Group1 Value1 Value2 Value3 ...
-# Group2 Value1 Value2 Value3 ...
-# ...
-# - XLabel - optional string used a X-axis label
-# - YLabel - optional string used a Y-axis label
-# - PlotTitle - optional string used a plot title
-# - OutputDir - optional directory for placement of resulting pdf files
-# - WithOverheads - if any value is given to this argument then the script
-# computes overheads relative to the values in the second column
-
-# Check if a given file exists
-file_exists(file) = system("test -f '".file."' && echo '1' || echo '0'") + 0
-
-if (exists("Style") && (Style eq "histogram" && Style eq "lines")) {
- print "ERROR: Unknown histogram style [histogram|lines]"
- print "See inline comments for details"
- exit 1
-}
-
-# Check if the base name of the datafile (name - extension .dat)
-# is given via commandline
-if (!exists("BaseFile")) {
- print "ERROR: Variable 'BaseFile' should be set via commandline"
- print "See inline comments for details"
- exit
-}
-
-# Set datafile name
-DataFile = BaseFile.'.dat'
-
-# Check if it exists
-if (!file_exists(DataFile)) {
- print "ERROR: ".DataFile." not found."
- print "See inline comments for details"
- exit
-}
-
-# Unless specified the plot title is named after the base name of the file
-if (!exists("PlotTitle"))
- PlotTitle = BaseFile
-# Unless specified the Y axis label is the leftmost column header
-if (!exists("YLabel"))
- YLabel = word(system(sprintf("head -n 1 %s", DataFile)),1)
-# Unless specified Y label is empty
-if (!exists("XLabel"))
- XLabel = ""
-
-# Fonts and background
-Background = '#F7F7F7'
-BaseFont = 'Arial,14'
-TicsFont = "Arial,10"
-LegendFont = "Arial,12"
-SideLabelFont = "Arial-Bold,16"
-
-# Line colours
-set linetype 6 linewidth 2 linecolor rgb "#666633" pointtype 6 pointsize 0.7 # Dark yellow
-set linetype 5 linewidth 2 linecolor rgb "#006633" pointtype 5 pointsize 0.7 # Green
-set linetype 4 linewidth 2 linecolor rgb "#000000" pointtype 4 pointsize 0.7 # Black
-set linetype 3 linewidth 2 linecolor rgb "#990099" pointtype 3 pointsize 0.7 # Magenta
-set linetype 2 linewidth 2 linecolor rgb "#000066" pointtype 8 pointsize 0.7 # Dark blue
-set linetype 1 linewidth 2 linecolor rgb "#990000" pointtype 7 pointsize 0.7 # Maroon
-
-# Use the postscript terminal, as a PDF one is not fully featured
-set terminal postscript landscape size 10,7 enhanced color font BaseFont
-
-# Set background colour for the plot area
-set object 1 rectangle from graph 0, graph 0 to graph 1, graph 1 behind fc rgbcolor Background fs noborder
-
-# Set font for ticks and make them appear outside
-# nomirror removes x2ticks and y2ticks (top and right)
-set ytics font TicsFont out nomirror
-set xtics font TicsFont out nomirror
-
-set autoscale
-
-# Legend font
-set key on horizontal font LegendFont
-
-# PlotTitle variable should come from environment via -e
-set title PlotTitle
-
-# Enable fonts for side labels
-set xlabel XLabel font SideLabelFont
-set ylabel YLabel font SideLabelFont
-
-# Enable macros
-set macros
-
-PsFile = BaseFile.'.ps'
-PdfFile = BaseFile.'.pdf'
-
-if (exists("OutputDir")) {
- PsFile = OutputDir."/".system("basename ".DataFile)
- PdfFile = OutputDir."/".system("basename ".PdfFile)
-}
-
-Columns=`tail -n 1 @DataFile | wc -w`
-
-# Set output file command
-set output PsFile
-
-# Overhead plotting function
-# nat - time of an original executable
-# mod -= time of the modified executable
-# If WithOverheads var is defined then compute overheads, otherwise plot as is
-ovh(nat, mod) = exists("WithOverheads") ? mod/nat : mod
-
-###################
-# Plotting
-###################
-# Build a line plot
-if (Style eq "lines") {
- plot for [COL = 2:Columns] DataFile \
- using 1:(ovh(column(2), column(COL))) title columnheader(COL) with linespoints
-}
-
-# Build a histogram
-if (Style eq "histogram") {
- set yrange [0:]
- set style data histogram
- set style fill solid border -1
- plot for [COL=2:Columns] DataFile using (ovh(column(2), column(COL))):xticlabels(1) title columnheader
-}
-
-# At this point postscript is generated, create PDF
-!ps2pdf @PsFile @PdfFile
-!rm @PsFile
-
-
diff --git a/src/plugins/e-acsl/benchmarking/tools/fc-time.c b/src/plugins/e-acsl/benchmarking/tools/fc-time.c
deleted file mode 100644
index 4aa78abe3ff66ffcddf642722e97584ca795e766..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/benchmarking/tools/fc-time.c
+++ /dev/null
@@ -1,467 +0,0 @@
-/* Copyright (C) 1990, 91, 92, 93, 96 Free Software Foundation, Inc.
- *
- * This program is free software; you can redistribute it and/or modify
- * it under the terms of the GNU General Public License as published by
- * the Free Software Foundation; either version 2, or (at your option)
- * any later version.
- *
- * This program is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with this program; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
- * 02111-1307, USA. */
-
-/* fc-time -- mesaure real time of an executed command */
-
-#include <stdlib.h>
-#include <string.h>
-#include <stdio.h>
-#include <unistd.h>
-#include <stdarg.h>
-#include <errno.h>
-#include <getopt.h>
-#include <signal.h>
-#include <sys/wait.h>
-#include <sys/time.h>
-#include <sys/types.h>
-#include <sys/resource.h>
-
-/* Extra declarations to suppress warnings in -std=c99 or -std=c11 modes */
-int kill(pid_t pid, int sig);
-
-const char *strdup(const char *s);
-
-pid_t wait4(pid_t pid, int *status, int options, struct rusage *rusage);
-
-typedef void (*sighandler_t) (int);
-
-#ifdef __linux__
-#include <linux/limits.h>
-#endif
-
-/* Minimal reported runtime */
-#define MINTIME 0.001
-
-/* Minimal time limit after which a program is forcibly terminated */
-#define MINLIMIT 0.1
-
-/* Name of the output file. Only used if -o option is given. */
-static const char *outfile;
-
-/* Output stream, defaults to stderr */
-static FILE *outfp;
-
-/* If true, append to `outfile' rather than truncating it */
-static int append;
-
-/* Program name */
-static const char * program_name = NULL;
-
-/* Time limit in seconds */
-long double time_limit = 0;
-
-/* Verbosity level */
-int verbose;
-
-/* Gather memory stats via /proc/[pid]/statm */
-int memory;
-
-/* Struct for holding the results of memory statistics */
-struct statistics {
- unsigned long vsize; /* (1) total program size (page size) */
- unsigned long rss; /* (2) resident set size (page size) */
- unsigned long share; /* (3) shared pages (page size) */
- unsigned long text; /* (4) text (page size) */
- unsigned long lib; /* (5) library (page size) */
- unsigned long data; /* (6) data + stack (page size) */
-
- /* The number of times a procfile has been read */
- unsigned long count;
- int status; /* exit status */
-
- struct timeval start; /* timestamp of program start */
- struct timeval finish; /* timestamp of program end */
- struct rusage resusage; /* struct for use with getrusage */
-};
-
-/* Name of the used memory stat file */
-char procfile [PATH_MAX];
-
-/* Memory stat file stream */
-FILE *procfp = NULL;
-
-/* Default report format string */
-char *report_format = "%e\n";
-
-/* Memory size units */
-#define B_SZ 1
-#define KB_SZ 1024
-#define MB_SZ (1024*KB_SZ)
-#define GB_SZ (1024*MB_SZ)
-
-/* Reported block unit */
-static int block_size;
-
-/* Short options */
-static const char *shortopts = "+ao:l:vmB:f:";
-
-/* Long options */
-static struct option longopts[] = {
- {"limit", required_argument, NULL, 'l'},
- {"verbose", no_argument, NULL, 'v'},
- {"append", no_argument, NULL, 'a'},
- {"help", no_argument, NULL, 'h'},
- {"output-file", required_argument, NULL, 'o'},
- {"memory", required_argument, NULL, 'm'},
- {"block-bize", required_argument, NULL, 'B'},
- {"format", required_argument, NULL, 'f'},
- {NULL, no_argument, NULL, 0}
-};
-
-/* Print help page and exit */
-static void usage (FILE *stream, int status) {
- fprintf(stream,
-"NAME:\n"
-" fc-time -- measure execution time and/or memory consumption of a command\n"
-"SYNOPSIS:\n"
-" fc-time [options] command [arg...]\n"
-"OPTIONS:\n"
-" -h, --help print this help page and exit.\n"
-" -o FILE send output to a named file [stderr].\n"
-" -a, --append append an output file without truncating it (with -o).\n"
-" -l SECONDS limit in seconds arter which a program is terminated\n"
-" even if it is not finshed. The limit needs to be specified with seconds\n"
-" precision.\n"
-" -m, --memory - collect memory statistics [disabled].\n"
-" -v warn if a program has been terminated via -l option.\n"
-" -f printf-like report format string.\n"
-" %%e - elapsed real time [seconds:milliseconds].\n"
-" %%E - same as %%e\n"
-" %%U - total time spent in user mode [seconds:milliseconds].\n"
-" %%S - total time spent in kernel mode [seconds:milliseconds].\n"
-" %%v - virtual memory consumption peak [bytes].\n"
-" %%t - text segment size [bytes].\n"
-" %%d - data + stack segments sizes [bytes].\n"
-" %%r - maximum resident set size [bytes].\n"
-" Memory-related measurements (e.g., virtual memory consumption or rss)\n"
-" are disabled by default. Unless -m option is used they are reported as\n"
-" zeroes. Computing memory peaks may result in the increase of runtime.\n"
-" -B, --byte-size=<B|KB|MB|GB> - change reported memory unit [B].\n");
- exit(status);
-}
-
-/* Error reporting function. Replica of the GNU error (3).
- * Added for portability purposes. */
-static void error(int status, int errnum, const char *format, ...) {
- fflush(stderr); /* Flush streams */
- fflush(stdout);
-
- if (program_name) /* Report program name */
- fprintf(stderr, "%s: ", program_name);
-
- va_list va; /* Pass the error message given by the user */
- va_start(va, format);
- vfprintf(stderr, format, va);
- va_end(va);
-
- if (errnum) /* Report error given via errno */
- fprintf(stderr, ": %s", strerror(errnum));
-
- /* Add the newline at the end */
- fprintf(stderr, "\n");
-
- /* Exit if status is a non-zero */
- if (status)
- exit(status);
-}
-
-#define warning(_fmt, ...) \
- if (verbose) { \
- error(0, 0, _fmt, __VA_ARGS__); \
- }
-
-/* Initialize the options and parse the command line arguments.
- Also note the position in ARGV where the command to time starts. */
-static const char ** getargs (int argc, char **argv) {
- int optc;
- outfile = NULL;
- outfp = stderr; /* Output to stderr by default */
- append = 0;
- verbose = 0;
- memory = 0;
- block_size = KB_SZ;
-
- while ((optc = getopt_long(argc, argv, shortopts, longopts, NULL)) != EOF) {
- switch (optc) {
- case 'a':
- append = 1;
- break;
- case 'h':
- usage (stdout, 0);
- case 'o':
- outfile = optarg;
- break;
- case 'v':
- verbose = 1;
- break;
- case 'm':
- memory = 1;
- break;
- case 'f':
- report_format = (char*)strdup(optarg);
- break;
- case 'l':
- /* Convert time limit to seconds */
- time_limit = strtold(optarg, NULL);
-
- /* Abort if the time limit provided at input is invalid or less than
- the threshold given by MINLIMIT */
- if (time_limit < MINLIMIT)
- error(1, errno, "Bad time limit specification: '%s'."
- " Expected positive number greater than %0.3f", optarg, MINLIMIT);
- /* Detect over- or underflow */
- if (errno == ERANGE)
- error(1, errno, "%s", optarg);
- break;
- case 'B': { /* reported unit size */
- switch(optarg[0]) {
- case 'B': /* report memory in bytes */
- block_size = B_SZ;
- break;
- case 'K': /* ... kilobytes */
- block_size = KB_SZ;
- break;
- case 'M': /* ... megabytes */
- block_size = MB_SZ;
- break;
- case 'G': /* ... gigabytes */
- block_size = GB_SZ;
- break;
- default:
- error(1, 0, "Bad block size specification (%s), expected B,K,M or G", optarg);
- }
- break;
- }
- default:
- usage (stderr, 1);
- }
- }
-
- if (optind == argc)
- usage (stderr, 1);
-
- if (outfile) {
- if (append)
- outfp = fopen (outfile, "a");
- else
- outfp = fopen (outfile, "w");
- if (outfp == NULL)
- error(1, errno, "%s", outfile);
- }
- return (const char **) &argv[optind];
-}
-
-/* Convert timeval into a double with millisecond precision */
-#define TIMEWMS(_tval) (_tval.tv_sec + (_tval.tv_usec/1000000.0))
-#define TIMEDIFF(_finish,_start) (TIMEWMS(_finish) - TIMEWMS(_start))
-
-/* Assign the max of _old and _new to _old */
-#define assignmax(_old, _new) _old = (_old > _new) ? _old : _new
-
-/* Observe the child's execution, collect memory stats and terminate the
- * execution if the time limit is exceeded
- *
- * - This function is invoked only if either `time_limit' or `memory'
- * are specified, i.e., a user requests either to collect memory stats
- * or terminate the execution upon exceeding some time limit.
- *
- * - For the case when a time limit is given but memory statistics do not
- * need to be collected the parent process checks if the time limit is
- * exceeded each second. This is to limit the interference
- *
- * - If memory stats are collected, then checking time limit and reading
- * procfile is done in a cycle without sleeping periods. This may slightly
- * extend the execution of the program
-*/
-int observe(pid_t chpid, struct statistics * stats) {
- int status;
- pid_t rpid;
-
- while (!(rpid = wait4(chpid, &status, WNOHANG, &stats->resusage))) {
- gettimeofday(&stats->finish, NULL);
- if (time_limit && TIMEDIFF(stats->finish, stats->start) > time_limit) {
- warning("Warning: Attempting graceful termination due exceeded time "
- "limit of %0.2Lf seconds", "", time_limit);
- kill(chpid, SIGTERM);
- break;
- } else {
- /* No mem stats need to be collected, sleep for one second */
- if (!memory) {
- sleep(1);
- /* Mem stats need to be collected */
- } else {
- unsigned long vsize, rss, share, text, lib, data;
- /* Open and read process file */
- procfp = fopen(procfile, "r");
- if (!procfp)
- error(1, errno, "cannot open process memory stat file %s", procfile);
- fscanf(procfp, "%lu %lu %lu %lu %lu %lu",
- &vsize, &rss, &share, &text, &lib, &data);
- assignmax(stats->vsize, vsize);
- assignmax(stats->rss, rss);
- assignmax(stats->share, share);
- assignmax(stats->text, text);
- assignmax(stats->lib, lib);
- assignmax(stats->data, data);
- fclose(procfp);
- stats->count++;
- }
- }
- }
-
- if (rpid == -1)
- return 0;
- return 1;
-}
-
-/* Run command and return statistics on it. */
-static int run_command (const char ** cmd) {
- pid_t pid = 0; /* Pid of child */
- int status = 0; /* Status of a child */
- sighandler_t interrupt_signal, quit_signal;
-
- struct statistics stats;
- memset(&stats, 0, sizeof(struct statistics));
-
- /* Fork the child process */
- pid = fork();
-
- /* Copy the name of the stat file to the `procfile` global */
- sprintf(procfile, "/proc/%d/statm", pid);
-
- /* Start measuring real time */
- gettimeofday(&stats.start, NULL);
-
- if (pid < 0) {
- error(1, errno, "cannot fork");
- } else if (pid == 0) { /* If child. */
- execvp(cmd[0], (char *const*) cmd);
- error(0, errno, "cannot run %s", cmd[0]);
- exit(errno == ENOENT ? 127 : 126);
- }
-
- /* Have signals kill the child but not self */
- interrupt_signal = signal(SIGINT, SIG_IGN);
- quit_signal = signal(SIGQUIT, SIG_IGN);
-
- /* Time limit has been specified. Observe execution of the child process
- * and terminate the program after the time limit has been exceeded. */
- if (time_limit || memory) {
- if (observe(pid, &stats) == 0)
- error(1, errno, "error waiting for child process");
- /* No time limit given. Run the program as is and compute the runtime after
- * the process terminates. */
- } else {
- pid_t rpid = wait4(pid, &status, 0, &stats.resusage);
- gettimeofday(&stats.finish, NULL);
- if (rpid == -1)
- error (1, errno, "error waiting for child process");
- }
-
- /* Re-enable signals. */
- signal(SIGINT, interrupt_signal);
- signal(SIGQUIT, quit_signal);
-
- /* Format string for report */
- char *fmt = report_format;
-
- /* Page size (/proc/[pid]/statm) reports sizes in pages */
- long pagesz = sysconf(_SC_PAGESIZE);
-
- while(*fmt != '\0') {
- switch(*fmt) {
- case '%': {
- fmt++;
- switch (*fmt) {
- /* Elapsed time with millisecond precition */
- case 'E':
- case 'e': {
- double elapsed = TIMEWMS(stats.finish) - TIMEWMS(stats.start);
- fprintf(outfp, "%0.3f", (elapsed > MINTIME) ? elapsed : MINTIME);
- break;
- }
- /* Time spent in kernel mode */
- case 'S':
- fprintf(outfp, "%0.3f", TIMEWMS(stats.resusage.ru_stime));
- break;
- /* Time spent in user mode */
- case 'U':
- fprintf(outfp, "%0.3f", TIMEWMS(stats.resusage.ru_utime));
- break;
- case 'v':
- fprintf(outfp, "%lu", (stats.vsize*pagesz)/block_size);
- break;
- case 'd':
- fprintf(outfp, "%lu", (stats.data*pagesz)/block_size);
- break;
- case 't':
- fprintf(outfp, "%lu", (stats.text*pagesz)/block_size);
- break;
- case 'r':
- fprintf(outfp, "%lu", (stats.rss*pagesz)/block_size);
- break;
- default:
- fprintf(outfp, "???");
- break;
- }
- break;
- }
- case '\\': {
- fmt++;
- switch (*fmt) {
- case 't':
- putc ('\t', outfp);
- break;
- case 'n':
- putc ('\n', outfp);
- break;
- case '\\':
- putc ('\\', outfp);
- break;
- default:
- putc ('?', outfp);
- putc ('\\', outfp);
- putc (*fmt, outfp);
- }
- break;
- }
- default: {
- putc (*fmt, outfp);
- }
- }
- fmt++;
- }
-
- fflush(outfp);
- /* ... and return the status of the child */
- return status;
-}
-
-int main (int argc, char **argv) {
- program_name = *argv;
- const char **command_line = getargs(argc, argv);
- int status = run_command(command_line);
-
- /* Examining exit status of wait */
- if (WIFSTOPPED(status))
- exit(WSTOPSIG(status));
- else if (WIFSIGNALED(status))
- exit(WTERMSIG(status));
- else if (WIFEXITED(status))
- exit(WEXITSTATUS(status));
- return 0;
-}
diff --git a/src/plugins/e-acsl/configure.ac b/src/plugins/e-acsl/configure.ac
index 29b1bdd3392aa58e00710e5168dd389d09dd17d8..c1f310d918f3f38887caef4b16997e63bff11c48 100644
--- a/src/plugins/e-acsl/configure.ac
+++ b/src/plugins/e-acsl/configure.ac
@@ -123,15 +123,20 @@ write_plugin_config(Makefile)
###############################
# Configure contrib libraries #
###############################
+
+m4_ifndef([plugin_dir], [
+ m4_define([plugin_dir],[./])
+])
+
# Configure libgmp
if test "$FULL_GMP" = yes; then
AC_MSG_NOTICE([Configure libgmp])
- (cd contrib/libgmp && ./configure)
+ (cd plugin_dir/contrib/libgmp && ./configure)
fi
# Configure libjemalloc
AC_MSG_NOTICE([Configure libjemalloc])
-(cd contrib/libjemalloc && ./autogen.sh \
+(cd plugin_dir/contrib/libjemalloc && ./autogen.sh \
--with-jemalloc-prefix="__e_acsl_native_" \
--with-private-namespace="__e_acsl_hidden_" \
--with-install-suffix="-e-acsl")
diff --git a/src/plugins/e-acsl/env.ml b/src/plugins/e-acsl/env.ml
index 8f6beb3ef83fa07f053ce42629c7a924709ac385..7224d5519e39957161ade8c2d5719d564b076592 100644
--- a/src/plugins/e-acsl/env.ml
+++ b/src/plugins/e-acsl/env.ml
@@ -277,7 +277,7 @@ module Logic_binding = struct
| Ltype _ as ty when Logic_const.is_boolean_type ty -> Cil.charType
| Ltype _ | Lvar _ | Lreal | Larrow _ as lty ->
let msg =
- Pretty_utils.sfprintf
+ Format.asprintf
"logic variable of type %a" Logic_type.pretty lty
in
Error.not_yet msg
diff --git a/src/plugins/e-acsl/main.ml b/src/plugins/e-acsl/main.ml
index b1c35e90567872a1dc4f3ac1cbc422770cb2ea81..a3871f06a64cd2914f885513318126cbdc97f8e3 100644
--- a/src/plugins/e-acsl/main.ml
+++ b/src/plugins/e-acsl/main.ml
@@ -54,7 +54,7 @@ let unmemoized_extend_ast () =
let share = Options.Share.dir ~error:true () in
Options.feedback ~level:3 "setting kernel options for E-ACSL.";
Kernel.CppExtraArgs.add
- (Pretty_utils.sfprintf " -DE_ACSL_MACHDEP=%s -I%s/memory_model"
+ (Format.asprintf " -DE_ACSL_MACHDEP=%s -I%s/memory_model"
(Kernel.Machdep.get ())
share);
Kernel.Keep_unused_specified_functions.off ();
@@ -64,7 +64,7 @@ let unmemoized_extend_ast () =
(File.NeedCPP
(s,
ppc
- ^ Pretty_utils.sfprintf " -I%s" share,
+ ^ Format.asprintf " -I%s" share,
ppk))
in
List.iter register (Misc.library_files ())
@@ -89,7 +89,7 @@ E-ACSL is going to work on a copy.";
Project.create_by_copy
~last:false
~selection
- (Pretty_utils.sfprintf "%s for E-ACSL" name)
+ (Format.asprintf "%s for E-ACSL" name)
in
Project.on prj
(fun () ->
diff --git a/src/plugins/e-acsl/misc.ml b/src/plugins/e-acsl/misc.ml
index e02584848d7edb79a7311bdf6f7ac552eb075bf7..70fff43f9fca3e5a348b482df02ea88033a4521f 100644
--- a/src/plugins/e-acsl/misc.ml
+++ b/src/plugins/e-acsl/misc.ml
@@ -146,7 +146,7 @@ let mk_e_acsl_guard ?(reverse=false) kind kf e p =
let loc = p.pred_loc in
let msg =
Kernel.Unicode.without_unicode
- (Pretty_utils.sfprintf "%a@?" Printer.pp_predicate) p
+ (Format.asprintf "%a@?" Printer.pp_predicate) p
in
let line = (fst loc).Lexing.pos_lnum in
let e =
diff --git a/src/plugins/e-acsl/quantif.ml b/src/plugins/e-acsl/quantif.ml
index c6140bbc1fafb5b39571dff2e54af521abaa3994..f26cb8fa5f1069e757cab8767ebfc5a128e5970f 100644
--- a/src/plugins/e-acsl/quantif.ml
+++ b/src/plugins/e-acsl/quantif.ml
@@ -34,9 +34,9 @@ let term_to_exp_ref
let compute_quantif_guards quantif bounded_vars hyps =
let error msg pp x =
- let msg1 = Pretty_utils.sfprintf msg pp x in
+ let msg1 = Format.asprintf msg pp x in
let msg2 =
- Pretty_utils.sfprintf "@[ in quantification@ %a@]"
+ Format.asprintf "@[ in quantification@ %a@]"
Printer.pp_predicate quantif
in
Error.untypable (msg1 ^ msg2)
@@ -93,7 +93,7 @@ let compute_quantif_guards quantif bounded_vars hyps =
| [] -> ()
| _ :: _ ->
let msg =
- Pretty_utils.sfprintf
+ Format.asprintf
"@[unguarded variable%s %tin quantification@ %a@]"
(if List.length vars = 1 then "" else "s")
(fun fmt ->
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index c5e3bb3ad05178a0f9e02e590387bf24e344938f..b06878b47bf9ef1ef341dd449c669671c0d5ba35 100755
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
@@ -311,7 +311,7 @@ do
# Do use Frama-C stdlib, which is the default behaviour of Frama-C
--frama-c-stdlib|-L)
shift;
- OPTION_FRAMA_STDLIB=""
+ OPTION_FRAMA_STDLIB="-frama-c-stdlib"
;;
# Use as much memory-related instrumentation as possible
-M|--full-mmodel)
@@ -427,11 +427,7 @@ GCCMACHDEP="-m$MACHDEPFLAGS"
EACSL_MACRO_ID="__E_ACSL__"
# Frama-C and related flags
-FRAMAC_CPP_EXTRA="
- $OPTION_FRAMAC_CPP_EXTRA
- -D$EACSL_MACRO_ID
- -I$FRAMAC_SHARE/libc
- $CPPMACHDEP"
+FRAMAC_CPP_EXTRA="$OPTION_FRAMAC_CPP_EXTRA $CPPMACHDEP"
EACSL_MMODEL="$OPTION_EACSL_MMODEL"
# Re-set EACSL_SHARE directory is it has been given by the user
@@ -481,7 +477,7 @@ done
# Gcc and related flags
CC="$OPTION_CC"
CFLAGS="$OPTION_CFLAGS
- -std=c99 $GCCMACHDEP -g3 -O2 -fno-builtin
+ -std=c99 $GCCMACHDEP -g3 -fno-builtin -fno-merge-constants
-Wall \
-Wno-long-long \
-Wno-attributes \
@@ -496,6 +492,12 @@ CFLAGS="$OPTION_CFLAGS
-Wno-implicit-function-declaration \
-Wno-empty-body"
+if test -z "$OPTION_DEBUG_MACRO"; then
+ CFLAGS="-O2 $CFLAGS"
+else
+ CFLAGS="-O0 $CFLAGS"
+fi
+
# Disable extra warning for clang
if [ "`basename $CC`" = 'clang' ]; then
CFLAGS="-Wno-unknown-warning-option \
@@ -546,7 +548,7 @@ if [ -n "$OPTION_INSTRUMENT" ]; then
$FRAMAC \
$FRAMAC_FLAGS \
$MACHDEP \
- -cpp-extra-args="$OPTION_FRAMAC_CPP_EXTRA" \
+ -cpp-extra-args="$FRAMAC_CPP_EXTRA" \
-e-acsl-share=$EACSL_SHARE \
$OPTION_FRAMA_STDLIB \
$OPTION_VERBOSE \
diff --git a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_api.h b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_api.h
index 2913a829f55684b268d06caccad8a870389df99c..224d50dbeefe922733488e265d6f9a3a7ccd74b4 100644
--- a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_api.h
+++ b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_api.h
@@ -39,6 +39,10 @@ struct bt_block {
size_t init_bytes; //!< Number of initialized bytes within a block
_Bool is_readonly; //!< True if a block is marked read-only
_Bool freeable; //!< True if a block can be de-allocated using `free`
+#ifdef E_ACSL_DEBUG
+ size_t line; //!< Line number where this block was recorded
+ char* file; //!< File name where this block was recorded
+#endif
};
typedef struct bt_block bt_block;
diff --git a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
index 875b9c6b58115caa08ee9f7f2f516fb982a67d52..42007a97637d3d9f5d5a2b43846abfad651e5d3b 100644
--- a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
+++ b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
@@ -67,6 +67,20 @@ static size_t get_heap_size(void) {
}
/* }}} */
+/**************************/
+/* DEBUG {{{ */
+/**************************/
+#ifdef E_ACSL_DEBUG
+/* Notion of current location for debugging purposes */
+static struct current_location {
+ int line;
+ char *file;
+} cloc = { 0, "undefined" };
+
+#define update_cloc(_file, _line) { cloc.line = _line; cloc.file = _file; }
+#endif
+/* }}} */
+
/**************************/
/* INITIALIZATION {{{ */
/**************************/
@@ -238,28 +252,66 @@ static int offset(void* ptr) {
/* store the block of size bytes starting at ptr, the new block is returned.
* Warning: the return type is implicitly (bt_block*). */
static void* store_block(void* ptr, size_t size) {
- bt_block * tmp;
- DASSERT(ptr != NULL);
- tmp = native_malloc(sizeof(bt_block));
- DASSERT(tmp != NULL);
- tmp->ptr = (uintptr_t)ptr;
- tmp->size = size;
- tmp->init_ptr = NULL;
- tmp->init_bytes = 0;
- tmp->is_readonly = false;
- tmp->freeable = false;
- bt_insert(tmp);
+#ifdef E_ACSL_DEBUG
+ if (ptr == NULL)
+ vabort("Attempt to record NULL block");
+ else {
+ char *check = (char*)ptr;
+ bt_block * exitsing_block = bt_find(ptr);
+ if (exitsing_block) {
+ vabort("\nRecording %a [%lu] at %s:%d failed."
+ " Overlapping block %a [%lu] found at %s:%d\n",
+ ptr, size, cloc.file, cloc.line, base_addr(check),
+ block_length(check), exitsing_block->file, exitsing_block->line);
+ }
+ check += size - 1;
+ exitsing_block = bt_find(check);
+ if (exitsing_block) {
+ vabort("\nRecording %a [%lu] at %d failed."
+ " Overlapping block %a [%lu] found at %s:%d\n",
+ ptr, size, cloc.file, cloc.line, base_addr(check),
+ block_length(check), exitsing_block->file, exitsing_block->line);
+ }
+ }
+#endif
+ bt_block * tmp = NULL;
+ if (ptr) {
+ tmp = native_malloc(sizeof(bt_block));
+ tmp->ptr = (uintptr_t)ptr;
+ tmp->size = size;
+ tmp->init_ptr = NULL;
+ tmp->init_bytes = 0;
+ tmp->is_readonly = false;
+ tmp->freeable = false;
+ bt_insert(tmp);
+#ifdef E_ACSL_DEBUG
+ tmp->line = 0;
+ tmp->file = "undefined";
+#endif
+ }
return tmp;
}
/* remove the block starting at ptr */
static void delete_block(void* ptr) {
- DASSERT(ptr != NULL);
- bt_block * tmp = bt_lookup(ptr);
- DASSERT(tmp != NULL);
- bt_clean_block_init(tmp);
- bt_remove(tmp);
- native_free(tmp);
+#ifdef E_ACSL_DEBUG
+ /* Make sure the recorded block is not NULL */
+ if (!ptr)
+ vabort("Attempt to delete NULL block");
+#endif
+ if (ptr != NULL) {
+ bt_block * tmp = bt_lookup(ptr);
+#ifdef E_ACSL_DEBUG
+ /* Make sure the removed block exists in the tracked allocation */
+ if (!tmp)
+ vabort("Attempt to delete untracked block");
+#endif
+ if (tmp) {
+ bt_clean_block_init(tmp);
+ bt_remove(tmp);
+ native_free(tmp);
+ }
+ }
}
/* }}} */
@@ -445,6 +497,51 @@ static void memory_init(int *argc_ref, char ***argv_ref, size_t ptr_size) {
}
/* }}} */
+#ifdef E_ACSL_DEBUG
+
+/* Debug version of store block with location tracking. This function is aimed
+ * at manual debugging. While there is no easy way of traking file/line numbers
+ * recorded memory blocks with the use of the following macros placed after the
+ * declaration of __e_acsl_store_block:
+ *
+ * #define __e_acsl_store_block(...) \
+ * __e_acsl_store_block_debug(__FILE__, __LINE__, __VA_ARGS__)
+ *
+ * The above macros with rewrite of instances of __e_acsl_store_block generating
+ * origin information of tracked memory blocks.
+*/
+void* store_block_debug(char *file, int line, void* ptr, size_t size) {
+ update_cloc(file, line);
+ bt_block * res = store_block(ptr, size);
+ if (res) {
+ res->line = line;
+ res->file = file;
+ }
+ return res;
+}
+
+void delete_block_debug(char *file, int line, void* ptr) {
+ update_cloc(file, line);
+ bt_block * tmp = bt_lookup(ptr);
+ if (!tmp) {
+ vabort("Block with base address %a not found in the memory model at %s:%d",
+ ptr, file, line);
+ }
+ delete_block(ptr);
+}
+
+/* Debug print of block information */
+void block_info(char *p) {
+ bt_block * res = bt_find(p);
+ if (res) {
+ printf(" << %a >> %a [%lu] => %lu \n",
+ p, base_addr(p), offset(p), block_length(p));
+ } else {
+ printf(" << %a >> not allocated\n", p);
+ }
+}
+#endif
+
/* API BINDINGS {{{ */
/* Heap allocation (native) */
strong_alias(bittree_malloc, malloc)
@@ -478,6 +575,9 @@ public_alias(heap_size)
#ifdef E_ACSL_DEBUG /* Debug */
public_alias(bt_print_block)
public_alias(bt_print_tree)
+public_alias(block_info)
+public_alias(store_block_debug)
+public_alias(delete_block_debug)
#endif
/* }}} */
#endif
diff --git a/src/plugins/e-acsl/tests/bts/bts1390.c b/src/plugins/e-acsl/tests/bts/bts1390.c
index fd280a0af1d1e1ce3670d44c1ade6e0a67f0f968..74cba86cdbefc49eb207bda3bdbe6f3178c5f15c 100644
--- a/src/plugins/e-acsl/tests/bts/bts1390.c
+++ b/src/plugins/e-acsl/tests/bts/bts1390.c
@@ -4,13 +4,12 @@
#include "stdlib.h"
-/*@ behavior exists:
- assumes \exists integer i; 0 <= i < n && ((char*)buf)[i] == c;
- ensures
- \forall int j; 0 <= j < \offset((char*)\result) ==> ((char*)buf)[j] != c;
+/*@behavior exists:
+ assumes \exists integer i; 0 <= i < (int)n && ((char*)buf)[i] == c;
+ ensures \forall int j; 0 <= j < (int)\offset((char*)\result) ==> ((char*)buf)[j] != c;
behavior not_exists:
- assumes \forall integer k; 0 <= k < n ==> ((char*)buf)[k] != c;
- ensures \result == (void*) 0; */
+ assumes \forall integer k; 0 <= k < (int)n ==> ((char*)buf)[k] != c;
+ ensures \result == (void*) 0; */
void *memchr(const void *buf, int c, size_t n) {
int i;
char *s = buf;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
index cac7100842598b1e9303261944366a036f23bc78..655291e225abb8a61a0ac65993c51f87b9f4b8a7 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
@@ -2,4 +2,6 @@
FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:150:[value] warning: function __gmpz_add: precondition got status invalid.
+tests/bts/bts1390.c:12:[value] warning: function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:12:[value] warning: function __gen_e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:17:[value] warning: out of bounds read. assert \valid_read(s);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
index 121b10cc72ff299854cbc94605c2d014c83b549e..38237e0896b0689561307db1ab04286605702305 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
@@ -129,17 +129,11 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__gen_e_acsl_valid_3 = __e_acsl_valid((void *)Mtmin_out,sizeof(float));
__e_acsl_assert(__gen_e_acsl_valid_3,(char *)"Precondition",
(char *)"bar",(char *)"\\valid(Mtmin_out)",19);
- __e_acsl_store_block((void *)(& __gen_e_acsl_at_6),8UL);
__gen_e_acsl_at_6 = Mwmin;
- __e_acsl_store_block((void *)(& __gen_e_acsl_at_5),8UL);
__gen_e_acsl_at_5 = Mtmin_in;
- __e_acsl_store_block((void *)(& __gen_e_acsl_at_4),8UL);
__gen_e_acsl_at_4 = Mwmin;
- __e_acsl_store_block((void *)(& __gen_e_acsl_at_3),8UL);
__gen_e_acsl_at_3 = Mtmin_in;
- __e_acsl_store_block((void *)(& __gen_e_acsl_at_2),8UL);
__gen_e_acsl_at_2 = Mtmin_in;
- __e_acsl_store_block((void *)(& __gen_e_acsl_at),8UL);
__gen_e_acsl_at = Mtmin_out;
bar(Mtmin_in,Mwmin,Mtmin_out);
}
@@ -230,11 +224,8 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
__gen_e_acsl_valid_3 = __e_acsl_valid((void *)Mtmax_out,sizeof(float));
__e_acsl_assert(__gen_e_acsl_valid_3,(char *)"Precondition",
(char *)"foo",(char *)"\\valid(Mtmax_out)",7);
- __e_acsl_store_block((void *)(& __gen_e_acsl_at_3),8UL);
__gen_e_acsl_at_3 = Mwmax;
- __e_acsl_store_block((void *)(& __gen_e_acsl_at_2),8UL);
__gen_e_acsl_at_2 = Mtmax_in;
- __e_acsl_store_block((void *)(& __gen_e_acsl_at),8UL);
__gen_e_acsl_at = Mtmax_out;
foo(Mtmax_in,Mwmax,Mtmax_out);
}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
index 0dc222899d2d73a76c0464882443955ca0791d3f..04b954bcd02e789c3f174c8a91572ad3ad8a86c7 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
@@ -69,17 +69,11 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
int *__gen_e_acsl_at;
__e_acsl_store_block((void *)(& Accel),8UL);
__e_acsl_store_block((void *)(& AverageAccel),8UL);
- __e_acsl_store_block((void *)(& __gen_e_acsl_at_6),8UL);
__gen_e_acsl_at_6 = Accel;
- __e_acsl_store_block((void *)(& __gen_e_acsl_at_5),8UL);
__gen_e_acsl_at_5 = Accel;
- __e_acsl_store_block((void *)(& __gen_e_acsl_at_4),8UL);
__gen_e_acsl_at_4 = Accel;
- __e_acsl_store_block((void *)(& __gen_e_acsl_at_3),8UL);
__gen_e_acsl_at_3 = Accel;
- __e_acsl_store_block((void *)(& __gen_e_acsl_at_2),8UL);
__gen_e_acsl_at_2 = Accel;
- __e_acsl_store_block((void *)(& __gen_e_acsl_at),8UL);
__gen_e_acsl_at = AverageAccel;
atp_NORMAL_computeAverageAccel(Accel,AverageAccel);
{
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
index 5c194226eec561c2ae4eae73fb98baec27f7a8d4..c2302f70811614faa51481211425ec7a4d140363 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
@@ -2,27 +2,27 @@
char *__gen_e_acsl_literal_string;
char *__gen_e_acsl_literal_string_2;
/*@ behavior exists:
- assumes ∃ ℤ i; 0 ≤ i < n ∧ (int)*((char *)buf+i) ≡ c;
+ assumes ∃ ℤ i; 0 ≤ i < (int)n ∧ (int)*((char *)buf+i) ≡ c;
ensures
∀ int j;
- 0 ≤ j < \offset((char *)\result) ⇒
+ 0 ≤ j < (int)\offset((char *)\result) ⇒
(int)*((char *)\old(buf)+j) ≢ \old(c);
behavior not_exists:
- assumes ∀ ℤ k; 0 ≤ k < n ⇒ (int)*((char *)buf+k) ≢ c;
+ assumes ∀ ℤ k; 0 ≤ k < (int)n ⇒ (int)*((char *)buf+k) ≢ c;
ensures \result ≡ (void *)0;
*/
void *__gen_e_acsl_memchr(void const *buf, int c, size_t n);
/*@ behavior exists:
- assumes ∃ ℤ i; 0 ≤ i < n ∧ (int)*((char *)buf+i) ≡ c;
+ assumes ∃ ℤ i; 0 ≤ i < (int)n ∧ (int)*((char *)buf+i) ≡ c;
ensures
∀ int j;
- 0 ≤ j < \offset((char *)\result) ⇒
+ 0 ≤ j < (int)\offset((char *)\result) ⇒
(int)*((char *)\old(buf)+j) ≢ \old(c);
behavior not_exists:
- assumes ∀ ℤ k; 0 ≤ k < n ⇒ (int)*((char *)buf+k) ≢ c;
+ assumes ∀ ℤ k; 0 ≤ k < (int)n ⇒ (int)*((char *)buf+k) ≢ c;
ensures \result ≡ (void *)0;
*/
void *memchr(void const *buf, int c, size_t n)
@@ -37,6 +37,7 @@ void *memchr(void const *buf, int c, size_t n)
s = (char *)buf;
i = 0;
while ((size_t)i < n) {
+ /*@ assert Value: mem_access: \valid_read(s); */
if ((int)*s == c) {
__e_acsl_full_init((void *)(& __retres));
__retres = (void *)s;
@@ -56,14 +57,14 @@ void *memchr(void const *buf, int c, size_t n)
}
/*@ behavior exists:
- assumes ∃ ℤ i; 0 ≤ i < n ∧ (int)*((char *)buf+i) ≡ c;
+ assumes ∃ ℤ i; 0 ≤ i < (int)n ∧ (int)*((char *)buf+i) ≡ c;
ensures
∀ int j;
- 0 ≤ j < \offset((char *)\result) ⇒
+ 0 ≤ j < (int)\offset((char *)\result) ⇒
(int)*((char *)\old(buf)+j) ≢ \old(c);
behavior not_exists:
- assumes ∀ ℤ k; 0 ≤ k < n ⇒ (int)*((char *)buf+k) ≢ c;
+ assumes ∀ ℤ k; 0 ≤ k < (int)n ⇒ (int)*((char *)buf+k) ≢ c;
ensures \result ≡ (void *)0;
*/
void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
@@ -79,9 +80,9 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
int __gen_e_acsl_forall_2;
unsigned long __gen_e_acsl_k;
__gen_e_acsl_forall_2 = 1;
- __gen_e_acsl_k = 0UL;
+ __gen_e_acsl_k = 0U;
while (1) {
- if (__gen_e_acsl_k < n) ; else break;
+ if (__gen_e_acsl_k < (unsigned int)((int)n)) ; else break;
{
int __gen_e_acsl_valid_read_3;
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)((char *)buf + __gen_e_acsl_k),
@@ -89,40 +90,27 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",
(char *)"memchr",
(char *)"mem_access: \\valid_read((char *)buf+__gen_e_acsl_k)",
- 12);
+ 11);
if ((int)*((char *)buf + __gen_e_acsl_k) != c) ;
else {
__gen_e_acsl_forall_2 = 0;
goto e_acsl_end_loop3;
}
}
- {
- mpz_t __gen_e_acsl__5;
- mpz_t __gen_e_acsl_add_3;
- unsigned long __gen_e_acsl__6;
- __gmpz_init_set_si(__gen_e_acsl__5,1L);
- __gmpz_init(__gen_e_acsl_add_3);
- __gmpz_add(__gen_e_acsl_add_3,(__mpz_struct const *)__gen_e_acsl_k,
- (__mpz_struct const *)(__gen_e_acsl__5));
- __gen_e_acsl__6 = __gmpz_get_ui((__mpz_struct const *)(__gen_e_acsl_add_3));
- __gen_e_acsl_k = __gen_e_acsl__6;
- __gmpz_clear(__gen_e_acsl__5);
- __gmpz_clear(__gen_e_acsl_add_3);
- }
+ __gen_e_acsl_k ++;
}
e_acsl_end_loop3: ;
__gen_e_acsl_at_4 = __gen_e_acsl_forall_2;
}
__gen_e_acsl_at_3 = c;
- __e_acsl_store_block((void *)(& __gen_e_acsl_at_2),8UL);
__gen_e_acsl_at_2 = buf;
{
int __gen_e_acsl_exists;
unsigned long __gen_e_acsl_i;
__gen_e_acsl_exists = 0;
- __gen_e_acsl_i = 0UL;
+ __gen_e_acsl_i = 0U;
while (1) {
- if (__gen_e_acsl_i < n) ; else break;
+ if (__gen_e_acsl_i < (unsigned int)((int)n)) ; else break;
{
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)((char *)buf + __gen_e_acsl_i),
@@ -137,19 +125,7 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
goto e_acsl_end_loop1;
}
}
- {
- mpz_t __gen_e_acsl_;
- mpz_t __gen_e_acsl_add;
- unsigned long __gen_e_acsl__2;
- __gmpz_init_set_si(__gen_e_acsl_,1L);
- __gmpz_init(__gen_e_acsl_add);
- __gmpz_add(__gen_e_acsl_add,(__mpz_struct const *)__gen_e_acsl_i,
- (__mpz_struct const *)(__gen_e_acsl_));
- __gen_e_acsl__2 = __gmpz_get_ui((__mpz_struct const *)(__gen_e_acsl_add));
- __gen_e_acsl_i = __gen_e_acsl__2;
- __gmpz_clear(__gen_e_acsl_);
- __gmpz_clear(__gen_e_acsl_add);
- }
+ __gen_e_acsl_i ++;
}
e_acsl_end_loop1: ;
__gen_e_acsl_at = __gen_e_acsl_exists;
@@ -168,7 +144,8 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
{
int __gen_e_acsl_offset;
__gen_e_acsl_offset = __e_acsl_offset(__retres);
- if (__gen_e_acsl_j < __gen_e_acsl_offset) ; else break;
+ if (__gen_e_acsl_j < (unsigned int)__gen_e_acsl_offset) ;
+ else break;
}
{
int __gen_e_acsl_valid_read_2;
@@ -177,7 +154,7 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",
(char *)"memchr",
(char *)"mem_access: \\valid_read((char *)__gen_e_acsl_at_2+__gen_e_acsl_j)",
- 10);
+ 9);
if ((int)*((char *)__gen_e_acsl_at_2 + __gen_e_acsl_j) != __gen_e_acsl_at_3)
;
else {
@@ -185,33 +162,21 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
goto e_acsl_end_loop2;
}
}
- {
- mpz_t __gen_e_acsl__3;
- mpz_t __gen_e_acsl_add_2;
- unsigned long __gen_e_acsl__4;
- __gmpz_init_set_si(__gen_e_acsl__3,1L);
- __gmpz_init(__gen_e_acsl_add_2);
- __gmpz_add(__gen_e_acsl_add_2,(__mpz_struct const *)__gen_e_acsl_j,
- (__mpz_struct const *)(__gen_e_acsl__3));
- __gen_e_acsl__4 = __gmpz_get_ui((__mpz_struct const *)(__gen_e_acsl_add_2));
- __gen_e_acsl_j = __gen_e_acsl__4;
- __gmpz_clear(__gen_e_acsl__3);
- __gmpz_clear(__gen_e_acsl_add_2);
- }
+ __gen_e_acsl_j ++;
}
e_acsl_end_loop2: ;
__gen_e_acsl_implies = __gen_e_acsl_forall;
}
__e_acsl_assert(__gen_e_acsl_implies,(char *)"Postcondition",
(char *)"memchr",
- (char *)"\\old(\\exists integer i; 0 <= i < n && (int)*((char *)buf+i) == c) ==>\n(\\forall int j;\n 0 <= j < \\offset((char *)\\result) ==>\n (int)*((char *)\\old(buf)+j) != \\old(c))",
- 10);
+ (char *)"\\old(\\exists integer i; 0 <= i < (int)n && (int)*((char *)buf+i) == c) ==>\n(\\forall int j;\n 0 <= j < (int)\\offset((char *)\\result) ==>\n (int)*((char *)\\old(buf)+j) != \\old(c))",
+ 9);
if (! __gen_e_acsl_at_4) __gen_e_acsl_implies_2 = 1;
else __gen_e_acsl_implies_2 = __retres == (void *)0;
__e_acsl_assert(__gen_e_acsl_implies_2,(char *)"Postcondition",
(char *)"memchr",
- (char *)"\\old(\\forall integer k; 0 <= k < n ==> (int)*((char *)buf+k) != c) ==>\n\\result == (void *)0",
- 13);
+ (char *)"\\old(\\forall integer k; 0 <= k < (int)n ==> (int)*((char *)buf+k) != c) ==>\n\\result == (void *)0",
+ 12);
__e_acsl_delete_block((void *)(& buf));
__e_acsl_delete_block((void *)(& __retres));
return __retres;
diff --git a/src/plugins/e-acsl/tests/bts/test_config b/src/plugins/e-acsl/tests/bts/test_config
index f996eb13e7da3e64c5bf2dac43f9bdaf9019e758..171db7a2a18a956f81596ea501bef1fe308b893a 100644
--- a/src/plugins/e-acsl/tests/bts/test_config
+++ b/src/plugins/e-acsl/tests/bts/test_config
@@ -1,3 +1,3 @@
LOG: gen_@PTEST_NAME@.c
OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/bts/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -value-verbose 0
-EXECNOW: ./scripts/testrun.sh @PTEST_NAME@ bts "" "--frama-c=@frama-c@"
+EXEC: ./scripts/testrun.sh @PTEST_NAME@ bts "" "--frama-c=@frama-c@"
diff --git a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevator_test/CSRV14/main.o b/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevator_test/CSRV14/main.o
deleted file mode 100755
index 41692ff84e80669df0633240871ef9484128465d..0000000000000000000000000000000000000000
Binary files a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevator_test/CSRV14/main.o and /dev/null differ
diff --git a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/cabin.o b/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/cabin.o
deleted file mode 100755
index 7ef4b421ba573c31d17f4838e2a1a4c496b7cd2e..0000000000000000000000000000000000000000
Binary files a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/cabin.o and /dev/null differ
diff --git a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/door.o b/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/door.o
deleted file mode 100755
index 07cc21e7226302faf0db09e9d52b851171012680..0000000000000000000000000000000000000000
Binary files a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/door.o and /dev/null differ
diff --git a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/elevator.o b/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/elevator.o
deleted file mode 100755
index 2e58d11072effaf2debbfa9048618b2a1d9f5023..0000000000000000000000000000000000000000
Binary files a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/elevator.o and /dev/null differ
diff --git a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/ext_call.o b/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/ext_call.o
deleted file mode 100755
index 08a427d2d19bf02c9a4cff84adc6099c209d908a..0000000000000000000000000000000000000000
Binary files a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/ext_call.o and /dev/null differ
diff --git a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/rendering.o b/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/rendering.o
deleted file mode 100755
index 3849778e6b1899979ba67ec3e5e2c7c2a30514c5..0000000000000000000000000000000000000000
Binary files a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/rendering.o and /dev/null differ
diff --git a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/testing.o b/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/testing.o
deleted file mode 100755
index b168888c608f174a022e681f1032eda7d84d06e2..0000000000000000000000000000000000000000
Binary files a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/testing.o and /dev/null differ
diff --git a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/transitions.o b/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/transitions.o
deleted file mode 100755
index 0a7018777f678ae53443b4232b18ba249eec8a91..0000000000000000000000000000000000000000
Binary files a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/transitions.o and /dev/null differ
diff --git a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/utils.o b/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/utils.o
deleted file mode 100755
index 8f3f5088e0dae947f0fbb96d5f69d5ad79a92a6a..0000000000000000000000000000000000000000
Binary files a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/utils.o and /dev/null differ
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
index a59759c3885b81a338b3313783d76852c40890e5..c1e8d6648be0a8c95ef8404483507f09cb3efc86 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
@@ -51,7 +51,6 @@ void g(int *p, int *q)
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)q,sizeof(int));
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"g",
(char *)"mem_access: \\valid_read(q)",28);
- __e_acsl_store_block((void *)(& __gen_e_acsl_at_3),8UL);
__gen_e_acsl_at_3 = (unsigned long)*q;
}
{
@@ -59,7 +58,6 @@ void g(int *p, int *q)
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)q,sizeof(int));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"g",
(char *)"mem_access: \\valid_read(q)",26);
- __e_acsl_store_block((void *)(& __gen_e_acsl_at),8UL);
__gen_e_acsl_at = (unsigned long)*q;
}
__e_acsl_initialize((void *)p,sizeof(int));
@@ -76,7 +74,6 @@ void g(int *p, int *q)
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"g",
(char *)"mem_access: \\valid_read(p+__gen_e_acsl_at)",
26);
- __e_acsl_store_block((void *)(& __gen_e_acsl_at_2),4UL);
__gen_e_acsl_at_2 = *(p + __gen_e_acsl_at);
}
A = 4;
@@ -126,11 +123,8 @@ int main(void)
__e_acsl_full_init((void *)(& x));
x = __gen_e_acsl_h(0);
L:
- __e_acsl_store_block((void *)(& __gen_e_acsl_at_3),4UL);
__gen_e_acsl_at_3 = x;
- __e_acsl_store_block((void *)(& __gen_e_acsl_at_2),8UL);
__gen_e_acsl_at_2 = x + 1L;
- __e_acsl_store_block((void *)(& __gen_e_acsl_at),4UL);
__gen_e_acsl_at = x;
/*@ assert x ≡ 0; */
__e_acsl_assert(x == 0,(char *)"Assertion",(char *)"main",
@@ -164,7 +158,6 @@ int __gen_e_acsl_h(int x)
int __retres;
__e_acsl_store_block((void *)(& __retres),4UL);
__e_acsl_store_block((void *)(& x),4UL);
- __e_acsl_store_block((void *)(& __gen_e_acsl_at),4UL);
__gen_e_acsl_at = x;
__retres = h(x);
__e_acsl_assert(__retres == __gen_e_acsl_at,(char *)"Postcondition",
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
index 5c2f9f5687e1eb9ade14568536f9b763ec593005..2fe226b344b8efbbcc708c3463b5def8e37ad5c1 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
@@ -106,7 +106,6 @@ void g(int *p, int *q)
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)q,sizeof(int));
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"g",
(char *)"mem_access: \\valid_read(q)",28);
- __e_acsl_store_block((void *)(& __gen_e_acsl_at_3),8UL);
__gen_e_acsl_at_3 = (unsigned long)*q;
}
{
@@ -114,7 +113,6 @@ void g(int *p, int *q)
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)q,sizeof(int));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"g",
(char *)"mem_access: \\valid_read(q)",26);
- __e_acsl_store_block((void *)(& __gen_e_acsl_at),8UL);
__gen_e_acsl_at = (unsigned long)*q;
}
__e_acsl_initialize((void *)p,sizeof(int));
diff --git a/src/plugins/e-acsl/tests/gmp/test_config b/src/plugins/e-acsl/tests/gmp/test_config
index ebb7cbf51e4a4bb8fd52deafb1d71761c1a2b989..b51a18dcf2f95a90239b1a25a517a65a5e866834 100644
--- a/src/plugins/e-acsl/tests/gmp/test_config
+++ b/src/plugins/e-acsl/tests/gmp/test_config
@@ -1,5 +1,5 @@
LOG: gen_@PTEST_NAME@.c
OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/gmp/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results
-EXECNOW: ./scripts/testrun.sh @PTEST_NAME@ gmp "1" "--frama-c=@frama-c@"
+EXEC: ./scripts/testrun.sh @PTEST_NAME@ gmp "1" "--frama-c=@frama-c@"
LOG: gen_@PTEST_NAME@2.c
OPT: -machdep gcc_x86_64 -check -e-acsl -e-acsl-gmp-only -then-last -load-script tests/print.cmxs -print -ocode tests/gmp/result/gen_@PTEST_NAME@2.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results
diff --git a/src/plugins/e-acsl/tests/runtime/block_length.c b/src/plugins/e-acsl/tests/runtime/block_length.c
index 9898e98c851b27c67f8d1d405b26abd539917f09..ec9929798b2e3c4fb86e2c6867dd66c904dd3b71 100644
--- a/src/plugins/e-acsl/tests/runtime/block_length.c
+++ b/src/plugins/e-acsl/tests/runtime/block_length.c
@@ -10,6 +10,11 @@ int *PA;
struct Zero { } ZERO;
int main(void) {
+ /* Zero-sized blocks */
+ struct Zero zero;
+ /*@ assert \block_length(&ZERO) == 0; */
+ /*@ assert \block_length(&zero) == 0; */
+
/* Global memory */
PA = (int*)&A;
/*@ assert \block_length(A) == sizeof(A); */
@@ -54,9 +59,4 @@ int main(void) {
/*@ assert \block_length(q) == size; */
q += 4;
/*@ assert \block_length(q) == size; */
-
- /* Zero-sized blocks */
- struct Zero zero;
- /*@ assert \block_length(&ZERO) == 0; */
- /*@ assert \block_length(&zero) == 0; */
}
diff --git a/src/plugins/e-acsl/tests/runtime/literal_string.i b/src/plugins/e-acsl/tests/runtime/literal_string.i
index 311aa4afae01b36ff1f05d534cef4e70567b101a..553b9e3ed0dbcd42b9cf1841bc7d3c0facc87db8 100644
--- a/src/plugins/e-acsl/tests/runtime/literal_string.i
+++ b/src/plugins/e-acsl/tests/runtime/literal_string.i
@@ -17,6 +17,9 @@ char *S2 = "foo2";
int IDX = 1;
int G2 = 2;
+const char *s_str = "the cat";
+const char *l_str = "the dog and the cat";
+
int main(void) {
char *SS = "ss";
/*@ assert S[G2] == 'o'; */
@@ -24,6 +27,12 @@ int main(void) {
/*@ assert \valid_read(S2); */
/*@ assert ! \valid(SS); */
f();
+
+ /* Make sure that compiler does not "merge strings", i.e., represents literal
+ * strings as separate memory blocks. An assertion enabled in the debug mode
+ * fails the execution if `s_str` is used as a part of `l_str`. */
+ s_str++;
+ l_str++;
return 0;
}
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/block_length.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/block_length.res.oracle
index 3ca9eaf93f66c8f959a17b5e4948ffe220e4640e..61ec66632fbda2359eac00eccf644295e1a9093e 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/block_length.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/block_length.res.oracle
@@ -1,9 +1,9 @@
[e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
-tests/runtime/block_length.c:45:[value] warning: assertion got status unknown.
+tests/runtime/block_length.c:50:[value] warning: assertion got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/runtime/block_length.c:46:[value] warning: assertion got status unknown.
-tests/runtime/block_length.c:48:[value] warning: assertion got status unknown.
-tests/runtime/block_length.c:54:[value] warning: assertion got status unknown.
-tests/runtime/block_length.c:56:[value] warning: assertion got status unknown.
+tests/runtime/block_length.c:51:[value] warning: assertion got status unknown.
+tests/runtime/block_length.c:53:[value] warning: assertion got status unknown.
+tests/runtime/block_length.c:59:[value] warning: assertion got status unknown.
+tests/runtime/block_length.c:61:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_block_length.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_block_length.c
index 0ff26feea3cf2ed88cef6d941f6225d17afaff95..59a9d93d684fa911b4e00cb1592a11b5d965c484 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_block_length.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_block_length.c
@@ -19,6 +19,7 @@ void __e_acsl_globals_init(void)
int main(void)
{
int __retres;
+ struct Zero zero;
int a[4];
int *pa;
long l;
@@ -27,10 +28,8 @@ int main(void)
size_t size;
char *p;
long *q;
- struct Zero zero;
__e_acsl_memory_init((int *)0,(char ***)0,8UL);
__e_acsl_globals_init();
- __e_acsl_store_block((void *)(& zero),0UL);
__e_acsl_store_block((void *)(& q),8UL);
__e_acsl_store_block((void *)(& p),8UL);
__e_acsl_store_block((void *)(& pi),8UL);
@@ -38,42 +37,57 @@ int main(void)
__e_acsl_store_block((void *)(& l),8UL);
__e_acsl_store_block((void *)(& pa),8UL);
__e_acsl_store_block((void *)(a),16UL);
+ __e_acsl_store_block((void *)(& zero),0UL);
+ /*@ assert \block_length(&ZERO) ≡ 0; */
+ {
+ unsigned long __gen_e_acsl_block_length;
+ __gen_e_acsl_block_length = __e_acsl_block_length((void *)(& ZERO));
+ __e_acsl_assert(__gen_e_acsl_block_length == 0UL,(char *)"Assertion",
+ (char *)"main",(char *)"\\block_length(&ZERO) == 0",15);
+ }
+ /*@ assert \block_length(&zero) ≡ 0; */
+ {
+ unsigned long __gen_e_acsl_block_length_2;
+ __gen_e_acsl_block_length_2 = __e_acsl_block_length((void *)(& zero));
+ __e_acsl_assert(__gen_e_acsl_block_length_2 == 0UL,(char *)"Assertion",
+ (char *)"main",(char *)"\\block_length(&zero) == 0",16);
+ }
PA = (int *)(& A);
/*@ assert \block_length((int *)A) ≡ sizeof(A); */
{
- unsigned long __gen_e_acsl_block_length;
- __gen_e_acsl_block_length = __e_acsl_block_length((void *)(A));
- __e_acsl_assert(__gen_e_acsl_block_length == 16,(char *)"Assertion",
+ unsigned long __gen_e_acsl_block_length_3;
+ __gen_e_acsl_block_length_3 = __e_acsl_block_length((void *)(A));
+ __e_acsl_assert(__gen_e_acsl_block_length_3 == 16,(char *)"Assertion",
(char *)"main",
- (char *)"\\block_length((int *)A) == sizeof(A)",15);
+ (char *)"\\block_length((int *)A) == sizeof(A)",20);
}
/*@ assert \block_length(&A[3]) ≡ sizeof(A); */
{
- unsigned long __gen_e_acsl_block_length_2;
- __gen_e_acsl_block_length_2 = __e_acsl_block_length((void *)(& A[3UL]));
- __e_acsl_assert(__gen_e_acsl_block_length_2 == 16,(char *)"Assertion",
+ unsigned long __gen_e_acsl_block_length_4;
+ __gen_e_acsl_block_length_4 = __e_acsl_block_length((void *)(& A[3UL]));
+ __e_acsl_assert(__gen_e_acsl_block_length_4 == 16,(char *)"Assertion",
(char *)"main",
- (char *)"\\block_length(&A[3]) == sizeof(A)",16);
+ (char *)"\\block_length(&A[3]) == sizeof(A)",21);
}
/*@ assert \block_length(PA) ≡ sizeof(A); */
{
- unsigned long __gen_e_acsl_block_length_3;
- __gen_e_acsl_block_length_3 = __e_acsl_block_length((void *)PA);
- __e_acsl_assert(__gen_e_acsl_block_length_3 == 16,(char *)"Assertion",
+ unsigned long __gen_e_acsl_block_length_5;
+ __gen_e_acsl_block_length_5 = __e_acsl_block_length((void *)PA);
+ __e_acsl_assert(__gen_e_acsl_block_length_5 == 16,(char *)"Assertion",
(char *)"main",(char *)"\\block_length(PA) == sizeof(A)",
- 17);
+ 22);
}
PA ++;
/*@ assert \block_length(PA+1) ≡ \block_length(&A[1]); */
{
- unsigned long __gen_e_acsl_block_length_4;
- unsigned long __gen_e_acsl_block_length_5;
- __gen_e_acsl_block_length_4 = __e_acsl_block_length((void *)(PA + 1UL));
- __gen_e_acsl_block_length_5 = __e_acsl_block_length((void *)(& A[1UL]));
- __e_acsl_assert(__gen_e_acsl_block_length_4 == __gen_e_acsl_block_length_5,
+ unsigned long __gen_e_acsl_block_length_6;
+ unsigned long __gen_e_acsl_block_length_7;
+ __gen_e_acsl_block_length_6 = __e_acsl_block_length((void *)(PA + 1UL));
+ __gen_e_acsl_block_length_7 = __e_acsl_block_length((void *)(& A[1UL]));
+ __e_acsl_assert(__gen_e_acsl_block_length_6 == __gen_e_acsl_block_length_7,
(char *)"Assertion",(char *)"main",
(char *)"\\block_length(PA+1) == \\block_length(&A[1])",
- 19);
+ 24);
}
__e_acsl_initialize((void *)(a),sizeof(int));
a[0] = 1;
@@ -87,40 +101,40 @@ int main(void)
pa = (int *)(& a);
/*@ assert \block_length((int *)a) ≡ sizeof(a); */
{
- unsigned long __gen_e_acsl_block_length_6;
- __gen_e_acsl_block_length_6 = __e_acsl_block_length((void *)(a));
- __e_acsl_assert(__gen_e_acsl_block_length_6 == 16,(char *)"Assertion",
+ unsigned long __gen_e_acsl_block_length_8;
+ __gen_e_acsl_block_length_8 = __e_acsl_block_length((void *)(a));
+ __e_acsl_assert(__gen_e_acsl_block_length_8 == 16,(char *)"Assertion",
(char *)"main",
- (char *)"\\block_length((int *)a) == sizeof(a)",24);
+ (char *)"\\block_length((int *)a) == sizeof(a)",29);
}
/*@ assert \block_length(&a[3]) ≡ sizeof(a); */
{
- unsigned long __gen_e_acsl_block_length_7;
- __gen_e_acsl_block_length_7 = __e_acsl_block_length((void *)(& a[3UL]));
- __e_acsl_assert(__gen_e_acsl_block_length_7 == 16,(char *)"Assertion",
+ unsigned long __gen_e_acsl_block_length_9;
+ __gen_e_acsl_block_length_9 = __e_acsl_block_length((void *)(& a[3UL]));
+ __e_acsl_assert(__gen_e_acsl_block_length_9 == 16,(char *)"Assertion",
(char *)"main",
- (char *)"\\block_length(&a[3]) == sizeof(a)",25);
+ (char *)"\\block_length(&a[3]) == sizeof(a)",30);
}
/*@ assert \block_length(pa) ≡ sizeof(a); */
{
- unsigned long __gen_e_acsl_block_length_8;
- __gen_e_acsl_block_length_8 = __e_acsl_block_length((void *)pa);
- __e_acsl_assert(__gen_e_acsl_block_length_8 == 16,(char *)"Assertion",
+ unsigned long __gen_e_acsl_block_length_10;
+ __gen_e_acsl_block_length_10 = __e_acsl_block_length((void *)pa);
+ __e_acsl_assert(__gen_e_acsl_block_length_10 == 16,(char *)"Assertion",
(char *)"main",(char *)"\\block_length(pa) == sizeof(a)",
- 26);
+ 31);
}
__e_acsl_full_init((void *)(& pa));
pa ++;
/*@ assert \block_length(pa+1) ≡ \block_length(&a[1]); */
{
- unsigned long __gen_e_acsl_block_length_9;
- unsigned long __gen_e_acsl_block_length_10;
- __gen_e_acsl_block_length_9 = __e_acsl_block_length((void *)(pa + 1UL));
- __gen_e_acsl_block_length_10 = __e_acsl_block_length((void *)(& a[1UL]));
- __e_acsl_assert(__gen_e_acsl_block_length_9 == __gen_e_acsl_block_length_10,
+ unsigned long __gen_e_acsl_block_length_11;
+ unsigned long __gen_e_acsl_block_length_12;
+ __gen_e_acsl_block_length_11 = __e_acsl_block_length((void *)(pa + 1UL));
+ __gen_e_acsl_block_length_12 = __e_acsl_block_length((void *)(& a[1UL]));
+ __e_acsl_assert(__gen_e_acsl_block_length_11 == __gen_e_acsl_block_length_12,
(char *)"Assertion",(char *)"main",
(char *)"\\block_length(pa+1) == \\block_length(&a[1])",
- 28);
+ 33);
}
__e_acsl_full_init((void *)(& l));
l = (long)4;
@@ -128,119 +142,104 @@ int main(void)
pl = (char *)(& l);
/*@ assert \block_length(&l) ≡ sizeof(long); */
{
- unsigned long __gen_e_acsl_block_length_11;
- __gen_e_acsl_block_length_11 = __e_acsl_block_length((void *)(& l));
- __e_acsl_assert(__gen_e_acsl_block_length_11 == 8,(char *)"Assertion",
+ unsigned long __gen_e_acsl_block_length_13;
+ __gen_e_acsl_block_length_13 = __e_acsl_block_length((void *)(& l));
+ __e_acsl_assert(__gen_e_acsl_block_length_13 == 8,(char *)"Assertion",
(char *)"main",
- (char *)"\\block_length(&l) == sizeof(long)",34);
+ (char *)"\\block_length(&l) == sizeof(long)",39);
}
/*@ assert \block_length(pl) ≡ sizeof(long); */
{
- unsigned long __gen_e_acsl_block_length_12;
- __gen_e_acsl_block_length_12 = __e_acsl_block_length((void *)pl);
- __e_acsl_assert(__gen_e_acsl_block_length_12 == 8,(char *)"Assertion",
+ unsigned long __gen_e_acsl_block_length_14;
+ __gen_e_acsl_block_length_14 = __e_acsl_block_length((void *)pl);
+ __e_acsl_assert(__gen_e_acsl_block_length_14 == 8,(char *)"Assertion",
(char *)"main",
- (char *)"\\block_length(pl) == sizeof(long)",35);
+ (char *)"\\block_length(pl) == sizeof(long)",40);
}
/*@ assert \block_length(pl+7) ≡ sizeof(long); */
{
- unsigned long __gen_e_acsl_block_length_13;
- __gen_e_acsl_block_length_13 = __e_acsl_block_length((void *)(pl + 7UL));
- __e_acsl_assert(__gen_e_acsl_block_length_13 == 8,(char *)"Assertion",
+ unsigned long __gen_e_acsl_block_length_15;
+ __gen_e_acsl_block_length_15 = __e_acsl_block_length((void *)(pl + 7UL));
+ __e_acsl_assert(__gen_e_acsl_block_length_15 == 8,(char *)"Assertion",
(char *)"main",
- (char *)"\\block_length(pl+7) == sizeof(long)",36);
+ (char *)"\\block_length(pl+7) == sizeof(long)",41);
}
__e_acsl_full_init((void *)(& pi));
pi = (int *)(& l);
/*@ assert \block_length(pi) ≡ \block_length(&l); */
{
- unsigned long __gen_e_acsl_block_length_14;
- unsigned long __gen_e_acsl_block_length_15;
- __gen_e_acsl_block_length_14 = __e_acsl_block_length((void *)pi);
- __gen_e_acsl_block_length_15 = __e_acsl_block_length((void *)(& l));
- __e_acsl_assert(__gen_e_acsl_block_length_14 == __gen_e_acsl_block_length_15,
+ unsigned long __gen_e_acsl_block_length_16;
+ unsigned long __gen_e_acsl_block_length_17;
+ __gen_e_acsl_block_length_16 = __e_acsl_block_length((void *)pi);
+ __gen_e_acsl_block_length_17 = __e_acsl_block_length((void *)(& l));
+ __e_acsl_assert(__gen_e_acsl_block_length_16 == __gen_e_acsl_block_length_17,
(char *)"Assertion",(char *)"main",
- (char *)"\\block_length(pi) == \\block_length(&l)",38);
+ (char *)"\\block_length(pi) == \\block_length(&l)",43);
}
__e_acsl_full_init((void *)(& pi));
pi ++;
/*@ assert \block_length(pi) ≡ \block_length(&l); */
{
- unsigned long __gen_e_acsl_block_length_16;
- unsigned long __gen_e_acsl_block_length_17;
- __gen_e_acsl_block_length_16 = __e_acsl_block_length((void *)pi);
- __gen_e_acsl_block_length_17 = __e_acsl_block_length((void *)(& l));
- __e_acsl_assert(__gen_e_acsl_block_length_16 == __gen_e_acsl_block_length_17,
+ unsigned long __gen_e_acsl_block_length_18;
+ unsigned long __gen_e_acsl_block_length_19;
+ __gen_e_acsl_block_length_18 = __e_acsl_block_length((void *)pi);
+ __gen_e_acsl_block_length_19 = __e_acsl_block_length((void *)(& l));
+ __e_acsl_assert(__gen_e_acsl_block_length_18 == __gen_e_acsl_block_length_19,
(char *)"Assertion",(char *)"main",
- (char *)"\\block_length(pi) == \\block_length(&l)",40);
+ (char *)"\\block_length(pi) == \\block_length(&l)",45);
}
size = (unsigned long)12;
__e_acsl_full_init((void *)(& p));
p = (char *)malloc(size);
/*@ assert \block_length(p) ≡ size; */
{
- unsigned long __gen_e_acsl_block_length_18;
- __gen_e_acsl_block_length_18 = __e_acsl_block_length((void *)p);
- __e_acsl_assert(__gen_e_acsl_block_length_18 == size,(char *)"Assertion",
- (char *)"main",(char *)"\\block_length(p) == size",45);
+ unsigned long __gen_e_acsl_block_length_20;
+ __gen_e_acsl_block_length_20 = __e_acsl_block_length((void *)p);
+ __e_acsl_assert(__gen_e_acsl_block_length_20 == size,(char *)"Assertion",
+ (char *)"main",(char *)"\\block_length(p) == size",50);
}
/*@ assert \block_length(p+11) ≡ size; */
{
- unsigned long __gen_e_acsl_block_length_19;
- __gen_e_acsl_block_length_19 = __e_acsl_block_length((void *)(p + 11UL));
- __e_acsl_assert(__gen_e_acsl_block_length_19 == size,(char *)"Assertion",
- (char *)"main",(char *)"\\block_length(p+11) == size",46);
+ unsigned long __gen_e_acsl_block_length_21;
+ __gen_e_acsl_block_length_21 = __e_acsl_block_length((void *)(p + 11UL));
+ __e_acsl_assert(__gen_e_acsl_block_length_21 == size,(char *)"Assertion",
+ (char *)"main",(char *)"\\block_length(p+11) == size",51);
}
__e_acsl_full_init((void *)(& p));
p += 5;
/*@ assert \block_length(p+5) ≡ \block_length(p-5); */
{
- unsigned long __gen_e_acsl_block_length_20;
- unsigned long __gen_e_acsl_block_length_21;
- __gen_e_acsl_block_length_20 = __e_acsl_block_length((void *)(p + 5UL));
- __gen_e_acsl_block_length_21 = __e_acsl_block_length((void *)(p - 5UL));
- __e_acsl_assert(__gen_e_acsl_block_length_20 == __gen_e_acsl_block_length_21,
+ unsigned long __gen_e_acsl_block_length_22;
+ unsigned long __gen_e_acsl_block_length_23;
+ __gen_e_acsl_block_length_22 = __e_acsl_block_length((void *)(p + 5UL));
+ __gen_e_acsl_block_length_23 = __e_acsl_block_length((void *)(p - 5UL));
+ __e_acsl_assert(__gen_e_acsl_block_length_22 == __gen_e_acsl_block_length_23,
(char *)"Assertion",(char *)"main",
- (char *)"\\block_length(p+5) == \\block_length(p-5)",48);
+ (char *)"\\block_length(p+5) == \\block_length(p-5)",53);
}
size = (unsigned long)30 * sizeof(long);
__e_acsl_full_init((void *)(& q));
q = (long *)malloc(size);
/*@ assert \block_length(q) ≡ size; */
{
- unsigned long __gen_e_acsl_block_length_22;
- __gen_e_acsl_block_length_22 = __e_acsl_block_length((void *)q);
- __e_acsl_assert(__gen_e_acsl_block_length_22 == size,(char *)"Assertion",
- (char *)"main",(char *)"\\block_length(q) == size",54);
+ unsigned long __gen_e_acsl_block_length_24;
+ __gen_e_acsl_block_length_24 = __e_acsl_block_length((void *)q);
+ __e_acsl_assert(__gen_e_acsl_block_length_24 == size,(char *)"Assertion",
+ (char *)"main",(char *)"\\block_length(q) == size",59);
}
__e_acsl_full_init((void *)(& q));
q += 4;
/*@ assert \block_length(q) ≡ size; */
- {
- unsigned long __gen_e_acsl_block_length_23;
- __gen_e_acsl_block_length_23 = __e_acsl_block_length((void *)q);
- __e_acsl_assert(__gen_e_acsl_block_length_23 == size,(char *)"Assertion",
- (char *)"main",(char *)"\\block_length(q) == size",56);
- }
- /*@ assert \block_length(&ZERO) ≡ 0; */
- {
- unsigned long __gen_e_acsl_block_length_24;
- __gen_e_acsl_block_length_24 = __e_acsl_block_length((void *)(& ZERO));
- __e_acsl_assert(__gen_e_acsl_block_length_24 == 0UL,(char *)"Assertion",
- (char *)"main",(char *)"\\block_length(&ZERO) == 0",60);
- }
- /*@ assert \block_length(&zero) ≡ 0; */
{
unsigned long __gen_e_acsl_block_length_25;
- __gen_e_acsl_block_length_25 = __e_acsl_block_length((void *)(& zero));
- __e_acsl_assert(__gen_e_acsl_block_length_25 == 0UL,(char *)"Assertion",
- (char *)"main",(char *)"\\block_length(&zero) == 0",61);
+ __gen_e_acsl_block_length_25 = __e_acsl_block_length((void *)q);
+ __e_acsl_assert(__gen_e_acsl_block_length_25 == size,(char *)"Assertion",
+ (char *)"main",(char *)"\\block_length(q) == size",61);
}
__retres = 0;
__e_acsl_delete_block((void *)(& ZERO));
__e_acsl_delete_block((void *)(& PA));
__e_acsl_delete_block((void *)(A));
- __e_acsl_delete_block((void *)(& zero));
__e_acsl_delete_block((void *)(& q));
__e_acsl_delete_block((void *)(& p));
__e_acsl_delete_block((void *)(& pi));
@@ -248,6 +247,7 @@ int main(void)
__e_acsl_delete_block((void *)(& l));
__e_acsl_delete_block((void *)(& pa));
__e_acsl_delete_block((void *)(a));
+ __e_acsl_delete_block((void *)(& zero));
__e_acsl_memory_clean();
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_literal_string.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_literal_string.c
index 531162cdcd18536c09ddd048013571191a720e4e..6bb6497d113ff21faddbc425f4bbc820be4c68af 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_literal_string.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_literal_string.c
@@ -1,4 +1,6 @@
/* Generated by Frama-C */
+char *__gen_e_acsl_literal_string_6;
+char *__gen_e_acsl_literal_string_5;
char *__gen_e_acsl_literal_string;
char *__gen_e_acsl_literal_string_4;
char *__gen_e_acsl_literal_string_3;
@@ -28,9 +30,21 @@ char *S = (char *)"foo";
char *S2 = (char *)"foo2";
int IDX = 1;
int G2 = 2;
+char const *s_str = "the cat";
+char const *l_str = "the dog and the cat";
char *U = (char *)"baz";
void __e_acsl_globals_init(void)
{
+ __gen_e_acsl_literal_string_6 = "the dog and the cat";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_6,
+ sizeof("the dog and the cat"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_6);
+ __e_acsl_readonly((void *)__gen_e_acsl_literal_string_6);
+ __gen_e_acsl_literal_string_5 = "the cat";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_5,
+ sizeof("the cat"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_5);
+ __e_acsl_readonly((void *)__gen_e_acsl_literal_string_5);
__gen_e_acsl_literal_string = "ss";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string,sizeof("ss"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string);
@@ -47,6 +61,10 @@ void __e_acsl_globals_init(void)
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,sizeof("bar"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
__e_acsl_readonly((void *)__gen_e_acsl_literal_string_2);
+ __e_acsl_store_block((void *)(& l_str),8UL);
+ __e_acsl_full_init((void *)(& l_str));
+ __e_acsl_store_block((void *)(& s_str),8UL);
+ __e_acsl_full_init((void *)(& s_str));
__e_acsl_store_block((void *)(& S2),8UL);
__e_acsl_full_init((void *)(& S2));
__e_acsl_store_block((void *)(& S),8UL);
@@ -72,23 +90,23 @@ int main(void)
sizeof(char));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(S+(unsigned long)G2)",
- 22);
+ 25);
__e_acsl_assert(*(S + (unsigned long)G2) == 'o',(char *)"Assertion",
- (char *)"main",(char *)"*(S+G2) == \'o\'",22);
+ (char *)"main",(char *)"*(S+G2) == \'o\'",25);
}
/*@ assert \initialized(S); */
{
int __gen_e_acsl_initialized;
__gen_e_acsl_initialized = __e_acsl_initialized((void *)S,sizeof(char));
__e_acsl_assert(__gen_e_acsl_initialized,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(S)",23);
+ (char *)"main",(char *)"\\initialized(S)",26);
}
/*@ assert \valid_read(S2); */
{
int __gen_e_acsl_valid_read_2;
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)S2,sizeof(char));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"Assertion",
- (char *)"main",(char *)"\\valid_read(S2)",24);
+ (char *)"main",(char *)"\\valid_read(S2)",27);
}
/*@ assert ¬\valid(SS); */
{
@@ -103,10 +121,14 @@ int main(void)
}
else __gen_e_acsl_and = 0;
__e_acsl_assert(! __gen_e_acsl_and,(char *)"Assertion",(char *)"main",
- (char *)"!\\valid(SS)",25);
+ (char *)"!\\valid(SS)",28);
}
f();
+ s_str ++;
+ l_str ++;
__retres = 0;
+ __e_acsl_delete_block((void *)(& l_str));
+ __e_acsl_delete_block((void *)(& s_str));
__e_acsl_delete_block((void *)(& S2));
__e_acsl_delete_block((void *)(& S));
__e_acsl_delete_block((void *)(& T));
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 6163e18aed41bd79f62b36b9dd58cf18c83d0cec..393c8fffed987632fb7e92d4611014dc645c9926 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -563,21 +563,6 @@ and at_to_exp env t_opt label e =
That is this variable which is the resulting expression.
ACSL typing rule ensures that the type of this variable is the same as
the one of [e]. *)
- let must_model_new_var e =
- let res = ref false in
- let o = object
- inherit Cil.nopCilVisitor
- method !vlval (host, _) = match host with
- | Var v ->
- if Mmodel_analysis.old_must_model_vi (Env.get_behavior env) v then
- res := true;
- Cil.SkipChildren
- | Mem _ ->
- Cil.DoChildren
- end in
- ignore (Cil.visitCilExpr o e);
- !res
- in
let loc = Stmt.loc stmt in
let res_v, res, new_env =
Env.new_var
@@ -587,8 +572,7 @@ and at_to_exp env t_opt label e =
env
t_opt
(Cil.typeOf e)
- (fun v _ ->
- if must_model_new_var e then [ Misc.mk_store_stmt v ] else [])
+ (fun _ _ -> [])
in
let env_ref = ref new_env in
(* visitor modifying in place the labeled statement in order to store [e]