Skip to content
Snippets Groups Projects
Commit ed926e66 authored by Boris Yakobowski's avatar Boris Yakobowski
Browse files

Merge remote-tracking branch 'origin/master' into feature/boris/monomorphize-logic 

Conflicts:
	misc.ml
	quantif.ml
parents c49edb0b e5c9ad5e
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 179 additions and 842 deletions
src/plugins/e-acsl/.gitignore
+ 0
− 1
View file @ ed926e66
......@@ -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
src/plugins/e-acsl/Makefile.in
+ 0
− 30
View file @ ed926e66
......@@ -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 #
################################################
......
src/plugins/e-acsl/benchmarking/examples/plotting/dat/barplot.dat deleted 100644 → 0
+ 0
− 4
View file @ c49edb0b
Benchmark No-model Segment-model Bittree-model
grep 2 4.4 18
sed 3 9 16
diff 4 9.3 7.3
src/plugins/e-acsl/benchmarking/examples/plotting/dat/lineplot.dat deleted 100644 → 0
+ 0
− 11
View file @ c49edb0b
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
src/plugins/e-acsl/benchmarking/examples/plotting/sample-plot.sh deleted 100755 → 0
+ 0
− 32
View file @ c49edb0b
#!/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
src/plugins/e-acsl/benchmarking/tools/bm.gnuplot deleted 100755 → 0
+ 0
− 180
View file @ c49edb0b
#!/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
src/plugins/e-acsl/benchmarking/tools/fc-time.c deleted 100644 → 0
+ 0
− 467
View file @ c49edb0b
/* 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;
}
src/plugins/e-acsl/configure.ac
+ 7
− 2
View file @ ed926e66
......@@ -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")
src/plugins/e-acsl/env.ml
+ 1
− 1
View file @ ed926e66
......@@ -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
......
src/plugins/e-acsl/main.ml
+ 3
− 3
View file @ ed926e66
......@@ -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 () ->
......
src/plugins/e-acsl/misc.ml
+ 1
− 1
View file @ ed926e66
......@@ -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 =
......
src/plugins/e-acsl/quantif.ml
+ 3
− 3
View file @ ed926e66
......@@ -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 ->
......
src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+ 10
− 8
View file @ ed926e66
......@@ -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 \
......
src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_api.h
+ 4
− 0
View file @ ed926e66
......@@ -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;
......
src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
+ 117
− 17
View file @ ed926e66
......@@ -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
src/plugins/e-acsl/tests/bts/bts1390.c
+ 5
− 6
View file @ ed926e66
......@@ -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;
......
src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
+ 3
− 1
View file @ ed926e66
......@@ -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);
src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
+ 0
− 9
View file @ ed926e66
......@@ -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);
}
......
src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
+ 0
− 6
View file @ ed926e66
......@@ -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);
{
......
src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
+ 25
− 60
View file @ ed926e66
......@@ -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;
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment