diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 67badd902929239d8d609c12369c336bd1f4779d..ee12b9ccfad66a1cdbf93dfaa9dafb1ff3cfa4f5 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -178,53 +178,6 @@ e-acsl-distclean::
then $(MAKE) -s -C$(EACSL_GMP_DIR) distclean; \
fi
-################################################
-# E-ACSL Runtime Library #
-################################################
-
-EACSL_SHARE := $(EACSL_PLUGIN_DIR)/share/e-acsl
-
-EACSL_RTL_SRC = $(wildcard $(EACSL_SHARE)/*.[ch] $(EACSL_SHARE)/*/*.[ch])
-
-RTLFLAGS = -std=c99 -Wall -Wno-unused -Wno-attributes -I$(EACSL_SHARE) \
- -fno-omit-frame-pointer -DE_ACSL_BUILTINS -Wno-nonnull
-
-RTLOPT = $(RTLFLAGS) -O2
-RTLDEBUG = $(RTLFLAGS) -DE_ACSL_DEBUG -g3 -O0
-
-# Build a static E-ACSL library
- # $1 Compile-time flags
- # $2 Library path
- # $3 Source file
-MKRTL = \
- echo "Making $2"; \
- object=$$(basename -s .a $2).o && \
- echo ' CC $3' && \
- $(CC) $1 -c -o$$object $3 && \
- echo ' AR $2' && \
- $(AR) crus $2 $$object && \
- $(RM) -f $$object && \
- ranlib $2
-
-$(EACSL_LIBDIR)/libeacsl-rtl-%.a: $(EACSL_SHARE)/%_model/e_acsl_*_mmodel.c $(EACSL_RTL_SRC) $(EACSL_JEMALLOC_LIB) $(EACSL_GMP_LIB)
- $(call MKRTL, $(RTLOPT), $@, $<)
-
-$(EACSL_LIBDIR)/libeacsl-rtl-%-dbg.a: $(EACSL_SHARE)/%_model/e_acsl_*_mmodel.c $(EACSL_RTL_SRC) $(EACSL_JEMALLOC_LIB) $(EACSL_GMP_LIB)
- $(call MKRTL, $(RTLDEBUG), $@, $<)
-
-EACSL_RTL = \
- $(EACSL_LIBDIR)/libeacsl-rtl-bittree.a \
- $(EACSL_LIBDIR)/libeacsl-rtl-segment.a \
- $(EACSL_LIBDIR)/libeacsl-rtl-bittree-dbg.a \
- $(EACSL_LIBDIR)/libeacsl-rtl-segment-dbg.a
-
-clean::
- $(PRINT_RM) E-ACSL runtime library
- $(RM) $(EACSL_RTL)
- $(RM) $(EACSL_LIBDIR)/*.o
-
-all:: $(EACSL_RTL)
-
############
# Cleaning #
############
@@ -371,10 +324,14 @@ install::
$(MKDIR) $(FRAMAC_DATADIR)/e-acsl
$(CP) $(E_ACSL_DIR)/share/e-acsl/*.[ch] $(FRAMAC_DATADIR)/e-acsl
$(MKDIR) $(FRAMAC_DATADIR)/e-acsl/bittree_model \
- $(FRAMAC_DATADIR)/e-acsl/glibc
+ $(FRAMAC_DATADIR)/e-acsl/segment_model \
+ $(FRAMAC_DATADIR)/e-acsl/glibc
$(CP) $(E_ACSL_DIR)/share/e-acsl/bittree_model/* \
- $(FRAMAC_DATADIR)/e-acsl/bittree_model
- $(CP) $(E_ACSL_DIR)/share/e-acsl/glibc/* $(FRAMAC_DATADIR)/e-acsl/glibc
+ $(FRAMAC_DATADIR)/e-acsl/bittree_model
+ $(CP) $(E_ACSL_DIR)/share/e-acsl/segment_model/* \
+ $(FRAMAC_DATADIR)/e-acsl/segment_model
+ $(CP) $(E_ACSL_DIR)/share/e-acsl/glibc/* \
+ $(FRAMAC_DATADIR)/e-acsl/glibc
$(PRINT_INSTALL) E-ACSL manuals
$(MKDIR) $(FRAMAC_DATADIR)/manuals
$(CP) $(E_ACSL_DIR)/doc/manuals/e-acsl.pdf \
diff --git a/src/plugins/e-acsl/misc.ml b/src/plugins/e-acsl/misc.ml
index 5c6d57f6a4e517c9c31e35cd11c0edd5a4aae949..a1e78558beae129f7a85f2585ae7f97bfeb01764 100644
--- a/src/plugins/e-acsl/misc.ml
+++ b/src/plugins/e-acsl/misc.ml
@@ -63,25 +63,29 @@ let mk_call ~loc ?result fname args =
in
let f = Cil.evar ~loc vi in
vi.vreferenced <- true;
- let ty_params = match vi.vtype with
- | TFun(_, Some l, _, _) -> l
- | _ -> assert false
- in
- let args =
+ let make_args args ty_params =
List.map2
(fun (_, ty, _) arg ->
- let e =
- match ty, Cil.unrollType (Cil.typeOf arg), arg.enode with
- | TPtr _, TArray _, Lval lv -> Cil.new_exp ~loc (StartOf lv)
- | TPtr _, TArray _, _ -> assert false
- | _, _, _ -> arg
- in
- Cil.mkCast ~force:false ~newt:ty ~e)
+ let e =
+ match ty, Cil.unrollType (Cil.typeOf arg), arg.enode with
+ | TPtr _, TArray _, Lval lv -> Cil.new_exp ~loc (StartOf lv)
+ | TPtr _, TArray _, _ -> assert false
+ | _, _, _ -> arg
+ in
+ Cil.mkCast ~force:false ~newt:ty ~e)
ty_params
args
in
+ let args = match vi.vtype with
+ | TFun(_, Some params, _, _) -> make_args args params
+ | TFun(_, None, _, _) -> []
+ | _ -> assert false
+ in
Cil.mkStmtOneInstr ~valid_sid:true (Call(result, f, args, loc))
+let mk_deref ~loc lv =
+ Cil.new_exp ~loc (Lval(Mem(lv), NoOffset))
+
type annotation_kind =
| Assertion
| Precondition
@@ -125,6 +129,9 @@ let strip_prefix p s =
let is_generated_varinfo vi =
startswith e_acsl_gen_prefix vi.vname
+let is_generated_literal_string_varinfo vi =
+ startswith (e_acsl_gen_prefix ^ "literal_string") vi.vname
+
let is_library_name name =
startswith e_acsl_api_prefix name
@@ -197,23 +204,12 @@ let result_vi kf = match result_lhost kf with
(** {2 Handling the E-ACSL's C-libraries, part II} *)
(* ************************************************************************** *)
-let mk_debug_mmodel_stmt stmt =
- if Options.debug_atleast 1
- && Options.is_debug_key_enabled Options.dkey_analysis
- then
- let debug = mk_call ~loc:(Stmt.loc stmt) (mk_api_name "memory_debug") [] in
- Cil.mkStmt ~valid_sid:true (Block (Cil.mkBlock [ stmt; debug]))
- else
- stmt
-
let mk_full_init_stmt ?(addr=true) vi =
let loc = vi.vdecl in
- let stmt = match addr, Cil.unrollType vi.vtype with
+ match addr, Cil.unrollType vi.vtype with
| _, TArray(_,Some _, _, _) | false, _ ->
mk_call ~loc (mk_api_name "full_init") [ Cil.evar ~loc vi ]
| _ -> mk_call ~loc (mk_api_name "full_init") [ Cil.mkAddrOfVi vi ]
- in
- mk_debug_mmodel_stmt stmt
let mk_initialize ~loc (host, offset as lv) = match host, offset with
| Var _, NoOffset -> mk_call ~loc
@@ -229,14 +225,12 @@ let mk_named_store_stmt name ?str_size vi =
let ty = Cil.unrollType vi.vtype in
let loc = vi.vdecl in
let store = mk_call ~loc (mk_api_name name) in
- let stmt = match ty, str_size with
+ match ty, str_size with
| TArray(_, Some _,_,_), None ->
store [ Cil.evar ~loc vi ; Cil.sizeOf ~loc ty ]
| TPtr(TInt(IChar, _), _), Some size -> store [ Cil.evar ~loc vi ; size ]
| _, None -> store [ Cil.mkAddrOfVi vi ; Cil.sizeOf ~loc ty ]
| _, Some _ -> assert false
- in
- mk_debug_mmodel_stmt stmt
let mk_store_stmt ?str_size vi =
mk_named_store_stmt "store_block" ?str_size vi
@@ -246,17 +240,14 @@ let mk_duplicate_store_stmt ?str_size vi =
let mk_delete_stmt vi =
let loc = vi.vdecl in
- let stmt = match Cil.unrollType vi.vtype with
+ match Cil.unrollType vi.vtype with
| TArray(_, Some _, _, _) ->
mk_call ~loc (mk_api_name "delete_block") [ Cil.evar ~loc vi ]
| _ -> mk_call ~loc (mk_api_name "delete_block") [ Cil.mkAddrOfVi vi ]
- in
- mk_debug_mmodel_stmt stmt
-let mk_readonly vi =
+let mk_mark_readonly vi =
let loc = vi.vdecl in
- let stmt = mk_call ~loc (mk_api_name "readonly") [ Cil.evar ~loc vi ] in
- mk_debug_mmodel_stmt stmt
+ mk_call ~loc (mk_api_name "mark_readonly") [ Cil.evar ~loc vi ]
(* ************************************************************************** *)
(** {2 Other stuff} *)
@@ -279,6 +270,29 @@ let cty = function
| Ctype ty -> ty
| lty -> Options.fatal "Expecting a C type. Got %a" Printer.pp_logic_type lty
+let rec ptr_index ?(loc=Location.unknown) ?(index=(Cil.zero loc)) exp =
+ let arith_op = function
+ | MinusPI -> MinusA
+ | PlusPI -> PlusA
+ | IndexPI -> PlusA
+ | _ -> assert false in
+ match exp.enode with
+ | BinOp(op, lhs, rhs, _) ->
+ (match op with
+ (* Pointer arithmetic: split pointer and integer parts *)
+ | MinusPI | PlusPI | IndexPI ->
+ let index = Cil.mkBinOp exp.eloc (arith_op op) index rhs in
+ ptr_index ~index lhs
+ (* Other arithmetic: treat the whole expression as pointer address *)
+ | MinusPP | PlusA | MinusA | Mult | Div | Mod
+ | BAnd | BXor | BOr | Shiftlt | Shiftrt
+ | Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr -> (exp, index))
+ | CastE _ -> ptr_index ~loc ~index (Cil.stripCasts exp)
+ | Info (exp, _) -> ptr_index ~loc ~index exp
+ | Const _ | StartOf _ | AddrOf _ | Lval _ | UnOp _ -> (exp, index)
+ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _
+ -> assert false
+
(*
Local Variables:
compile-command: "make"
diff --git a/src/plugins/e-acsl/misc.mli b/src/plugins/e-acsl/misc.mli
index e9de1d3662c1aae4f9ea27c5e320add1ace87d82..10a2a111be7c8d3101a0eb0db7705ca7a8fde82d 100644
--- a/src/plugins/e-acsl/misc.mli
+++ b/src/plugins/e-acsl/misc.mli
@@ -36,7 +36,8 @@ val mk_call: loc:Location.t -> ?result:lval -> string -> exp list -> stmt
such a function or if these functions were never registered (only possible
when using E-ACSL through its API. *)
-val mk_debug_mmodel_stmt: stmt -> stmt
+val mk_deref: loc:Location.t -> exp -> exp
+(** Make a dereference of an expression *)
type annotation_kind =
| Assertion
@@ -75,7 +76,7 @@ val mk_duplicate_store_stmt: ?str_size:exp -> varinfo -> stmt
val mk_delete_stmt: varinfo -> stmt
val mk_full_init_stmt: ?addr:bool -> varinfo -> stmt
val mk_initialize: loc:location -> lval -> stmt
-val mk_readonly: varinfo -> stmt
+val mk_mark_readonly: varinfo -> stmt
(* ************************************************************************** *)
(** {2 Other stuff} *)
@@ -91,6 +92,11 @@ val reorder_ast: unit -> unit
val cty: logic_type -> typ
(* Assume that the logic type is indeed a C type. Just return it. *)
+val ptr_index: ?loc:location -> ?index:exp -> exp
+ -> Cil_types.exp * Cil_types.exp
+(** Split pointer-arithmetic expression of the type `p + i` into its
+pointer and integer parts. *)
+
(* ************************************************************************** *)
(** {2 Handling prefixes of generated library functions and variables} *)
(* ************************************************************************** *)
@@ -113,6 +119,10 @@ val is_generated_varinfo: varinfo -> bool
generated by E-ACSL. This is done by checking whether the name of the
varinfo has been generated using [mk_gen_name function]. *)
+val is_generated_literal_string_varinfo: varinfo -> bool
+(** Same as [is_generated_varinfo] but indicates that varinfo is a local
+ variable which replaced a literal string. *)
+
val is_generated_kf: kernel_function -> bool
(** Same as [is_generated_varinfo] but for kernel functions *)
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index 89405b75fda5d4888813fc957a598e492975ee56..fd3343162679b54d84755f5fb3435894d1928b90 100755
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
@@ -149,41 +149,20 @@ rte_options() {
return 0
}
-# Locate available E-ACSL memory models
-# - If no arguments are given then print the names of all memory models
-# available in this distribution of E-ACSL.
-# - If an argument is specified then it is assumed to be the name of a memory
-# model. In this case the following function prints the full path to a static
-# library representing this memory model.
-mmodel_lib() {
- local rtfeature=""
+# Output -D flags enabling a given E_ACSL memory model
+eacsl_mmodel() {
+ local model="$1"
+
+ case $model in
+ bittree) flags="-DE_ACSL_BITTREE_MMODEL" ;;
+ segment) flags="-DE_ACSL_SEGMENT_MMODEL" ;;
+ *) error "Memory model '$model' is not available in this distribution" ;;
+ esac
if [ -n "$OPTION_RT_DEBUG" ]; then
- rtfeature="-dbg"
- OPTION_CFLAGS="$OPTION_CFLAGS -O0 -fno-omit-frame-pointer"
- else
- OPTION_CFLAGS="$OPTION_CFLAGS -O2"
- fi
-
- # Supported models
- local models="segment bittree"
-
- if [ -n "$1" ]; then
- local modelname="$(echo $models | tr ' ' '\n' | grep "^$1$")"
- local modelpath="$(realpath "$LIBDIR/libeacsl-rtl-$modelname$rtfeature.a" 2>/dev/null)"
-
- # Bail if the name of the specified memory model does not match any of the
- # supported ones
- if [ -z "$modelname" ]; then
- error "Memory model '$1' is not available in this distribution"
- fi
- # Bail if the library for a specified memory model is not found
- if [ -z "$modelpath" ]; then
- error "Library '$modelpath' not found"
- fi
- echo $modelpath
- else
- echo $models
+ flags="$flags -DE_ACSL_DEBUG"
fi
+ local extra="-DE_ACSL_IDENTIFY"
+ echo $flags $extra
}
# Check if the following tools are GNU and abort otherwise
@@ -220,13 +199,16 @@ OPTION_FRAMA_STDLIB="-no-frama-c-stdlib" # Use Frama-C stdlib
OPTION_FULL_MMODEL= # Instrument as much as possible
OPTION_GMP= # Use GMP integers everywhere
OPTION_FRAMAC_CPP_EXTRA="-D__NO_CTYPE" # Extra CPP flags for Frama-C*
-OPTION_EACSL_MMODELS="bittree" # Memory model used
+OPTION_EACSL_MMODELS="segment" # Memory model used
OPTION_EACSL_SHARE= # Custom E-ACSL share directory
OPTION_INSTRUMENTED_ONLY= # Do not compile original code
OPTION_RTE= # Enable assertion generation
OPTION_CHECK= # Check AST integrity
OPTION_RTE_SELECT= # Generate assertions for these functions only
+# Supported memory model names
+SUPPORTED_MMODELS="bittree,segment"
+
manpage() {
printf "e-acsl-gcc.sh - instrument and compile C files with E-ACSL
Usage: e-acsl-gcc.sh [options] files
@@ -448,7 +430,7 @@ do
# Print names of the supported memody models.
--print-mmodels)
shift;
- mmodel_lib
+ echo $SUPPORTED_MMODELS
exit 0
;;
esac
@@ -518,15 +500,18 @@ if [ -n "$OPTION_EACSL_SHARE" ]; then
EACSL_SHARE="$OPTION_EACSL_SHARE"
fi
-# Once EACSL_SHARE is defined check the memory models provided at inputs
-for mod in $OPTION_EACSL_MMODELS; do
- mmodel_lib $mod >/dev/null
-done
+# Select optimization flags for both instrumented and noon-instrumented code
+# compilation
+if [ -n "$OPTION_RT_DEBUG" ]; then
+ OPT_CFLAGS="-g3 -O0 -fno-omit-frame-pointer"
+else
+ OPT_CFLAGS="-g -O2"
+fi
# Gcc and related flags
CC="$OPTION_CC"
CFLAGS="$OPTION_CFLAGS
- -std=c99 $GCCMACHDEP -g3
+ -std=c99 $GCCMACHDEP $OPT_CFLAGS
-fno-builtin -fno-merge-constants
-Wall \
-Wno-long-long \
@@ -618,19 +603,21 @@ if [ -n "$OPTION_COMPILE" ]; then
fi
# Compile and link E-ACSL-instrumented file with all models specified
- for mod in $OPTION_EACSL_MMODELS; do
+ for model in $OPTION_EACSL_MMODELS; do
# If multiple models are specified then the generated executable
# is appended a '-MODEL' suffix, where MODEL is the name of the memory
# model used
if ! [ "`echo $OPTION_EACSL_MMODELS | wc -w`" = 1 ]; then
- OUTPUT_EXEC="$EACSL_OUTPUT_EXEC-$mod"
+ OUTPUT_EXEC="$EACSL_OUTPUT_EXEC-$model"
else
OUTPUT_EXEC="$EACSL_OUTPUT_EXEC"
fi
# Sources of the selected memory model
- EACSL_RTL=$(mmodel_lib "$mod")
+ EACSL_RTL="$EACSL_SHARE/e_acsl_mmodel.c"
+ EACSL_MMODEL="$(eacsl_mmodel $model)"
($OPTION_ECHO;
$CC \
+ $EACSL_MMODEL \
$CFLAGS $CPPFLAGS \
$EACSL_CFLAGS $EACSL_CPPFLAGS \
-o "$OUTPUT_EXEC" \
diff --git a/src/plugins/e-acsl/scripts/testrun.sh b/src/plugins/e-acsl/scripts/testrun.sh
index 1365313c02e834d3813ffaaf876b0ec064d0d2c9..69407bc96ac0dc4c21699daf62c692f0e5d6ec4f 100755
--- a/src/plugins/e-acsl/scripts/testrun.sh
+++ b/src/plugins/e-acsl/scripts/testrun.sh
@@ -42,7 +42,8 @@
# * $ROOT/test/runtime/addrOf.c
# $3 - if specified, re-run test sequence with -e-acsl-gmp-only flag
# $4 - extra flags for a `e-acsl-gcc.sh` run
-# $5 - if specified print extra messages and retain log files (DEBUG option)
+# $5 - names of memory models to use
+# $6 - if specified print extra messages and retain log files (DEBUG option)
set -e
@@ -50,9 +51,11 @@ TEST="$1" # Base name of the test file
PREFIX="$2" # Test suite directory (e.g., runtime)
GMP="$3" # Whether to issue an additional run with -e-acsl-gmp-only
EXTRA="$4" # Extra e-acsl-gcc.sh flags
-DEBUG="$5" # Debug option
+MODELS="$5" # Specify models
+DEBUG="$6" # Debug option
EACSLGCC="$(dirname $0)/e-acsl-gcc.sh $EXTRA" # E-ACSL wrapper script
+MODELS=${5-"segment bittree"} # Memory models to use (unless specified)
ROOTDIR="`readlink -f $(dirname $0)/../`" # Root directory of the repository
TESTDIR="$ROOTDIR/tests/$PREFIX" # Test suite directory
@@ -90,6 +93,8 @@ error() {
exit 1
}
+debug "Test: $PREFIX/$TEST with $MODELS"
+
# Do a clean-up on exit
trap "clean" EXIT HUP INT QUIT TERM
@@ -118,11 +123,6 @@ run_test() {
local oexec=$OUT.$RUNS.out # Generated executable name
local oexeclog=$LOG.$RUNS.rlog # Log for executable output
local extra="$1" # Additional arguments to e-acsl-gcc.sh
- MODELS="$($EACSLGCC $extra --print-mmodels)" # Supported memory models
-
- # e-acsl-gcc.sh reports models as space-separated string. Make a
- # comma-separated one otherwise the following does not work
- MODELSTR="$(echo $MODELS | tr ' ' ',')"
# Command for instrumenting the source file
COMMAND="$EACSLGCC $TESTFILE --ocode=$ocode --logfile=$logfile $extra"
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 e62516c2fa143a86ea7cc919724857bfa3c95a7b..746cc75c6c26d0b95923051c5a6b5fe257020207 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
@@ -26,17 +26,6 @@
* on Patricia Trie. See e_acsl_mmodel_api.h for details.
***************************************************************************/
-#ifndef E_ACSL_BITTREE_MMODEL
-#define E_ACSL_BITTREE_MMODEL
-
-#include "e_acsl_string.h"
-#include "e_acsl_printf.h"
-#include "e_acsl_bits.h"
-#include "e_acsl_assert.h"
-#include "e_acsl_debug.h"
-#include "e_acsl_malloc.h"
-#include "e_acsl_safe_locations.h"
-#include "e_acsl_mmodel_api.h"
#include "e_acsl_bittree.h"
/**************************/
@@ -154,7 +143,7 @@ static void full_init (void * ptr) {
}
/* mark a block as read-only */
-static void readonly(void * ptr) {
+static void mark_readonly(void * ptr) {
bt_block * tmp;
if (ptr == NULL)
return;
@@ -212,22 +201,29 @@ static size_t block_length(void* ptr) {
return tmp->size;
}
+static int allocated(void* ptr, size_t size, void *ptr_base) {
+ bt_block * blk = bt_find(ptr);
+ bt_block * blk_base = bt_find(ptr_base);
+ if (blk == NULL || blk_base == NULL || blk->ptr != blk_base->ptr)
+ return false;
+ return (blk->size - ((size_t)ptr - blk->ptr) >= size);
+}
+
/* return whether the size bytes of ptr are readable/writable */
-static int valid(void* ptr, size_t size) {
- if(ptr == NULL)
+static int valid(void* ptr, size_t size, void *ptr_base, void *addr_of_base) {
+ /* Many similarities with allocated (so far at least), but it is better
+ * to use this tandalone definition, otherwise the block needs to be looked
+ * up twice */
+ bt_block * blk = bt_find(ptr);
+ bt_block * blk_base = bt_find(ptr_base);
+ if (blk == NULL || blk_base == NULL || blk->ptr != blk_base->ptr)
return false;
- bt_block * tmp = bt_find(ptr);
- return (tmp == NULL) ? false :
- (tmp->size - ((size_t)ptr - tmp->ptr ) >= size && !tmp->is_readonly);
+ return (blk->size - ((size_t)ptr - blk->ptr) >= size && !blk->is_readonly);
}
/* return whether the size bytes of ptr are readable */
-static int valid_read(void* ptr, size_t size) {
- if(ptr == NULL)
- return false;
- bt_block * tmp = bt_find(ptr);
- return (tmp == NULL) ?
- false : (tmp->size - ((size_t)ptr - tmp->ptr) >= size);
+static int valid_read(void* ptr, size_t size, void *ptr_base, void *addr_of_base) {
+ return allocated(ptr, size, ptr_base);
}
/* return the base address of the block containing ptr */
@@ -394,7 +390,7 @@ static int bittree_posix_memalign(void **memptr, size_t alignment, size_t size)
return -1;
/* Make sure that the first argument to posix memalign is indeed allocated */
- vassert(valid(memptr, sizeof(void*)),
+ vassert(allocated((void*)memptr, sizeof(void*), (void*)memptr),
"\\invalid memptr in posix_memalign", NULL);
int res = native_posix_memalign(memptr, alignment, size);
@@ -447,7 +443,7 @@ static void* bittree_realloc(void* ptr, size_t size) {
/* allocate memory to store partial initialization */
tmp->init_ptr = native_calloc(1, nb);
/* carry out initialization of the old block */
- setbits(tmp->init_ptr, tmp->size);
+ setbits(tmp->size, tmp->init_ptr);
}
} else { /* contains initialized and uninitialized parts */
int nb = needed_bytes(size);
@@ -510,6 +506,7 @@ static void init_argv(int argc, char **argv) {
}
static void memory_init(int *argc_ref, char ***argv_ref, size_t ptr_size) {
+ identify_run();
arch_assert(ptr_size);
/* Tracking program arguments */
if (argc_ref)
@@ -593,7 +590,7 @@ public_alias(valid)
public_alias(block_length)
public_alias(initialized)
public_alias(freeable)
-public_alias(readonly)
+public_alias(mark_readonly)
/* Block initialization */
public_alias(initialize)
public_alias(full_init)
@@ -611,4 +608,3 @@ public_alias(store_block_debug)
public_alias(delete_block_debug)
#endif
/* }}} */
-#endif
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_bits.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_bits.h
index 436433f27de5fdadfa34a840a032c1beb857d89a..d04144a17b0e0d71fd1e867e9d4d7bb8e6f65fd1 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_bits.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_bits.h
@@ -30,6 +30,9 @@
* is, the implementation assumes that least significant bytes are stored at
* the highest memory addresses. In future support for big-endian/PDP byte
* orders should also be provided.
+ *
+ * CAUTION: As per above FIXME notice, all examples, macros and functions
+ * assume little-endian byte order.
***************************************************************************/
#ifndef E_ACSL_BITS
@@ -55,34 +58,27 @@
/* 64-bit type with all bits set to zeroes */
#define ZERO (~ONE)
-/* Set a given bit in a number to '1' (least-significant bit is at index zero). *
+/* Set a given bit in a number to '1' (least-significant bit is at index zero).
* Example:
- * int x = 0;
- * // x => 0000 0000 ...
- * bitset(0, x)
- * // x => 1000 0000 ...
- * bitset(7, x)
- * // x => 1000 0001 ... */
+ * int x = 0; // x => 0000 0000 ...
+ * bitset(0, x) // x => 1000 0000 ...
+ * bitset(7, x) // x => 1000 0001 ... */
#define setbit(_bit,_number) (_number |= 1 << _bit)
-/* Same as bitset but the bit is cleared (set of zero) */
+/* Same as bitset but the `_bit` bit is cleared (i.e., set of zero) */
#define clearbit(_bit, _number) (_number &= ~(1 << _bit))
-/* Evaluates to a true value if a given bit in a number is set to 1.
- * int x = 1;
- * // x => 1000 0000 ...
- * checkbit(0, x) // true
- * checkbit(1, x) // false */
+/* Evaluate to a non-zero value if a given bit in a number is set to 1.
+ * int x = 1; // x => 1000 0000 ...
+ * checkbit(0, x) // 1
+ * checkbit(1, x) // 0 */
#define checkbit(_bit, _number) ((_number >> _bit) & 1)
/* Toggle a given bit.
* Example:
- * int x = 4; (assume little-endian)
- * // x => 0010 0000 ...
- * togglebit(3, x);
- * // x => 0000 0000 ...
- * togglebit(3, x);
- * // x => 0010 0000 ... */
+ * int x = 4; // x => 0010 0000 ...
+ * togglebit(3, x); // x => 0000 0000 ...
+ * togglebit(3, x); // x => 0010 0000 ... */
#define togglebit(_bit, _number) (_number ^= 1 << _bit)
/* Set a given bit to a specified value (e.g., 0 or 1). */
@@ -91,24 +87,47 @@
/* Set up to 64 bits from left to right to ones.
* Example:
- * int x = 0;
- * // x => 00000000 00000000 00000000 00000000
- * setbits64(11, x)
- * // => 11111111 11100000 00000000 00000000
- * setbits64(65, x)
- * // => behaviour undefined */
+ * int x = 0; // x => 00000000 00000000 ...
+ * setbits64(11, x) // => 11111111 11100000 ...
+ * setbits64(64, x) // => behaviour undefined */
#define setbits64(_bits, _number) (_number |= ~(ONE << _bits))
+/* Set up to 64 bits from left to right to ones skiping `_skip` leftmost bits
+ * Example:
+ * int x = 0; // x => 00000000 00000000 ...
+ * setbits64(11, x, 2) // => 00111111 11111000 ...
+ * setbits64(64, x, 2) // => behaviour undefined */
+#define setbits64_skip(_bits, _number, _skip) \
+ (_number |= ~(ONE << _bits) << _skip)
+
+/* Evaluate to 1 if up to 64 bits from left to right in `_number` are set:
+ * Example:
+ * int x = 31; // x => 11111000 00000000 ...
+ * checkbits64(4, x) // => 1
+ * checkbits64(5, x) // => 1
+ * checkbits64(6, x) // => 0
+ * checkbits64(64, x) // => behaviour undefined */
+#define checkbits64(_bits, _number) \
+ ((_number & ~(ONE << _bits)) == (~(ONE << _bits)))
+
+/* Same as checkbits64 but with skipping `_skip` leftmost bits
+ * Example:
+ * int x = 124; // x => 00111100 00000000 ...
+ * checkbits64_skip(3, x, 2) // => 1
+ * checkbits64_skip(4, x, 2) // => 1
+ * checkbits64_skip(5, x, 2) // => 0
+ * checkbits64_skip(3, x, 1) // => 0
+ * checkbits64_skip(64, x, 0) // => behaviour undefined */
+#define checkbits64_skip(_bits, _number, _skip) \
+ ((_number & ~(ONE << _bits) << _skip) == (~(ONE << _bits) << _skip))
+
/* Same as `setbits64' but clear the bits (set to zeroes). */
#define clearbits64(_bits, _number) (_number &= ONE << _bits)
-/* Assume that `_number' is a 64-bit integral type.
- * Set `_bits' bits from right to the left starting from a 64-bit boundary.
+/* Set `_bits' bits from right to the left starting from a 64-bit boundary.
* Example:
- * long x = 0;
- * // x => ... 00000000 00000000 00000000 00000000
- * setbits64_right(10, x)
- * // x => ... 00000000 00000000 00000011 11111111 */
+ * long x = 0; // x => ... 00000000 00000000 00000000 00000000
+ * setbits64_right(10, x) // x => ... 00000000 00000000 00000011 11111111 */
#define setbits64_right(_bits, _number) (_number |= ~(ONE >> _bits))
/* Same as setbits64_right but clears bits (sets to zeroes) */
@@ -117,11 +136,9 @@
/* Set `size' bits starting from an address given by `ptr' to ones.
* Example:
* char a[4];
- * memset(a,0,4);
- * // => 00000000 00000000 00000000 00000000
- * setbits(&a, 11);
- * // => 11111111 11100000 00000000 00000000 */
-void setbits(void *ptr, size_t size) {
+ * memset(a,0,4); // => 00000000 00000000 00000000 00000000
+ * setbits(&a, 11); // => 11111111 11100000 00000000 00000000 */
+static inline void setbits(size_t size, void *ptr) {
size_t i;
int64_t *lp = (int64_t*)ptr;
for (i = 0; i < size/64; i++)
@@ -130,7 +147,7 @@ void setbits(void *ptr, size_t size) {
}
/* Same as `setbits' but clear the bits (set to zeroes). */
-void clearbits(void *ptr, size_t size) {
+static inline void clearbits(size_t size, void *ptr) {
size_t i;
int64_t *lp = (int64_t*)ptr;
for (i = 0; i < size/64; i++)
@@ -138,14 +155,23 @@ void clearbits(void *ptr, size_t size) {
clearbits64(size%64, *(lp+i));
}
+/* Same as `setbits' but clear the bits (set to zeroes). */
+static inline int checkbits(size_t size, void *ptr) {
+ size_t i;
+ int64_t *lp = (int64_t*)ptr;
+ for (i = 0; i < size/64; i++) {
+ if (*(lp+i) != ONE)
+ return 0;
+ }
+ return checkbits64(size%64, *(lp+i));
+}
+
/* Same as `setbits' but set the bits from right to left
* Example:
* char a[4];
- * memset(a,0,4);
- * // => 00000000 00000000 00000000 00000000
- * setbits_right(&a, 11);
- * // => 00000000 00000000 00000111 11111111 */
-void setbits_right(void *ptr, size_t size) {
+ * memset(a,0,4); // => 00000000 00000000 00000000 00000000
+ * setbits_right(&a, 11); // => 00000000 00000000 00000111 11111111 */
+static inline void setbits_right(size_t size, void *ptr) {
size_t i = 0;
int64_t *lp = (int64_t*)ptr - 1;
for (i = 0; i < size/64; i++)
@@ -154,7 +180,7 @@ void setbits_right(void *ptr, size_t size) {
}
/* Same as `setbits_right' but clear the bits (set to zeroes). */
-void clearbits_right(void *ptr, size_t size) {
+static inline void clearbits_right(size_t size, void *ptr) {
size_t i = 0;
int64_t *lp = (int64_t*)ptr - 1;
for (i = 0; i < size/64; i++)
@@ -162,4 +188,4 @@ void clearbits_right(void *ptr, size_t size) {
clearbits64_right(size%64, *(lp-i));
}
/* }}} */
-#endif
\ No newline at end of file
+#endif
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_debug.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_debug.h
index 8d2de060598d325b8a9516c9d24801ddb6a2b8ce..e41d7c1fa3053be47555dee6f42a7d309c329ece 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_debug.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_debug.h
@@ -25,6 +25,8 @@
* \brief Debug-level functions and macros
***************************************************************************/
+static void vabort(char *fmt, ...);
+
/* Stringification macros {{{ */
#ifndef E_ACSL_STRINGIFICATION
#define E_ACSL_STRINGIFICATION
@@ -40,7 +42,7 @@
/* Default location of the E_ACSL log file */
#ifndef E_ACSL_DEBUG_LOG
-# define E_ACSL_DEBUG_LOG /tmp/e-acsl.log
+# define E_ACSL_DEBUG_LOG -
#endif
/*! \brief Name of the debug log file */
@@ -62,14 +64,13 @@ static int dlog_fd = -1;
* - open file descriptor
* - add program arguments to the log */
static void initialize_report_file(int *argc, char ***argv) {
- // Redirect the log to stderr is just set to be defined or set to '-'
+ /* Redirect the log to stderr is just set to be defined or set to '-' */
if (!strcmp(dlog_name, "-") || !strcmp(dlog_name, "1")) {
dlog_fd = 2;
} else {
dlog_fd = open(dlog_name, O_WRONLY | O_CREAT | O_TRUNC |O_NONBLOCK
| O_NOCTTY, S_IRUSR | S_IWUSR | S_IRGRP | S_IWGRP | S_IROTH | S_IWOTH);
}
-
if (dlog_fd == -1)
vabort("Cannot open file descriptor for %s\n", dlog_name);
else {
@@ -89,13 +90,14 @@ static void initialize_report_file(int *argc, char ***argv) {
static int debug_stop_number = 0;
int getchar(void);
-#define STOP { \
- DLOG(" << ==================== " "Debug Stop Point %d in '%s' at %s:%d" \
- " ==================== >> ", \
+#define DSTOP { \
+ printf(" << ***** " "Debug Stop %d in '%s' at %s:%d" " ***** >> ", \
++debug_stop_number, __func__, __FILE__, __LINE__); \
- getchar(); \
+ getchar(); \
}
+
#else
+# define DSTOP
# define initialize_report_file(...)
# define DLOG(...)
# define DASSERT(_e)
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel.c b/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel.c
new file mode 100644
index 0000000000000000000000000000000000000000..2e437e4f4561972999916dc78ed0d0c9a32111bd
--- /dev/null
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel.c
@@ -0,0 +1,68 @@
+/**************************************************************************/
+/* */
+/* This file is part of the Frama-C's E-ACSL plug-in. */
+/* */
+/* Copyright (C) 2012-2015 */
+/* 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). */
+/* */
+/**************************************************************************/
+
+/*! ***********************************************************************
+ * \file e_acsl_memory_mmodel.c
+ * \brief Configuration macros and RTL assembly
+***************************************************************************/
+
+#include <sys/mman.h>
+#include <errno.h>
+#include <sys/resource.h>
+
+#include "e_acsl_string.h"
+#include "e_acsl_bits.h"
+#include "e_acsl_printf.h"
+#include "e_acsl_debug.h"
+#include "e_acsl_assert.h"
+#include "e_acsl_malloc.h"
+#include "e_acsl_safe_locations.h"
+
+/* Memory model:
+ * E_ACSL_BITTREE_MMODEL - use Patricia-trie (tree-based) memory model, or
+ * E_ACSL_SEGMENT_MMODEL - use segment-based (shadow) memory model
+ * Debug Features:
+ * E_ACSL_DEBUG - enable debug features in RTL
+ * Extra messages:
+ * E_ACSL_IDENTIFY - print a message showing run configuration
+*/
+
+/* Print basic configuration before each run */
+static void identify_run() {
+#ifdef E_ACSL_IDENTIFY
+ printf("/* ========================================================= */\n");
+ printf(" * E-ACSL instrumented run with: "
+#ifndef E_ACSL_DEBUG
+ "NO-"
+#endif
+ "DEBUG\n");
+ printf("/* ========================================================= */\n");
+#endif
+}
+
+#if defined E_ACSL_SEGMENT_MMODEL
+# include "segment_model/e_acsl_segment_mmodel.c"
+#elif defined E_ACSL_BITTREE_MMODEL
+# include "bittree_model/e_acsl_bittree_mmodel.c"
+#else
+# error "No EACSL memory model defined. Aborting compilation"
+#endif
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
index f19c4294999fd8276c77caa25075c4e87785026a..52351c9447bd3992d652ef49f156b8827d6abe2a 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
@@ -112,7 +112,7 @@ void __e_acsl_full_init(void * ptr)
/*! \brief Mark a memory block which start address is given by \p ptr as
* read-only. */
/*@ assigns \nothing; */
-void __e_acsl_readonly(void * ptr)
+void __e_acsl_mark_readonly(void * ptr)
__attribute__((FC_BUILTIN));
/* ****************** */
@@ -134,7 +134,7 @@ int __e_acsl_freeable(void * ptr)
/*@ ensures \result == 0 || \result == 1;
@ ensures \result == 1 ==> \valid(((char *)ptr)+(0..size-1));
@ assigns \result \from *(((char*)ptr)+(0..size-1)); */
-int __e_acsl_valid(void * ptr, size_t size)
+int __e_acsl_valid(void * ptr, size_t size, void *ptr_base, void *addr_of_base)
__attribute__((FC_BUILTIN));
/*! \brief Implementation of the \b \\valid_read predicate of E-ACSL.
@@ -144,7 +144,7 @@ int __e_acsl_valid(void * ptr, size_t size)
/*@ ensures \result == 0 || \result == 1;
@ ensures \result == 1 ==> \valid_read(((char *)ptr)+(0..size-1));
@ assigns \result \from *(((char*)ptr)+(0..size-1)); */
-int __e_acsl_valid_read(void * ptr, size_t size)
+int __e_acsl_valid_read(void * ptr, size_t size, void *ptr_base, void *addr_of_base)
__attribute__((FC_BUILTIN));
/*! \brief Implementation of the \b \\base_addr predicate of E-ACSL.
@@ -206,8 +206,7 @@ void __e_acsl_memory_init(int *argc_ref, char ***argv, size_t ptr_size)
size_t __e_acsl_get_heap_allocation_size(void)
__attribute__((FC_BUILTIN));
-/*! \brief A variable holding a cumulative size (in bytes) of tracked
- * heap allocation. */
+/*! \brief A variable holding a byte size of tracked heap allocation. */
extern size_t __e_acsl_heap_allocation_size;
/*@ predicate diffSize{L1,L2}(integer i) =
diff --git a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c
index 4699f2d81716064a64b8dc1578e6783eb36080dc..d5db5b65f366472ee1e70c6a9a16e4945e0f351d 100644
--- a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c
+++ b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c
@@ -26,21 +26,10 @@
* model. See e_acsl_mmodel_api.h for details.
***************************************************************************/
-#include <sys/mman.h>
-#include <errno.h>
-#include <sys/resource.h>
-
-static int valid(void * ptr, size_t size);
-static int valid_read(void * ptr, size_t size);
-
-#include "e_acsl_string.h"
-#include "e_acsl_bits.h"
-#include "e_acsl_printf.h"
-#include "e_acsl_assert.h"
-#include "e_acsl_debug.h"
-#include "e_acsl_malloc.h"
+static int valid(void*, size_t, void*, void*);
+static int valid_read(void*, size_t, void*, void*);
+
#include "e_acsl_shadow_layout.h"
-#include "e_acsl_safe_locations.h"
#include "e_acsl_segment_tracking.h"
#include "e_acsl_mmodel_api.h"
@@ -59,7 +48,7 @@ static void delete_block(void * ptr) {
}
static void * store_block_duplicate(void * ptr, size_t size) {
- if (valid_read(ptr, size))
+ if (allocated((uintptr_t)ptr, size, (uintptr_t)ptr))
delete_block(ptr);
shadow_alloca(ptr, size);
return ptr;
@@ -69,35 +58,26 @@ static void full_init(void * ptr) {
initialize(ptr, block_length(ptr));
}
-static void readonly(void * ptr) {
- mark_readonly((uintptr_t)ptr, block_length(ptr));
+static void mark_readonly(void * ptr) {
+ mark_readonly_region((uintptr_t)ptr, block_length(ptr));
}
/* ****************** */
/* E-ACSL annotations */
/* ****************** */
-static int valid(void * ptr, size_t size) {
+/** \brief Return 1 if a given memory location is read-only and 0 otherwise */
+static int readonly (void *ptr) {
uintptr_t addr = (uintptr_t)ptr;
- if (IS_ON_HEAP(addr))
- return heap_allocated(addr, size);
- else if (IS_ON_STACK(addr) || IS_ON_TLS(addr))
- return static_allocated(addr, size);
- else if (IS_ON_GLOBAL(addr))
- return static_allocated(addr, size) && !global_readonly(addr);
- else if (!IS_ON_VALID(addr))
- return 0;
- return 0;
+ return IS_ON_GLOBAL(addr) && global_readonly(addr) ? 1 : 0;
}
-static int valid_read(void * ptr, size_t size) {
- uintptr_t addr = (uintptr_t)ptr;
- TRY_SEGMENT(addr,
- return heap_allocated(addr, size),
- return static_allocated(addr, size));
- if (!IS_ON_VALID(addr))
- return 0;
- return 0;
+static int valid(void * ptr, size_t size, void *ptr_base, void *addr_of_base) {
+ return allocated((uintptr_t)ptr, size, (uintptr_t)ptr_base) && !readonly(ptr);
+}
+
+static int valid_read(void * ptr, size_t size, void *ptr_base, void *addr_of_base) {
+ return allocated((uintptr_t)ptr, size, (uintptr_t)ptr_base);
}
/*! NB: The implementation for this function can also be specified via
@@ -112,7 +92,7 @@ static void * segment_base_addr(void * ptr) {
/*! NB: Implementation of the following function can also be specified
* via \p block_length macro. A more direct approach via ::TRY_SEGMENT
- * is preffered for performance reasons. */
+ * is preferred for performance reasons. */
static size_t segment_block_length(void * ptr) {
TRY_SEGMENT(ptr,
return heap_info((uintptr_t)ptr, 'L'),
@@ -122,7 +102,7 @@ static size_t segment_block_length(void * ptr) {
/*! NB: Implementation of the following function can also be specified
* via \p offset macro. A more direct approach via ::TRY_SEGMENT
- * is preffered for performance reasons. */
+ * is preferred for performance reasons. */
static int segment_offset(void *ptr) {
TRY_SEGMENT(ptr,
return heap_info((uintptr_t)ptr, 'O'),
@@ -151,10 +131,9 @@ static void memory_init(int *argc_ref, char *** argv_ref, size_t ptr_size) {
initialize_report_file(argc_ref, argv_ref);
/* Lift stack limit to account for extra stack memory overhead. */
increase_stack_limit(get_stack_size()*2);
- /* Allocate and log shadow memory layout of the execution. */
+ /* Allocate and log shadow memory layout of the execution */
init_memory_layout(argc_ref, argv_ref);
- /* Make sure the layout holds and output it (only in debug mode) */
- DEBUG_PRINT_LAYOUT;
+ /* Make sure the layout holds */
DVALIDATE_SHADOW_LAYOUT;
/* Track program arguments. */
if (argc_ref && argv_ref)
@@ -163,7 +142,6 @@ static void memory_init(int *argc_ref, char *** argv_ref, size_t ptr_size) {
collect_safe_locations();
int i;
for (i = 0; i < safe_location_counter; i++) {
- DLOG("Safe location %lu\n", safe_locations[i].address, safe_locations[i].address + safe_locations[i].length);
void *addr = (void*)safe_locations[i].address;
uintptr_t len = safe_locations[i].length;
shadow_alloca(addr, len);
@@ -197,8 +175,8 @@ public_alias(valid_read)
public_alias(valid)
public_alias(initialized)
public_alias(freeable)
-public_alias(readonly)
/* Block initialization */
+public_alias(mark_readonly)
public_alias(initialize)
public_alias(full_init)
/* Memory state initialization */
diff --git a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
index ae8d30bfa8bf158d55a5ec3279c764b55aee3aa7..5c42f259ca2aeaebdb89e8e95f11408b8254a9d1 100644
--- a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
+++ b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
@@ -27,6 +27,28 @@
/* Segment settings and shadow values interpretation {{{ */
+/* This file implements segment-based and offset-based shadow memory models
+ * (shadow encodings) (see draft of the PLDI'17 paper).
+ *
+ * IMPORTANT: While the implementation of the offset-based encoding mostly
+ * follows the description given by the paper, there are differences in the
+ * segment-based encoding for tracking heap memory. Some of these differences
+ * are as follows:
+ * 1) Size of a heap segment is increased to 32 bytes
+ * 2) Heap meta-segments are no longer used, segment-based representation of
+ * a heap block considers only block segments, such that:
+ * - Lowest `intptr_t` bytes of each shadow segment tracking an application
+ * block store the base address of that block;
+ * - `intptr_t` bytes of the first segment following the initial `intptr_t`
+ * bytes store the length of the block. Note, the length is only stored
+ * by the first segment.
+ * 3) Per-byte initialization of application bytes is tracked via a disjoint
+ * shadow region, which maps one bit of shadow memory to a byte of
+ * application memory. Comments within this file often refer to a shadow
+ * region tracking application blocks by segments as to `block shadow`,
+ * and to the region tracking initialization as to `init shadow`.
+*/
+
/*! @brief Byte size of a heap segment.
* This size is potentially used as an argument to `memalign`.
* It SHOULD be a multiple of 2 and a multiple of a pointer size.
@@ -35,10 +57,7 @@
* size greater than 64 bytes. This is because presently some initialization
* functionality relies on the fact that initialization per segment can be set
* and/or evaluated using an 8-byte bitmask. */
-#define HEAP_SEGMENT 16
-
-/*! \brief Number of bytes required to represent initialization of a segment. */
-#define INIT_BYTES (HEAP_SEGMENT/8)
+#define HEAP_SEGMENT 32
/*! \brief Size (in bytes) of a long block on the stack. */
#define LONG_BLOCK 8
@@ -79,26 +98,30 @@
* offset at which to read meta-data is (51 - 48). */
#define LONG_BLOCK_INDEX_START 48
-/*! \brief Increase the size to a multiple of a segment size. */
-#define ALIGNED_SIZE(_s) \
- (_s + ((_s%HEAP_SEGMENT) ? (HEAP_SEGMENT - _s%HEAP_SEGMENT) : 0))
+/*! \brief Decrease _n to be a multiple of _m */
+#define ALIGN_LEFT(_n, _m) (_n - _n%_m)
-/*! \brief Given the size of a block return the number of segments
- * that represent that block in the heap shadow */
-#define BLOCK_SEGMENTS(_s) (ALIGNED_SIZE(_s)/HEAP_SEGMENT)
+/*! \brief Increase _n to be a multiple of _m */
+#define ALIGN_RIGHT(_n, _m) (_n + ((_n%_m) ? (_m - _n%_m) : 0))
+
+/*! \brief Heap shadow address aligned at a segment boundary */
+#define ALIGNED_HEAP_SHADOW(_addr) \
+ HEAP_SHADOW(ALIGN_LEFT(_addr,HEAP_SEGMENT))
/* \brief Maximal size_t value that does not cause overflow via addition
* when segment size is added. */
-const size_t max_allocated = SIZE_MAX - HEAP_SEGMENT;
+static const size_t max_allocated = ALIGN_LEFT(SIZE_MAX,HEAP_SEGMENT);
-/* \brief Return actual allocation size which takes into account meta-block.
- * In the present implementation it is the requested size of a heap block +
- * the size if a segment */
-#define ALLOC_SIZE(_s) (_s > 0 && _s < max_allocated ? _s + HEAP_SEGMENT : 0)
+/* \brief Return actual allocation size which takes into account aligned
+ * allocation. In the present implementation it is the requested size of
+ * a heap block aligned at a segment boundary */
+#define ALLOC_SIZE(_s) \
+ (_s < max_allocated ? ALIGN_RIGHT(_s, HEAP_SEGMENT) : 0)
-/*! \brief The number of bytes used to represent a heap block in its shadow.
- * In the current implementation it aligned size + meta-segment size */
-#define HEAP_SHADOW_BLOCK_SIZE(_s) ((BLOCK_SEGMENTS(_s) + 1)*HEAP_SEGMENT)
+/** \brief Evaluate to `true` if address _addr belongs to a memory block
+ * with base address _base and length _length */
+#define BELONGS(_addr, _base, _length) \
+ (_addr >= _base && _addr < _base + _length)
/*! \brief For short blocks numbers 1 to 36 represent lengths and offsets,
* such that:
@@ -157,15 +180,15 @@ static const uint64_t heap_init_mask = ~(ONE << HEAP_SEGMENT);
* For instance, mark first X bytes of a number N as initialised:
* N |= static_init_masks[X] */
static const uint64_t static_init_masks [] = {
- 0UL, /* 0 bytes */
- 1UL, /* 1 byte */
- 257UL, /* 2 bytes */
- 65793UL, /* 3 bytes */
- 16843009UL, /* 4 bytes */
- 4311810305UL, /* 5 bytes */
- 1103823438081UL, /* 6 bytes */
- 282578800148737UL, /* 7 bytes */
- 72340172838076673UL /* 8 bytes */
+ 0, /* 0 bytes */
+ 1, /* 1 byte */
+ 257, /* 2 bytes */
+ 65793, /* 3 bytes */
+ 16843009, /* 4 bytes */
+ 4311810305, /* 5 bytes */
+ 1103823438081, /* 6 bytes */
+ 282578800148737, /* 7 bytes */
+ 72340172838076673 /* 8 bytes */
};
/*! \brief Bit masks for setting read-only (second least significant) bits.
@@ -182,15 +205,15 @@ static const uint64_t static_init_masks [] = {
* For instance, mark first X bytes of a number N as read-only:
* N |= static_readonly_masks[X] */
static const uint64_t static_readonly_masks [] = {
- 0UL, /* 0 bytes */
- 2UL, /* 1 byte */
- 514UL, /* 2 bytes */
- 131586UL, /* 3 bytes */
- 33686018UL, /* 4 bytes */
- 8623620610UL, /* 5 bytes */
- 2207646876162UL, /* 6 bytes */
- 565157600297474UL, /* 7 bytes */
- 144680345676153346UL /* 8 bytes */
+ 0, /* 0 bytes */
+ 2, /* 1 byte */
+ 514, /* 2 bytes */
+ 131586, /* 3 bytes */
+ 33686018, /* 4 bytes */
+ 8623620610, /* 5 bytes */
+ 2207646876162, /* 6 bytes */
+ 565157600297474, /* 7 bytes */
+ 144680345676153346 /* 8 bytes */
};
/* }}} */
@@ -206,7 +229,7 @@ static void validate_memory_layout() {
/* Check that the struct holding memory layout is marked as initialized. */
DVASSERT(mem_layout.initialized != 0, "Un-initialized shadow layout", NULL);
/* Make sure the order of program segments is as expected, i.e.,
- * top to bittom: stack -> tls -> heap -> global*/
+ * top to bottom: stack -> tls -> heap -> global */
#define NO_MEM_SEGMENTS 11
uintptr_t segments[NO_MEM_SEGMENTS][2] = {
@@ -273,31 +296,83 @@ static void validate_memory_layout() {
#define DVALIDATE_IS_ON_STATIC(_addr, _size) \
DVALIDATE_IS_ON(_addr, _size, STATIC)
+/* Assert that `_addr` is on heap and it is the base address of an allocated
+ * heap memory block */
+#define DVALIDATE_FREEABLE(_addr) \
+ DVASSERT(IS_ON_HEAP(_addr), "Expected heap location: %a\n", _addr); \
+ DVASSERT(_addr == base_addr(_addr), \
+ "Expected base address, i.e., %a, not %a\n", base_addr(_addr), _addr);
+
/* Assert that a memory block [_addr, _addr + _size] is allocated on a
* program's heap */
# define DVALIDATE_HEAP_ACCESS(_addr, _size) \
- DVASSERT(IS_ON_HEAP(_addr), "Expected heap location: %a\n ", _addr); \
- DVASSERT(heap_allocated((uintptr_t)_addr, _size), \
- "Operation on unallocated heap block [%a + %lu]\n ", _addr, _size)
+ DVASSERT(IS_ON_HEAP(_addr), "Expected heap location: %a\n", _addr); \
+ DVASSERT(heap_allocated((uintptr_t)_addr, _size, (uintptr_t)_addr), \
+ "Operation on unallocated heap block [%a + %lu]\n", _addr, _size)
+
+/* Assert that every location belonging to the range [_addr, _addr + _size] is
+ * - belongs to a tracked static region (i.e., stack, TLS or global)
+ * - not allocated */
+# define DVALIDATE_HEAP_FREE(_addr, _size) { \
+ uintptr_t i, a = (uintptr_t)_addr; \
+ for (i = 0; i < _size; i++) { \
+ DVASSERT(IS_ON_HEAP(a + i), "Expected heap location: %a\n", a + i); \
+ DVASSERT(!heap_allocated(a + i, 1, a + i), \
+ "Expected heap unallocated location: [%a + %lu]\n", a, i); \
+ } \
+}
/* Assert that memory block [_addr, _addr + _size] is allocated on stack, TLS
* or globally */
# define DVALIDATE_STATIC_ACCESS(_addr, _size) \
- DVASSERT(IS_ON_STATIC(_addr), "Expected location: %a\n ", _addr); \
- DVASSERT(static_allocated((uintptr_t)_addr, _size), \
- "Operation on unallocated block [%a + %lu]\n ", _addr, _size)
+ DVASSERT(IS_ON_STATIC(_addr), \
+ "Expected static location: [%a + %lu], \n", _addr, _size); \
+ DVASSERT(static_allocated((uintptr_t)_addr, _size,(uintptr_t)_addr), \
+ "Operation on unallocated static block [%a + %lu]\n", _addr, _size)
/* Same as ::DVALIDATE_STATIC_LOCATION but for a single memory location */
# define DVALIDATE_STATIC_LOCATION(_addr) \
- DVASSERT(IS_ON_STATIC(_addr), "Expected location: %a\n ", _addr); \
+ DVASSERT(IS_ON_STATIC(_addr), \
+ "Expected static location: %a\n", _addr); \
DVASSERT(static_allocated_one((uintptr_t)_addr), \
- "Operation on unallocated block [%a]\n ", _addr)
+ "Operation on unallocated static block [%a]\n", _addr)
+
+/* Assert that every location belonging to the range [_addr, _addr + _size] is
+ * - belongs to a tracked static region (i.e., stack, TLS or global)
+ * - not allocated */
+# define DVALIDATE_STATIC_FREE(_addr, _size) { \
+ uintptr_t i, a = (uintptr_t)_addr; \
+ for (i = 0; i < _size; i++) { \
+ DVASSERT(IS_ON_STATIC(a + i), \
+ "Expected static location in freea: %a\n", a + i); \
+ DVASSERT(!static_allocated_one(a + i), \
+ "Expected static unallocated location in freea: [%a + %lu]\n", a, i); \
+ } \
+}
-/* Assert that a memory block [_addr, _adddr + _size] is nullified */
+/* Assert that a memory block [_addr, _addr + _size] is nullified */
# define DVALIDATE_NULLIFIED(_addr, _size) \
DVASSERT(zeroed_out((void *)_addr, _size), \
"Block [%a, %a+%lu] not nullified", _addr, _addr, _size)
+/* Assert that memory block [_addr, _addr + _size] is allocated */
+# define DVALIDATE_ALLOCATED(_addr, _size, _base) \
+ DVASSERT(allocated((uintptr_t)_addr, _size, (uintptr_t)_base), \
+ "Operation on unallocated block [%a + %lu] with base %a\n", \
+ _addr, _size, _base)
+
+/* Assert that memory block [_addr, _addr + _size] is allocated
+ * and can be written to */
+# define DVALIDATE_RW_ACCESS(_addr, _size) { \
+ DVALIDATE_ALLOCATED((uintptr_t)_addr, _size, (uintptr_t)_addr); \
+ DVASSERT(!readonly((void*)_addr), \
+ "Unexpected readonly address: %lu\n", _addr) \
+}
+
+/* Assert that memory block [_addr, _addr + _size] is allocated */
+# define DVALIDATE_RO_ACCESS(_addr, _size) \
+ DVALIDATE_ALLOCATED((uintptr_t)_addr, _size, (uintptr_t)_addr)
+
#else
/*! \cond exclude from doxygen */
# define DVALIDATE_SHADOW_LAYOUT
@@ -312,6 +387,12 @@ static void validate_memory_layout() {
# define DVALIDATE_IS_ON_GLOBAL
# define DVALIDATE_IS_ON_TLS
# define DVALIDATE_IS_ON_STATIC
+# define DVALIDATE_FREEABLE
+# define DVALIDATE_STATIC_FREE
+# define DVALIDATE_HEAP_FREE
+# define DVALIDATE_RO_ACCESS
+# define DVALIDATE_RW_ACCESS
+# define DVALIDATE_ALLOCATED
/*! \endcond */
#endif
/* }}} */
@@ -320,27 +401,16 @@ static void validate_memory_layout() {
/* See definitions for documentation */
static uintptr_t heap_info(uintptr_t addr, char type);
static uintptr_t static_info(uintptr_t addr, char type);
-static int heap_allocated(uintptr_t addr, size_t size);
-static int static_allocated(uintptr_t addr, long size);
+static int heap_allocated(uintptr_t addr, size_t size, uintptr_t base_ptr);
+static int static_allocated(uintptr_t addr, long size, uintptr_t base_ptr);
+static int allocated(uintptr_t addr, long size, uintptr_t base_ptr);
static int freeable(void *ptr);
/*! \brief Quick test to check if a static location belongs to allocation.
* This macro really belongs where static_allocated is defined, but
* since it is used across this whole file it needs to be defined here. */
-#define static_allocated_one(addr) \
- ((int)PRIMARY_SHADOW(addr))
-
-/*! \brief Shortcut for executing statements based on the segment a given
- * address belongs to.
- * \param intptr_t _addr - a memory address
- * \param code_block _heap_stmt - code executed if `_addr` is a heap address
- * \param code_block _static_stmt - code executed if `_addr` is a static address */
-#define TRY_SEGMENT_WEAK(_addr, _heap_stmt, _static_stmt) \
- if (IS_ON_HEAP(_addr)) { \
- _heap_stmt; \
- } else if (IS_ON_STATIC(_addr)) { \
- _static_stmt; \
- } \
+#define static_allocated_one(_addr) \
+ (*((unsigned char*)PRIMARY_SHADOW(_addr)))
/*! \brief Shortcut for executing statements based on the segment a given
* address belongs to.
@@ -352,7 +422,7 @@ static int freeable(void *ptr);
_heap_stmt; \
} else if (IS_ON_STATIC(_addr)) { \
_static_stmt; \
- } \
+ }
/*! \brief Same as TRY_SEGMENT but performs additional checks aborting the
* execution if the given address is `NULL` or does not belong to known
@@ -363,10 +433,8 @@ static int freeable(void *ptr);
* the given address does not belong to any of the known segments. */
#define TRY_SEGMENT(_addr, _heap_stmt, _static_stmt) { \
TRY_SEGMENT_WEAK(_addr, _heap_stmt, _static_stmt) \
- else if (_addr == 0) { \
- vassert(0, "Unexpected null pointer\n", NULL); \
- } else { \
- vassert(0, "Address %a not found in known segments\n", _addr); \
+ else { \
+ vassert(0, "Use of invalid address %a in %s\n", _addr, __func__); \
} \
}
@@ -385,15 +453,11 @@ static uintptr_t predicate(uintptr_t addr, char p) {
return 0;
}
-/*! \brief Return a byte length of a memory block address `_addr` belongs to
- * \param uintptr_t _addr - a memory address */
+/*! \brief Return the byte length of the memory block containing `_addr` */
#define block_length(_addr) predicate((uintptr_t)_addr, 'L')
-/*! \brief Return a base address of a memory block address `_addr` belongs to
- * \param uintptr_t _addr - a memory address */
+/*! \brief Return the base address of the memory block containing `_addr` */
#define base_addr(_addr) predicate((uintptr_t)_addr, 'B')
-/*! \brief Return a byte offset of a memory address given by `_addr` within
- * its block
- * \param uintptr_t _addr - a memory address */
+/*! \brief Return the byte offset of `_addr` within its block */
#define offset(_addr) predicate((uintptr_t)_addr, 'O')
/* }}} */
@@ -434,7 +498,7 @@ static void shadow_alloca(void *ptr, size_t size) {
uint64_t *prim_shadow_alt = (uint64_t *)PRIMARY_SHADOW(ptr);
unsigned int *sec_shadow = (unsigned int*)SECONDARY_SHADOW(ptr);
- /* Make sure static region is nullified */
+ /* Make sure shadows are nullified */
DVALIDATE_NULLIFIED(prim_shadow, size);
DVALIDATE_NULLIFIED(sec_shadow, size);
@@ -488,8 +552,10 @@ static void shadow_freea(void *ptr) {
/*! \brief Return a non-zero value if a memory region of length `size`
* starting at address `addr` belongs to a tracked stack, tls or
* global memory block and 0 otherwise.
- * This function is only safe if applied to a tls, stack or global address. */
-static int static_allocated(uintptr_t addr, long size) {
+ * This function is only safe if applied to a tls, stack or global address.
+ * Explanations regarding the third argument - `base_ptr` - are given
+ * via inline documentation of function ::heap_allocated */
+static int static_allocated(uintptr_t addr, long size, uintptr_t base_ptr) {
unsigned char *prim_shadow = (unsigned char*)PRIMARY_SHADOW(addr);
/* Unless the address belongs to tracked allocation 0 is returned */
if (prim_shadow[0]) {
@@ -506,7 +572,14 @@ static int static_allocated(uintptr_t addr, long size) {
offset = short_offsets[code];
length = short_lengths[code];
}
- return offset + size <= length;
+
+ if (addr != base_ptr) {
+ uintptr_t base_addr = addr - offset;
+ return BELONGS(base_ptr, base_addr, length)
+ && offset + size <= length;
+ } else {
+ return offset + size <= length;
+ }
}
return 0;
}
@@ -517,7 +590,7 @@ static int static_allocated(uintptr_t addr, long size) {
static int static_initialized(uintptr_t addr, long size) {
/* Return 0 right away if the address does not belong to
* static allocation */
- if (!static_allocated(addr, size))
+ if (!static_allocated(addr, size, addr))
return 0;
DVALIDATE_STATIC_ACCESS(addr, size);
@@ -555,9 +628,9 @@ static int static_initialized(uintptr_t addr, long size) {
* - 'L' - return the size in bytes of the memory block `addr` belongs to or `0`
* if `addr` lies outside of tracked allocation.
*
- * NB: One should make sure that a given address if valid before querying.
- * That is, for the cases when addr does not refer to a valid memory address
- * belonging to static allocation the return value for this function is
+ * NB: One should make sure that a given address is allocated before querying.
+ * That is, for the cases when addr does not refer to an allocated memory
+ * address belonging to static allocation the return value for this function is
* unspecified. */
static uintptr_t static_info(uintptr_t addr, char type) {
DVALIDATE_STATIC_LOCATION(addr);
@@ -646,11 +719,11 @@ static void initialize_static_region(uintptr_t addr, long size) {
* NOTE: This function has many similarities with ::initialize_static_region
* The functionality, however is preferred to be kept separate
* because the ::mark_readonly should operate only on the global shadow. */
-static void mark_readonly (uintptr_t addr, long size) {
+static void mark_readonly_region (uintptr_t addr, long size) {
/* Since read-only blocks can only be stored in the globals segments (e.g.,
* TEXT), this function required ptr carry a global address. */
DASSERT(IS_ON_GLOBAL(addr));
- DASSERT(static_allocated(addr, 1));
+ DASSERT(static_allocated_one(addr));
DVASSERT(!(addr - base_addr(addr) + size > block_length(addr)),
"Attempt to mark read-only %lu bytes past block boundaries\n"
"starting at %a with block length %lu at base address %a\n",
@@ -691,56 +764,39 @@ static size_t heap_allocation_size = 0;
/*! \brief Create a heap shadow for an allocated memory block starting at `ptr`
* and of length `size`. Optionally mark it as initialized if `init`
* evaluates to a non-zero value.
- * \b NOTE: This function assumes that `ptr` is a valid base address of a
+ * \b NOTE: This function assumes that `ptr` is a base address of a
* heap-allocated memory block, such that HEAP_SEGMENT bytes preceding `ptr`
* correspond to `unusable space`.
* \b WARNING: Current implementation assumes that the size of a heap segment
* does not exceed 64 bytes. */
-static void set_heap_segment(void *ptr, size_t size, size_t init) {
+static void set_heap_segment(void *ptr, size_t size, size_t alloc_size, size_t init) {
/* Ensure the shadowed block in on the tracked heap portion */
DVALIDATE_IS_ON_HEAP(((uintptr_t)ptr) - HEAP_SEGMENT, size);
DVALIDATE_ALIGNMENT(ptr); /* Make sure alignment is right */
- heap_allocation_size += size; /* Adjuct tracked allocation size */
+ heap_allocation_size += size; /* Adjust tracked allocation size */
/* Get aligned size of the block, i.e., an actual size of the
* allocated block */
- size_t aligned_size = ALIGNED_SIZE(size);
- unsigned char *shadowed = (unsigned char*)HEAP_SHADOW(ptr);
- uintptr_t *shadow_meta = (uintptr_t*)(shadowed - HEAP_SEGMENT);
+ unsigned char *shadow = (unsigned char*)HEAP_SHADOW(ptr);
/* Make sure shadow is nullified before setting it */
- DVALIDATE_NULLIFIED(shadow_meta, aligned_size + HEAP_SEGMENT);
-
- /* Write the actual length to the meta-segment. First 8 (or 4 in a 32-bit
- * system) bytes of the segment are nullified to indicate that this segment
- * does not correspond to an allocated memory block. The following block (at
- * index 1) captures the size of the segment in bytes. */
- shadow_meta[1] = size;
+ DVALIDATE_NULLIFIED(shadow, alloc_size);
/* The overall number of block segments in a tracked memory block */
- size_t block_segments = aligned_size/HEAP_SEGMENT;
- uintptr_t *block_segment = NULL;
- int i;
+ size_t segments = alloc_size/HEAP_SEGMENT;
+ uintptr_t *segment = (uintptr_t*)(shadow);
+ segment[1] = size;
+ int i;
/* Write the offsets per segment */
- for (i = 0; i < block_segments; i++) {
- block_segment = (uintptr_t*)(shadowed + i*HEAP_SEGMENT);
- /* Write down the segment offset to the first 8 (or 4) bytes of the segment.
- * Here it is necessary to increment the offset by one. If there is no
- * increment, then the offset of the first segment is 0, which is the same
- * as for a segment that does not belong to a program's allocation. */
- *block_segment = i*HEAP_SEGMENT + 1;
+ for (i = 0; i < segments; i++) {
+ segment = (uintptr_t*)(shadow + i*HEAP_SEGMENT);
+ *segment = (uintptr_t)ptr;
}
/* If init is a non-zero value then mark all allocated bytes as initialized */
if (init) {
- for (i = 0; i < block_segments; i++) {
- block_segment = (uintptr_t*)(shadowed + i*HEAP_SEGMENT);
- block_segment[1] |= heap_init_mask;
- }
- /* If the last segment is partially allocated, nullify the unallocated
- * bits back. */
- block_segment[1] &= ~(ONE << size%HEAP_SEGMENT);
+ memset(HEAP_INIT_SHADOW(ptr), (unsigned int)ONE, alloc_size/8);
}
}
@@ -758,13 +814,13 @@ static void set_heap_segment(void *ptr, size_t size, size_t init) {
* returned pointer shall not be used to access an object." */
static void* shadow_malloc(size_t size) {
size_t alloc_size = ALLOC_SIZE(size);
+
/* Return NULL if the size is too large to be aligned */
- char* res = alloc_size ? (char*)native_malloc(alloc_size) : NULL;
+ char* res = alloc_size ?
+ (char*)native_aligned_alloc(HEAP_SEGMENT, alloc_size) : NULL;
- if (res) {
- res += HEAP_SEGMENT;
- set_heap_segment(res, size, 0);
- }
+ if (res)
+ set_heap_segment(res, size, alloc_size, 0);
return res;
}
@@ -774,17 +830,18 @@ static void* shadow_calloc(size_t nmemb, size_t size) {
/* Since both `nmemb` and `size` are both of size `size_t` the multiplication
* of the arguments (which gives the actual allocation size) might lead to an
* integer overflow. The below code checks for an overflow and sets the
- * `alloc_size` (agrument a memory allocation function) to zero. */
+ * `alloc_size` (argument a memory allocation function) to zero. */
size = (size && nmemb > SIZE_MAX/size) ? 0 : nmemb*size;
+ size_t alloc_size = ALLOC_SIZE(size);
+
/* Since aligned size is required by the model do the allocation through
* `malloc` and nullify the memory space by hand */
- char* res = size ? (char*)native_malloc(ALLOC_SIZE(size)) : NULL;
+ char* res = size ? (char*)native_malloc(alloc_size) : NULL;
if (res) {
- res += HEAP_SEGMENT;
memset(res, 0, size);
- set_heap_segment(res, size, 1);
+ set_heap_segment(res, size, alloc_size, 1);
}
return res;
@@ -792,16 +849,37 @@ static void* shadow_calloc(size_t nmemb, size_t size) {
/* }}} */
/* Heap deallocation (free) {{{ */
-static void shadow_free(void *res) {
- char *ptr = (char *)res;
+
+/*! \brief Remove a memory block with base address given by `ptr` from tracking.
+ * This function effectively nullifies block shadow tracking an application
+ * block and optionally nullifies an init shadow associated with the block.
+ *
+ * NOTE: ::unset_heap_segment assumes that `ptr` is a base address of an
+ * allocated heap memory block, i.e., `freeable(ptr)` evaluates to true. */
+static void unset_heap_segment(void *ptr, int init) {
+ DVALIDATE_FREEABLE(((uintptr_t)ptr));
+ /* Base address of shadow block */
+ uintptr_t *base_shadow = (uintptr_t*)HEAP_SHADOW(ptr);
+ /* Physical allocation size */
+ size_t alloc_size = ALLOC_SIZE(base_shadow[1]);
+ /* Actual block length */
+ size_t length = base_shadow[1];
+ /* Nullify shadow block */
+ memset(base_shadow, ZERO, alloc_size);
+ /* Adjust tracked allocation size */
+ heap_allocation_size -= length;
+ /* Nullify init shadow */
+ if (init) {
+ memset(HEAP_INIT_SHADOW(ptr), 0, alloc_size/8);
+ }
+}
+
+/*! \brief Replacement for `free` with memory tracking */
+static void shadow_free(void *ptr) {
if (ptr != NULL) { /* NULL is a valid behaviour */
if (freeable(ptr)) {
- size_t size = block_length(ptr);
- void *meta_shadow = (void*)(HEAP_SHADOW(ptr) - HEAP_SEGMENT);
- memset(meta_shadow, 0, HEAP_SHADOW_BLOCK_SIZE(size));
- native_free(ptr - HEAP_SEGMENT);
- /* Adjuct tracked allocation size carried via `__e_acsl_heap_allocation_size` */
- heap_allocation_size -= size;
+ unset_heap_segment(ptr, 1);
+ native_free(ptr);
} else {
vabort("Not a start of block (%a) in free\n", ptr);
}
@@ -810,8 +888,7 @@ static void shadow_free(void *res) {
/* }}} */
/* Heap reallocation (realloc) {{{ */
-static void* shadow_realloc(void *p, size_t size) {
- char *ptr = (char*)p;
+static void* shadow_realloc(void *ptr, size_t size) {
char *res = NULL; /* Resulting pointer */
/* If the pointer is NULL then realloc is equivalent to malloc(size) */
if (ptr == NULL)
@@ -821,76 +898,45 @@ static void* shadow_realloc(void *p, size_t size) {
else if (ptr != NULL && size == 0) {
shadow_free(ptr);
} else {
- if (freeable(ptr)) { /* ... and valid for free */
+ if (freeable(ptr)) { /* ... and can be used as an input to `free` */
size_t alloc_size = ALLOC_SIZE(size);
- res = native_realloc(ptr - HEAP_SEGMENT, alloc_size);
+ res = native_realloc(ptr, alloc_size);
DVALIDATE_ALIGNMENT(res);
/* realloc succeeds, otherwise nothing needs to be done */
if (res != NULL) {
- res += HEAP_SEGMENT;
- /* Tracked size of the old allocation */
- size_t old_size = block_length((uintptr_t)ptr);
- /* Number of block segments in the old allocation */
- size_t old_segments = BLOCK_SEGMENTS(old_size);
- /* Number of block segments in the new allocation */
- size_t new_segments = BLOCK_SEGMENTS(size);
- /* Adjuct tracked allocation size */
- heap_allocation_size += -old_size + size;
-
- /* Address of the meta-block in old allocation */
- uintptr_t *meta_shadow = (uintptr_t*)(HEAP_SHADOW(ptr) - HEAP_SEGMENT);
-
- /* The case when realloc displaces the base address of a pointer */
- if (ptr != res) {
- /* Address of the new shadow meta-block */
- uintptr_t *new_meta_shadow =
- (uintptr_t*)(HEAP_SHADOW(res) - HEAP_SEGMENT);
- size_t inflen = HEAP_SEGMENT*(old_segments + 1);
- /* Copy information over to the new shadow ... */
- memcpy(new_meta_shadow, meta_shadow, inflen);
- /* ... and nuke the old shadow */
- memset(meta_shadow, 0, inflen);
- meta_shadow = new_meta_shadow;
+ size_t alloc_size = ALLOC_SIZE(size);
+ size_t old_size = block_length(ptr);
+ size_t old_alloc_size = ALLOC_SIZE(old_size);
+
+ /* Nullify old representation */
+ unset_heap_segment(ptr, 0);
+
+ /* Set up new block shadow */
+ set_heap_segment(res, size, alloc_size, 0);
+
+ /* Move init shadow */
+ unsigned char* old_init_shadow = (unsigned char*)HEAP_INIT_SHADOW(ptr);
+ unsigned char* new_init_shadow = (unsigned char*)HEAP_INIT_SHADOW(res);
+
+ /* If realloc truncates allocation in the old init shadow it is first
+ * needed to clear the old init shadow from the boundary of the old
+ * shadow block to the size of the new allocation */
+ if (old_size > size) {
+ clearbits_right(
+ old_alloc_size - size,
+ old_init_shadow + old_alloc_size/8);
}
- /* Set new size */
- meta_shadow[1] = size;
-
- /* Realloc truncates allocation, need to truncate the shadow as well:
- * 1. Get the last segment in the new allocation and clear all init
- * bits from the old allocation that do not belong in the new.
- * 2. Nullify segments tracking old allocation but which do not
- * belong to the new one. These will be past the last segment
- * (as above). */
- if (old_segments > new_segments) {
- /* Last segment in the new allocation and the number of bits to
- * clear out */
- size_t last_index = new_segments - 1;
- size_t clear_bits = HEAP_SEGMENT - (size - last_index*HEAP_SEGMENT);
-
- /* Reset initialization in shadow past the new allocation (1). */
- void *seg_last = (void*)
- (HEAP_SHADOW(res) +
- last_index*HEAP_SEGMENT + INIT_BYTES + PTR_SZ);
- clearbits_right(seg_last, clear_bits);
-
- /* Clear out remaining shadow data from old allocation that is
- * not used in the new allocation (2) */
- int diff = old_segments - new_segments;
- char *seg_next = (char*)(HEAP_SHADOW(res)
- + (last_index+1)*HEAP_SEGMENT);
- memset(seg_next, 0, diff*HEAP_SEGMENT);
- /* Realloc increases allocation, only segment indices need to be added */
- } else if (old_segments < new_segments) {
- /* Just add indices to shadow. Realloc does not initialize
- * allocated data past the old allocation. */
- int i;
- for (i = old_segments; i < new_segments; i++) {
- uintptr_t *seg_next = (uintptr_t*)(HEAP_SHADOW(res)
- + i*HEAP_SEGMENT);
- seg_next[0] = HEAP_SEGMENT*i + 1;
- }
+ /* Now init shadow can be moved (if needed), keep in mind that
+ * segment base addresses are aligned at a boundary of something
+ * divisible by 8, so instead of moving actual bits here the
+ * segments are moved to avoid dealing with bit-level operations
+ * on incomplete bytes. */
+ if (res != ptr) {
+ size_t copy_size = (old_size > size) ? alloc_size : old_alloc_size;
+ memcpy(new_init_shadow, old_init_shadow, copy_size);
+ memset(old_init_shadow, 0, copy_size);
}
}
} else {
@@ -912,10 +958,9 @@ static void *shadow_aligned_alloc(size_t alignment, size_t size) {
return NULL;
char *res = native_aligned_alloc(alignment, size);
- if (res) {
- res += HEAP_SEGMENT;
- set_heap_segment(res, size, 0);
- }
+ if (res)
+ set_heap_segment(res, size, ALLOC_SIZE(size), 0);
+
return (void*)res;
}
/* }}} */
@@ -930,13 +975,12 @@ static int shadow_posix_memalign(void **memptr, size_t alignment, size_t size) {
return -1;
/* Make sure that the first argument to posix memalign is indeed allocated */
- vassert(valid(memptr, sizeof(void*)),
+ vassert(allocated((uintptr_t)memptr, sizeof(void*), (uintptr_t)memptr),
"\\invalid memptr in posix_memalign", NULL);
int res = native_posix_memalign(memptr, alignment, size);
if (!res) {
- *memptr += HEAP_SEGMENT;
- set_heap_segment(*memptr, size, 0);
+ set_heap_segment(*memptr, size, ALLOC_SIZE(size), 0);
}
return res;
}
@@ -946,28 +990,36 @@ static int shadow_posix_memalign(void **memptr, size_t alignment, size_t size) {
/*! \brief Return a non-zero value if a memory region of length `size`
* starting at address `addr` belongs to an allocated (tracked) heap memory
* block and a 0 otherwise. Note, this function is only safe if applied to a
- * heap address. */
-static int heap_allocated(uintptr_t addr, size_t size) {
- /* Offset within the segment */
- size_t block_offset = addr%HEAP_SEGMENT;
- /* Address of the shadow segment the address belongs to */
- uintptr_t *aligned_shadow =
- (uintptr_t*)HEAP_SHADOW(addr - block_offset);
+ * heap address.
+ *
+ * Note the third argument `base_ptr` that represents the base of a pointer, i.e.,
+ * `addr` of the form `base_ptr + i`, where `i` is some integer index.
+ * ::heap_allocated also returns zero if `base_ptr` and `addr` belong to different
+ * memory blocks, or if `base_ptr` lies within unallocated region. The intention
+ * here is to be able to detect dereferencing of an allocated memory block through
+ * a pointer to a different block. Consider, for instance, some pointer `p` that
+ * points to a memory block `B`, and an index `i`, such that `p+i` references a
+ * memory location belonging to a different memory block (say `C`). From a
+ * low-level viewpoint, dereferencing `p+i` is safe (since it belongs to a properly
+ * allocated block). From our perspective, however, dereference of `p+i` is
+ * only legal if both `p` and `p+i` point to the same block. */
+static int heap_allocated(uintptr_t addr, size_t size, uintptr_t base_ptr) {
+ /* Base address of the shadow segment the address belongs to */
+ uintptr_t *shadow = (uintptr_t*)HEAP_SHADOW(addr - addr%HEAP_SEGMENT);
/* Non-zero if the segment belongs to heap allocation */
- if (aligned_shadow[0]) {
- /* Offset stored by the segment (real offset from base incremented by 1) */
- size_t segment_offset = aligned_shadow[0];
- /* Base address */
- uintptr_t base_addr = addr - block_offset - segment_offset + 1;
- /* Pointer to the meta-segment */
- uintptr_t *meta_segment =
- (uintptr_t*)HEAP_SHADOW(base_addr - HEAP_SEGMENT);
- /* Size of the block stored by meta-segment */
- size_t length = meta_segment[1];
- /* Offset of a given address within its block */
- size_t offset = segment_offset - 1 + block_offset;
- return offset + size <= length;
+ if (shadow[0]) {
+ uintptr_t *base_shadow =
+ (uintptr_t*)HEAP_SHADOW(base_ptr - base_ptr%HEAP_SEGMENT);
+ uintptr_t *first_segment = (uintptr_t*)HEAP_SHADOW(shadow[0]);
+ /* shadow[0] - base address of the tracked block
+ * fist_segment[1] - length (i.e., location in the first segment
+ * after base address)
+ * offset is the difference between the address and base address (shadow[0])
+ * Then an address belongs to heap allocation if
+ * offset + size <= length */
+ return base_shadow[0] == shadow[0] &&
+ (addr - shadow[0]) + size <= first_segment[1];
}
return 0;
}
@@ -978,102 +1030,80 @@ static int heap_allocated(uintptr_t addr, size_t size) {
* As some of the other functions, \b \\freeable can be expressed using
* ::IS_ON_HEAP, ::heap_allocated and ::base_addr. Here direct
* implementation is preferred for performance reasons. */
-static int freeable(void *ptr) {
+static int freeable(void *ptr) { /* + */
uintptr_t addr = (uintptr_t)ptr;
+ /* Address is not on the program's heap, so cannot be freed */
if (!IS_ON_HEAP(addr))
return 0;
- /* Offset within the segment */
- size_t block_offset = addr%HEAP_SEGMENT;
- /* Address of the shadow segment the address belongs to */
- uintptr_t *aligned_shadow = (uintptr_t*)HEAP_SHADOW(addr - block_offset);
- /* Non-zero if the segment belongs to heap allocation */
- if (aligned_shadow[0])
- return addr == addr - block_offset - aligned_shadow[0] + 1;
- return 0;
-}
-
-/*! \brief Implementation of the \b \\initialized predicate for heap-allocated
- * memory. NB: If `addr` does not belong to a valid heap region this function
- * returns 0. */
-static int heap_initialized(uintptr_t addr, long len) {
- /* Unallocated heap address */
- if (!heap_allocated(addr, len))
- return 0;
-
- /* Do validate a block in debug mode otherwise */
- DVALIDATE_HEAP_ACCESS(addr, len);
- int result = 1;
- /* Offset within the segment. Also the number of bits
- * that needs to be skipped when evaluating init */
- int skipbits = addr%HEAP_SEGMENT;
-
- /* Base address of a shadow segment ptr belongs to */
- uintptr_t shadow_init = (uintptr_t)(HEAP_SHADOW(addr) + PTR_SZ - skipbits);
-
- int rem = HEAP_SEGMENT - skipbits;
- /* The number of bits that need to be checked in the `first' segment */
- int setbits = (len >= rem) ? rem : len;
-
- len -= setbits;
-
- /* Bit-mask for setting values. Tested bits are set to ones, the rest
- * are zeroes. */
- uint64_t mask = (ONE >> (ULONG_BITS - setbits)) << skipbits;
-
- uint64_t *init = (uint64_t*)shadow_init;
- result = result && ((mask & *init) == mask);
- shadow_init += HEAP_SEGMENT;
-
- while (len > 0) {
- /* Recompute the number of bits to be set */
- setbits = (len > HEAP_SEGMENT) ? HEAP_SEGMENT : len;
- /* Reset the mask */
- mask = ONE >> (ULONG_BITS - setbits);
- /* Current position of shadow initialization */
- init = (uint64_t*)shadow_init;
-
- result = result && ((mask & *init) == mask);
- len -= setbits;
- shadow_init += HEAP_SEGMENT;
+ /* Address of the shadow segment the address belongs to */
+ uintptr_t *shadow = (uintptr_t*)ALIGNED_HEAP_SHADOW(addr);
+ /* Non-zero if the segment belongs to heap allocation with *shadow
+ * capturing the base address of the tracked block */
+ if (*shadow) {
+ /* Block is freeable if `addr` is the base address of its block */
+ return (uintptr_t)*shadow == addr;
}
- return result;
+ return 0;
}
/*! \brief Querying information about a specific heap memory address.
* This function is similar to ::static_info except it returns data
- * associated with heap-allocated memory.
+ * associated with dynamically allocated memory.
* See in-line documentation for ::static_info for further details. */
static uintptr_t heap_info(uintptr_t addr, char type) {
+ /* Ensure that `addr` is an allocated location on a program's heap */
DVALIDATE_HEAP_ACCESS(addr, 1);
- /* Offset within the segment */
- size_t block_offset = addr%HEAP_SEGMENT;
- /* Address of the shadow segment the address belongs to */
- uintptr_t *aligned_shadow =
- (uintptr_t*)HEAP_SHADOW(addr - block_offset);
- /* Offset stored by the segment (real offset from base incremented by 1) */
- size_t segment_offset = aligned_shadow[0];
- /* Base address */
- uintptr_t base_addr = addr - block_offset - segment_offset + 1;
+ /* Base address of the shadow segment the address belongs to.
+ * First `sizeof(uintptr_t)` bytes of each segment store application-level
+ * base address of the tracked block */
+ uintptr_t *aligned_shadow = (uintptr_t*)ALIGNED_HEAP_SHADOW(addr);
switch(type) {
case 'B': /* Base address */
- return base_addr;
+ return *aligned_shadow;
case 'L': { /* Block length */
- /* Pointer to meta-segment */
- uintptr_t *meta_segment =
- (uintptr_t*)HEAP_SHADOW(base_addr - HEAP_SEGMENT);
- /* Size of the block stored by meta-segment */
- return meta_segment[1];
+ /* Pointer to the first-segment in the shadow block */
+ uintptr_t *base_segment = (uintptr_t*)HEAP_SHADOW(*aligned_shadow);
+ /* Length of the stored block is captured in `sizeof(uintptr_t)` bytes
+ * past `sizeof(uintptr_t)` tracking the base address */
+ return base_segment[1];
}
case 'O':
- /* Offset of a given address within its block */
- return segment_offset - 1 + block_offset;
+ /* Offset of a given address within its block. This is the difference
+ * between the input address and the base address of the block. */
+ return addr - *aligned_shadow;
default:
DASSERT(0 && "Unknown heap query type");
}
return 0;
}
+
+/*! \brief Implementation of the \b \\initialized predicate for heap-allocated
+ * memory. NB: If `addr` does not belong to an allocated heap block this
+ * function returns 0. */
+static int heap_initialized(uintptr_t addr, long len) {
+ /* Base address of a shadow segment addr belongs to */
+ unsigned char *shadow = (unsigned char*)(HEAP_INIT_SHADOW(addr));
+
+ /* See comments in the `initialize_heap_region` function for more details */
+ unsigned skip = (addr - HEAP_START)%8;
+ unsigned set;
+ if (skip) {
+ set = 8 - skip;
+ set = (len > set) ? set : len;
+ len -= set;
+ unsigned char mask = 0;
+ setbits64_skip(set,mask,skip);
+
+ if (*shadow != mask)
+ return 0;
+ }
+ if (len > 0)
+ return checkbits(len,shadow);
+ return 1;
+}
+
/* }}} */
/* Heap initialization {{{ */
@@ -1085,38 +1115,47 @@ static void initialize_heap_region(uintptr_t addr, long len) {
"starting at %a with block length %lu at base address %a\n",
len, addr, block_length(addr), base_addr(addr));
- /* Offset within the segment. Also the number of bits
- * that needs to be skipped when evaluating init */
- int skipbits = (addr)%HEAP_SEGMENT;
-
- /* Base address of a shadow segment addr belongs to */
- uintptr_t shadow_init = (uintptr_t)(HEAP_SHADOW(addr) + PTR_SZ - skipbits);
-
- int rem = HEAP_SEGMENT - skipbits;
- /* The number of bits that need to be checked in the `first' segment */
- int setbits = (len >= rem) ? rem : len;
-
- len -= setbits;
-
- /* Bit-mask for setting values. Bits that are tested are set to ones, the
- * rest are zeroes */
- uint64_t mask = (ONE >> (ULONG_BITS - setbits)) << skipbits;
-
- *(uint64_t*)shadow_init = *(uint64_t*)shadow_init | mask;
- shadow_init += HEAP_SEGMENT;
+ /* Address within init shadow tracking initialization */
+ unsigned char *shadow = (unsigned char*)(HEAP_INIT_SHADOW(addr));
+
+ /* First check whether the address in the init shadow is divisible by 8
+ * (i.e., located on a byte boundary) */
+ /* Leading bits in `*shadow` byte which do not need to be set
+ * (i.e., skipped) */
+ short skip = (addr - HEAP_START)%8;
+ if (skip) {
+ /* The remaining bits in the shadow byte */
+ short set = 8 - skip;
+ /* The length of initialized region can be short (shorter then the
+ * above remainder). Adjust the number of bits to set accordingly. */
+ set = (len > set) ? set : len;
+ len -= set;
+ setbits64_skip(set, *shadow, skip);
+ /* Move to the next location if there are more bits to set */
+ shadow++;
+ }
- while (len > 0) {
- /* Recompute the number of bits to be set */
- setbits = (len > HEAP_SEGMENT) ? HEAP_SEGMENT : len;
- /* Reset the mask */
- mask = ONE >> (ULONG_BITS - setbits);
- *(uint64_t*)shadow_init = *(uint64_t*)shadow_init | mask;
- len -= setbits;
- shadow_init += HEAP_SEGMENT;
+ if (len > 0) {
+ /* Set the remaining bits. Note `shadow` is now aligned at a byte
+ * boundary, thus one can set `len` bits starting with address given by
+ * `shadow` */
+ setbits(len, shadow);
}
}
/* }}} */
+/* Any allocation {{{ */
+/*! \brief Amalgamation of ::heap_allocated and ::static_allocated */
+static int allocated(uintptr_t addr, long size, uintptr_t base) {
+ TRY_SEGMENT_WEAK(addr,
+ return heap_allocated(addr, size, base),
+ return static_allocated(addr, size, base));
+ if (!IS_ON_VALID(addr))
+ return 0;
+ return 0;
+}
+/* }}} */
+
/* Any initialization {{{ */
/*! \brief Initialize a chunk of memory given by its start address (`addr`)
* and byte length (`n`). */
@@ -1173,20 +1212,39 @@ static void print_static_shadows(uintptr_t addr, size_t size) {
}
/*! \brief Print human-readable representation of a heap shadow region for a
- * memory block of length `size` starting at address `addr`. */
-static void print_heap_shadows(uintptr_t addr, size_t size) {
- unsigned char *shadowed = (unsigned char*)HEAP_SHADOW(addr);
- uintptr_t *shadow_meta = (uintptr_t*)(shadowed - HEAP_SEGMENT);
-
- size_t block_segments = (ALIGNED_SIZE(size))/HEAP_SEGMENT;
- DLOG("Meta: %3lu", shadow_meta[1]);
+ * memory block of length `size` starting at address `addr`. This function
+ * assumes that `addr` is the base address of the memory block. */
+static void print_heap_shadows(uintptr_t addr) {
+ unsigned char *block_shadow = (unsigned char*)HEAP_SHADOW(addr);
+ unsigned char *init_shadow = (unsigned char*)HEAP_INIT_SHADOW(addr);
+
+ size_t length = (size_t)((uintptr_t*)(block_shadow))[1];
+ size_t alloc_size = ALLOC_SIZE(length);
+ size_t segments = alloc_size/HEAP_SEGMENT;
+ uintptr_t *segment = (uintptr_t*)(block_shadow);
+
+ DLOG(" | === Block Shadow ======================================\n");
+ DLOG(" | Access addr: %a\n", addr);
+ DLOG(" | Block Shadow: %a\n", block_shadow);
+ DLOG(" | Init Shadow: %a\n", init_shadow);
+ DLOG(" | Segments: %lu\n", segments);
+ DLOG(" | Actual size: %lu bytes\n", alloc_size);
+ DLOG(" | Tracked Length: %lu bytes\n", length);
+
+ if (zeroed_out(block_shadow, alloc_size))
+ DLOG(" | << Nullified >> \n");
size_t i;
- for (i = 0; i < block_segments; i++) {
- uintptr_t *block_segment = (uintptr_t*)(shadowed + i*HEAP_SEGMENT);
- DLOG("%s | Block %2lu, Offset %3lu, Init: %"
- TOSTRING(HEAP_SEGMENT) "b\t\t || %a \n", i ? " " : "", i,
- block_segment[0], block_segment[1], block_segment);
+ for (i = 0; i < segments; i++) {
+ segment = (uintptr_t*)(block_shadow + i*HEAP_SEGMENT);
+ DLOG(" | Segment: %lu, Base: %a \n", i, *segment);
+ }
+
+ DLOG(" | Initialization: \n | ");
+ for (i = 0; i < alloc_size/8; i++) {
+ if (i > 0 && (i*8)%HEAP_SEGMENT == 0)
+ DLOG("\n | ");
+ DLOG("%8b ", init_shadow[i], init_shadow[i]);
}
DLOG("\n");
}
@@ -1195,22 +1253,16 @@ static void print_shadows(uintptr_t addr, size_t size) {
if (IS_ON_STATIC(addr))
print_static_shadows(addr, size);
else if (IS_ON_HEAP(addr))
- print_heap_shadows(addr, size);
+ print_heap_shadows(addr);
}
static void print_memory_segment(struct memory_segment *seg, const char *name) {
DLOG(" --- %s ------------------------------------------\n", name);
- DLOG("%s Shadow Size: %16lu MB\n", name, MB_SZ(seg->shadow_size));
- DLOG("%s Start: %19lu\n", name, seg->start);
- DLOG("%s End: %19lu\n", name, seg->end);
- DLOG("%s Primary Shadow Offset: %19lu\n", name, seg->prim_offset);
- DLOG("%s Primary Shadow Start: %19lu\n", name, seg->prim_start);
- DLOG("%s Primary Shadow End: %19lu\n", name, seg->prim_end);
- if (seg->sec_start) {
- DLOG("%s Secondary Shadow Offset: %19lu\n", name, seg->sec_offset);
- DLOG("%s Secondary Shadow Start: %19lu\n", name, seg->sec_start);
- DLOG("%s Secondary Shadow End: %19lu\n", name, seg->sec_end);
- }
+ DLOG("Segment: %lu MB [%a, %a]\n", MB_SZ(seg->size), seg->start, seg->end);
+ DLOG("Primary: %lu MB [%a, %a] {Offset: %lu}\n",
+ MB_SZ(seg->prim_size), seg->prim_start, seg->prim_end, seg->prim_offset);
+ DLOG("Secondary: %lu MB [%a, %a] {Offset: %lu}\n",
+ MB_SZ(seg->sec_size), seg->sec_start, seg->sec_end, seg->sec_offset);
}
static void print_memory_layout() {
diff --git a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_shadow_layout.h b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_shadow_layout.h
index afe67693198baa0603f74fffa61d121d46732c46..2a2ff24bf9acab6fe668f65924e779677f5ba0c5 100644
--- a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_shadow_layout.h
+++ b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_shadow_layout.h
@@ -68,7 +68,7 @@ char *strerror(int errnum);
/** Hardcoded sizes of tracked program segments {{{ */
/*! \brief Size of a program's heap */
-#define PGM_HEAP_SIZE (256 * MB)
+#define PGM_HEAP_SIZE (512 * MB)
/*! \brief Size of a program's Thread-local storage (TLS) */
#define PGM_TLS_SIZE (16 * MB)
@@ -136,8 +136,8 @@ static uintptr_t get_stack_start(int *argc_ref, char *** argv_ref) {
env++;
uintptr_t addr = (uintptr_t)*env + strlen(*env);
- /* When returning the end stack addess we need to make sure that
- * ::ULONG_BITS past that address are actually writable. This is
+ /* When returning the end stack address we need to make sure that
+ * ::ULONG_BITS past that address are actually writeable. This is
* to be able to set initialization and read-only bits ::ULONG_BITS
* at a time. If not respected, this may cause a segfault in
* ::argv_alloca. */
@@ -157,7 +157,7 @@ static void increase_stack_limit(const size_t size) {
rl.rlim_cur = stacksz;
result = setrlimit(RLIMIT_STACK, &rl);
if (result != 0) {
- vabort("setrlimit returned result = %d\n", result);
+ vabort("setrlimit: %s \n", strerror(errno));
}
}
}
@@ -175,6 +175,13 @@ static uintptr_t get_heap_start() {
static size_t get_heap_size() {
return PGM_HEAP_SIZE;
}
+
+/*! \brief Return the size of a secondary shadow region tracking
+ * initialization (i.e., init shadow). */
+static size_t get_heap_init_size() {
+ return get_heap_size()/8;
+}
+
/** }}} */
/** Program global information {{{ */
@@ -195,11 +202,12 @@ static size_t get_global_size() {
* pointer to its base address. Since this function is used to set-up shadowing
* the program is aborted if `mmap` fails to allocate a new memory block. */
static void *do_mmap(size_t size) {
- DLOG("<<< Request to allocate %lu bytes with mmap >>>\n", size);
void *res = mmap(0, size, PROT_READ|PROT_WRITE,
MAP_ANONYMOUS|MAP_PRIVATE, -1, (size_t)0);
- if (res == MAP_FAILED)
+ if (res == MAP_FAILED) {
+ DLOG("<<< Request to allocate %lu MB with mmap failed >>>\n", MB_SZ(size));
vabort("mmap error: %s\n", strerror(errno));
+ }
/* Make sure that mmap returned a fully nullified mapping */
DVASSERT(zeroed_out(res, size),
"Memory mapping of size %lu at address %a not fully nullified", size, res);
@@ -264,17 +272,20 @@ NOTE: With mmap allocations heap does not necessarily grows from program break
* shadow spaces. */
struct memory_segment {
const char *name;
- uintptr_t start; //!< Least address in application segment
- uintptr_t end; //!< Greatest address in application segment
-
- size_t shadow_size; //!< Byte-size of shadow area
-
- uintptr_t prim_start; //!< Least address in primary shadow
- uintptr_t prim_end; //!< Greatest address in primary shadow
+ uintptr_t start; //!< Least address in the application segment
+ uintptr_t end; //!< Greatest address in the application segment
+ uintptr_t size; //!< Size of the tracked segment in application memory
+ /* Primary shadow space */
+ size_t prim_size; //!< Byte-size of the primary shadow
+ size_t prim_ratio; //! Ratio of shadow to application memory
+ uintptr_t prim_start; //!< Least address in the primary shadow
+ uintptr_t prim_end; //!< Greatest address in the primary shadow
uintptr_t prim_offset; //!< Primary shadow offset
-
- uintptr_t sec_start; //!< Least address secondary shadow
- uintptr_t sec_end; //!< Greatest address secondary shadow
+ /* Secondary shadow space */
+ size_t sec_size; //!< Byte-size of shadow area
+ size_t sec_ratio; //! Ratio of shadow to application memory
+ uintptr_t sec_start; //!< Least address in the secondary shadow
+ uintptr_t sec_end; //!< Greatest address in the secondary shadow
uintptr_t sec_offset; //!< Secondary shadow offset
int initialized; //! Notion on whether the layout is initialized
@@ -291,24 +302,39 @@ struct memory_layout {
int initialized;
};
-/*! \brief Set a given memory segment and its shadow spaces. */
+/*! \brief Set a given memory segment and its shadow spaces.
+ *
+ * \param start - least address in an application's segment
+ * \param size - byte size of a tracked application's segment
+ * \param prim_ratio - compression ratio of the primary shadow segment
+ * \param sec_ratio - compression ratio of the secondary shadow segment
+ * \param name - segment name
+*/
static void set_shadow_segment(struct memory_segment *seg, uintptr_t start,
- size_t size, int secondary, const char *name) {
- DLOG("<<< Initialize %s segment of %lu MB >>>\n", name, size/MB);
- seg -> name = name;
- seg->start = start;
- seg->end = seg->start + size - 1;
- seg->shadow_size = size;
+ size_t size, size_t prim_ratio, size_t sec_ratio, const char *name) {
- void *prim_shadow = do_mmap(seg->shadow_size);
- seg->prim_start = (uintptr_t)prim_shadow;
- seg->prim_end = seg->prim_start + seg->shadow_size - 1;
- seg->prim_offset = shadow_offset(prim_shadow, start);
+ seg->name = name;
+ seg->start = start;
+ seg->size = size;
+ seg->end = seg->start + seg->size - 1;
+
+ if (prim_ratio) {
+ seg->prim_ratio = prim_ratio;
+ seg->prim_size = seg->size/seg->prim_ratio;
+ void *prim_shadow = do_mmap(seg->prim_size);
+ seg->prim_start = (uintptr_t)prim_shadow;
+ seg->prim_end = seg->prim_start + seg->prim_size - 1;
+ seg->prim_offset = shadow_offset(prim_shadow, start);
+ } else {
+ seg->prim_start = seg->prim_end = seg->prim_offset = 0;
+ }
- if (secondary) {
- void *sec_shadow = do_mmap(seg->shadow_size);
+ if (sec_ratio) {
+ seg->sec_ratio = sec_ratio;
+ seg->sec_size = seg->size/seg->sec_ratio;
+ void *sec_shadow = do_mmap(seg->sec_size);
seg->sec_start = (uintptr_t)sec_shadow;
- seg->sec_end = seg->sec_start + seg->shadow_size - 1;
+ seg->sec_end = seg->sec_start + seg->sec_size - 1;
seg->sec_offset = shadow_offset(sec_shadow, seg->start);
} else {
seg->sec_start = seg->sec_end = seg->sec_offset = 0;
@@ -319,32 +345,34 @@ static void set_shadow_segment(struct memory_segment *seg, uintptr_t start,
* allocate shadow memory spaces and compute offsets. This function populates
* global struct ::mem_layout holding that information with data. */
static void init_memory_layout(int *argc_ref, char ***argv_ref) {
+ /* Use DEBUG_PRINT_LAYOUT to output the details (if they are needed) */
set_shadow_segment(&mem_layout.heap,
- get_heap_start(), get_heap_size(), 0, "heap");
+ get_heap_start(), get_heap_size(), 1, 8, "heap");
set_shadow_segment(&mem_layout.stack,
- get_stack_start(argc_ref, argv_ref), get_stack_size(), 1, "stack");
+ get_stack_start(argc_ref, argv_ref), get_stack_size(), 1, 1, "stack");
set_shadow_segment(&mem_layout.global,
- get_global_start(), get_global_size(), 1, "global");
+ get_global_start(), get_global_size(), 1, 1, "global");
set_shadow_segment(&mem_layout.tls,
- get_tls_start(), get_tls_size(), 1, "tls");
+ get_tls_start(), get_tls_size(), 1, 1, "tls");
mem_layout.initialized = 1;
}
/*! \brief Deallocate a shadow segment */
-void clean_memory_segment(struct memory_segment *seg, int secondary) {
- munmap((void*)seg->prim_start, seg->shadow_size);
- if (secondary)
- munmap((void*)seg->sec_start, seg->shadow_size);
+void clean_memory_segment(struct memory_segment *seg) {
+ if (seg->prim_start)
+ munmap((void*)seg->prim_start, seg->prim_size);
+ if (seg->sec_start)
+ munmap((void*)seg->sec_start, seg->prim_size);
}
/*! \brief Deallocate shadow regions used by runtime analysis */
static void clean_memory_layout() {
DLOG("<<< Clean shadow layout >>>\n");
if (mem_layout.initialized) {
- clean_memory_segment(&mem_layout.heap, 0);
- clean_memory_segment(&mem_layout.stack, 1);
- clean_memory_segment(&mem_layout.global, 1);
- clean_memory_segment(&mem_layout.tls, 1);
+ clean_memory_segment(&mem_layout.heap);
+ clean_memory_segment(&mem_layout.stack);
+ clean_memory_segment(&mem_layout.global);
+ clean_memory_segment(&mem_layout.tls);
}
}
/* }}} */
@@ -381,6 +409,24 @@ static void clean_memory_layout() {
#define HIGHER_SHADOW_ACCESS(_addr,_offset) \
SHADOW_ACCESS(_addr,_offset,+)
+/*! \brief Same as SHADOW_ACCESS but with an additional scale factor given via
+ * _scale argument. Scale factor describes ratio of application to shadow bytes,
+ * for instance if one bit shadow memory is used to track one byte of
+ * application memory then the scale factor is 8. */
+#define SCALED_SHADOW_ACCESS(_addr,_start,_offset,_scale,_direction) \
+ (_addr _direction \
+ (_offset - \
+ ((uintptr_t)_addr - _start) + \
+ ((uintptr_t)_addr - _start)/_scale))
+
+/*! \brief Same as `LOWER_SHADOW_ACCESS` but with an additional scale factor */
+#define LOWER_SCALED_SHADOW_ACCESS(_addr,_start,_offset,_scale) \
+ SCALED_SHADOW_ACCESS(_addr,_start,_offset,_scale, -)
+
+/*! \brief Same as `HIGHER_SHADOW_ACCESS` but with an additional scale factor */
+#define HIGHER_SCALED_SHADOW_ACCESS(_addr,_start,_offset,_scale) \
+ SCALED_SHADOW_ACCESS(_addr,_start,_offset,_scale, +)
+
/*! \brief Convert a stack address into its primary shadow counterpart */
#define PRIMARY_STACK_SHADOW(_addr) \
LOWER_SHADOW_ACCESS(_addr, mem_layout.stack.prim_offset)
@@ -421,6 +467,16 @@ static void clean_memory_layout() {
/*! \brief Convert a heap address into its shadow counterpart */
#define HEAP_SHADOW(_addr) \
HIGHER_SHADOW_ACCESS(_addr, mem_layout.heap.prim_offset)
+
+#define HEAP_START mem_layout.heap.start
+
+/*! \brief Convert a heap address into its init shadow counterpart */
+#define HEAP_INIT_SHADOW(_addr) \
+ HIGHER_SCALED_SHADOW_ACCESS(_addr, \
+ mem_layout.heap.start, \
+ mem_layout.heap.sec_offset, \
+ mem_layout.heap.sec_ratio)
+
/* }}} */
/** Memory segment ranges {{{ */
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 7cc4edfe216c6307c95229f8b11bb0ba03b30c96..5717cea664861ca0917acd17d42a8851651ba87e 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
@@ -121,13 +121,18 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__e_acsl_store_block((void *)(& Mtmin_out),(size_t)8);
__e_acsl_store_block((void *)(& Mwmin),(size_t)8);
__e_acsl_store_block((void *)(& Mtmin_in),(size_t)8);
- __gen_e_acsl_valid = __e_acsl_valid((void *)Mtmin_in,sizeof(float));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)Mtmin_in,sizeof(float),
+ (void *)Mtmin_in,
+ (void *)(& Mtmin_in));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",(char *)"bar",
(char *)"\\valid(Mtmin_in)",17);
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)Mwmin,sizeof(float));
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)Mwmin,sizeof(float),
+ (void *)Mwmin,(void *)(& Mwmin));
__e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Precondition",
(char *)"bar",(char *)"\\valid(Mwmin)",18);
- __gen_e_acsl_valid_3 = __e_acsl_valid((void *)Mtmin_out,sizeof(float));
+ __gen_e_acsl_valid_3 = __e_acsl_valid((void *)Mtmin_out,sizeof(float),
+ (void *)Mtmin_out,
+ (void *)(& Mtmin_out));
__e_acsl_assert(__gen_e_acsl_valid_3,(char *)"Precondition",
(char *)"bar",(char *)"\\valid(Mtmin_out)",19);
__gen_e_acsl_at_6 = Mwmin;
@@ -144,23 +149,31 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
int __gen_e_acsl_and;
int __gen_e_acsl_if;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)__gen_e_acsl_at_2,
- sizeof(float));
+ sizeof(float),
+ (void *)__gen_e_acsl_at_2,
+ (void *)(& __gen_e_acsl_at_2));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"bar",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at_2)",23);
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)__gen_e_acsl_at,
- sizeof(float));
+ sizeof(float),
+ (void *)__gen_e_acsl_at,
+ (void *)(& __gen_e_acsl_at));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"bar",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at)",23);
if (*__gen_e_acsl_at == *__gen_e_acsl_at_2) {
int __gen_e_acsl_valid_read_3;
int __gen_e_acsl_valid_read_4;
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)__gen_e_acsl_at_4,
- sizeof(float));
+ sizeof(float),
+ (void *)__gen_e_acsl_at_4,
+ (void *)(& __gen_e_acsl_at_4));
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"bar",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at_4)",
23);
__gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)__gen_e_acsl_at_3,
- sizeof(float));
+ sizeof(float),
+ (void *)__gen_e_acsl_at_3,
+ (void *)(& __gen_e_acsl_at_3));
__e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",(char *)"bar",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at_3)",
23);
@@ -170,7 +183,9 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
if (__gen_e_acsl_and) {
int __gen_e_acsl_valid_read_5;
__gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)__gen_e_acsl_at_5,
- sizeof(float));
+ sizeof(float),
+ (void *)__gen_e_acsl_at_5,
+ (void *)(& __gen_e_acsl_at_5));
__e_acsl_assert(__gen_e_acsl_valid_read_5,(char *)"RTE",(char *)"bar",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at_5)",
23);
@@ -179,7 +194,9 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
else {
int __gen_e_acsl_valid_read_6;
__gen_e_acsl_valid_read_6 = __e_acsl_valid_read((void *)__gen_e_acsl_at_6,
- sizeof(float));
+ sizeof(float),
+ (void *)__gen_e_acsl_at_6,
+ (void *)(& __gen_e_acsl_at_6));
__e_acsl_assert(__gen_e_acsl_valid_read_6,(char *)"RTE",(char *)"bar",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at_6)",
23);
@@ -217,13 +234,18 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
__e_acsl_store_block((void *)(& Mtmax_out),(size_t)8);
__e_acsl_store_block((void *)(& Mwmax),(size_t)8);
__e_acsl_store_block((void *)(& Mtmax_in),(size_t)8);
- __gen_e_acsl_valid = __e_acsl_valid((void *)Mtmax_in,sizeof(float));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)Mtmax_in,sizeof(float),
+ (void *)Mtmax_in,
+ (void *)(& Mtmax_in));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",(char *)"foo",
(char *)"\\valid(Mtmax_in)",5);
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)Mwmax,sizeof(float));
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)Mwmax,sizeof(float),
+ (void *)Mwmax,(void *)(& Mwmax));
__e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Precondition",
(char *)"foo",(char *)"\\valid(Mwmax)",6);
- __gen_e_acsl_valid_3 = __e_acsl_valid((void *)Mtmax_out,sizeof(float));
+ __gen_e_acsl_valid_3 = __e_acsl_valid((void *)Mtmax_out,sizeof(float),
+ (void *)Mtmax_out,
+ (void *)(& Mtmax_out));
__e_acsl_assert(__gen_e_acsl_valid_3,(char *)"Precondition",
(char *)"foo",(char *)"\\valid(Mtmax_out)",7);
__gen_e_acsl_at_3 = Mwmax;
@@ -236,15 +258,21 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
int __gen_e_acsl_valid_read_2;
int __gen_e_acsl_valid_read_3;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)__gen_e_acsl_at_3,
- sizeof(float));
+ sizeof(float),
+ (void *)__gen_e_acsl_at_3,
+ (void *)(& __gen_e_acsl_at_3));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"foo",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at_3)",11);
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)__gen_e_acsl_at_2,
- sizeof(float));
+ sizeof(float),
+ (void *)__gen_e_acsl_at_2,
+ (void *)(& __gen_e_acsl_at_2));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"foo",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at_2)",11);
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)__gen_e_acsl_at,
- sizeof(float));
+ sizeof(float),
+ (void *)__gen_e_acsl_at,
+ (void *)(& __gen_e_acsl_at));
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"foo",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at)",11);
__e_acsl_assert(*__gen_e_acsl_at == *__gen_e_acsl_at_2 + ((long double)5 -
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
index 22ff3c673342aadefb8e35967fd01932dd0f3d38..04cb8cbdf7534223386e6d7ad5e7ab96680c50fc 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
@@ -67,14 +67,17 @@ int __gen_e_acsl_sorted(int *t, int n)
int __gen_e_acsl_valid_read;
int __gen_e_acsl_valid_read_2;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(t + __gen_e_acsl_i),
- sizeof(int));
+ sizeof(int),(void *)t,
+ (void *)(& t));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",
(char *)"sorted",
(char *)"mem_access: \\valid_read(t + __gen_e_acsl_i)",
6);
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(t + (
__gen_e_acsl_i - 1L)),
- sizeof(int));
+ sizeof(int),
+ (void *)t,
+ (void *)(& t));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",
(char *)"sorted",
(char *)"mem_access: \\valid_read(t + (long)(__gen_e_acsl_i - 1))",
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 ab9d25dbf699d44b02f3ef9c205537dfdb309abb..847be00d2729b5edcb71933b1e8656473daeabcf 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
@@ -79,37 +79,49 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
int __gen_e_acsl_valid_read_5;
int __gen_e_acsl_valid_read_6;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(*__gen_e_acsl_at_6),
- sizeof(int));
+ sizeof(int),
+ (void *)(*__gen_e_acsl_at_6),
+ (void *)(*__gen_e_acsl_at_6));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",
(char *)"atp_NORMAL_computeAverageAccel",
(char *)"mem_access: \\valid_read((int *)*__gen_e_acsl_at_6)",
8);
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_5)[1]),
- sizeof(int));
+ sizeof(int),
+ (void *)(& (*__gen_e_acsl_at_5)[1]),
+ (void *)(& (*__gen_e_acsl_at_5)[1]));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",
(char *)"atp_NORMAL_computeAverageAccel",
(char *)"mem_access: \\valid_read(&(*__gen_e_acsl_at_5)[1])",
8);
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_4)[2]),
- sizeof(int));
+ sizeof(int),
+ (void *)(& (*__gen_e_acsl_at_4)[2]),
+ (void *)(& (*__gen_e_acsl_at_4)[2]));
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",
(char *)"atp_NORMAL_computeAverageAccel",
(char *)"mem_access: \\valid_read(&(*__gen_e_acsl_at_4)[2])",
8);
__gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_3)[3]),
- sizeof(int));
+ sizeof(int),
+ (void *)(& (*__gen_e_acsl_at_3)[3]),
+ (void *)(& (*__gen_e_acsl_at_3)[3]));
__e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",
(char *)"atp_NORMAL_computeAverageAccel",
(char *)"mem_access: \\valid_read(&(*__gen_e_acsl_at_3)[3])",
8);
__gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_2)[4]),
- sizeof(int));
+ sizeof(int),
+ (void *)(& (*__gen_e_acsl_at_2)[4]),
+ (void *)(& (*__gen_e_acsl_at_2)[4]));
__e_acsl_assert(__gen_e_acsl_valid_read_5,(char *)"RTE",
(char *)"atp_NORMAL_computeAverageAccel",
(char *)"mem_access: \\valid_read(&(*__gen_e_acsl_at_2)[4])",
8);
__gen_e_acsl_valid_read_6 = __e_acsl_valid_read((void *)__gen_e_acsl_at,
- sizeof(int));
+ sizeof(int),
+ (void *)__gen_e_acsl_at,
+ (void *)(& __gen_e_acsl_at));
__e_acsl_assert(__gen_e_acsl_valid_read_6,(char *)"RTE",
(char *)"atp_NORMAL_computeAverageAccel",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at)",8);
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 b3b07a810c4810f60ea45889e8a3a4ba0875f260..d162a6aa8af1d3950d49a402bad992c1dd71b1b4 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
@@ -86,7 +86,9 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
{
int __gen_e_acsl_valid_read_3;
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)((char *)buf + __gen_e_acsl_k),
- sizeof(char));
+ sizeof(char),
+ (void *)buf,
+ (void *)(& buf));
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",
(char *)"memchr",
(char *)"mem_access: \\valid_read((char *)buf + __gen_e_acsl_k)",
@@ -114,7 +116,9 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
{
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)((char *)buf + __gen_e_acsl_i),
- sizeof(char));
+ sizeof(char),
+ (void *)buf,
+ (void *)(& buf));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",
(char *)"memchr",
(char *)"mem_access: \\valid_read((char *)buf + __gen_e_acsl_i)",
@@ -151,7 +155,9 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
{
int __gen_e_acsl_valid_read_2;
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)((char *)__gen_e_acsl_at_2 + __gen_e_acsl_j),
- sizeof(char));
+ sizeof(char),
+ (void *)__gen_e_acsl_at_2,
+ (void *)(& __gen_e_acsl_at_2));
__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)",
@@ -189,11 +195,11 @@ void __e_acsl_globals_init(void)
__gen_e_acsl_literal_string = "toto";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string,sizeof("toto"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string);
- __e_acsl_readonly((void *)__gen_e_acsl_literal_string);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
__gen_e_acsl_literal_string_2 = "tata";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,sizeof("tata"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
- __e_acsl_readonly((void *)__gen_e_acsl_literal_string_2);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_2);
return;
}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
index 6b0fb4d512e7d921fd31fe45a5d6486a8ccce33e..6e3a6dfa88ee40d0fd1d3c907dee3889c686d5da 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
@@ -29,7 +29,9 @@ void __gen_e_acsl_loop(void)
int __gen_e_acsl_valid;
__e_acsl_assert(global_i == 0,(char *)"Precondition",(char *)"loop",
(char *)"global_i == 0",9);
- __gen_e_acsl_valid = __e_acsl_valid((void *)global_i_ptr,sizeof(int));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)global_i_ptr,sizeof(int),
+ (void *)global_i_ptr,
+ (void *)(& global_i_ptr));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",(char *)"loop",
(char *)"\\valid(global_i_ptr)",10);
__e_acsl_assert(global_i_ptr == & global_i,(char *)"Precondition",
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
index 0170ff8665ae278e2536dd65456af82665ca79d6..17c06da00028f0507772d51ccfa8a71c55f5cd43 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
@@ -14,7 +14,8 @@ int main(void)
/*@ assert \valid(&s); */
{
int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)(& s),sizeof(struct toto));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)(& s),sizeof(struct toto),
+ (void *)(& s),(void *)(& s));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"main",
(char *)"\\valid(&s)",9);
}
@@ -28,7 +29,8 @@ int main(void)
sizeof(struct toto *));
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid_2;
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)p,sizeof(struct toto));
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)p,sizeof(struct toto),
+ (void *)p,(void *)(& p));
__gen_e_acsl_and = __gen_e_acsl_valid_2;
}
else __gen_e_acsl_and = 0;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
index cdf251232dd40241b8adc40535bdfaad166fd255..8849e28f584d838d51d8ca051fbd5b9802932821 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
@@ -19,7 +19,8 @@ int main(void)
sizeof(int *));
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),(void *)p,
+ (void *)(& p));
__gen_e_acsl_and = __gen_e_acsl_valid;
}
else __gen_e_acsl_and = 0;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
index ac14adc8208dad17a2bb801052e7cdeab0bc7924..6a1f48467405e520ce022c13c0ce394a8edcf3f6 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
@@ -19,7 +19,8 @@ int main(void)
sizeof(int *));
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),(void *)p,
+ (void *)(& p));
__gen_e_acsl_and = __gen_e_acsl_valid;
}
else __gen_e_acsl_and = 0;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
index 8a8c2d0efb0e6345b3ce1dc5c46df9c181b6efa7..1be5aa98ba9199f85d66a4d0da156a02c667e2b9 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
@@ -20,7 +20,8 @@ int main(void)
sizeof(int *));
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),(void *)p,
+ (void *)(& p));
__gen_e_acsl_and = __gen_e_acsl_valid;
}
else __gen_e_acsl_and = 0;
@@ -41,7 +42,8 @@ int main(void)
if (__gen_e_acsl_initialized_2) {
int __gen_e_acsl_valid_2;
/*@ assert Value: dangling_pointer: ¬\dangling(&p); */
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)p,sizeof(int),
+ (void *)p,(void *)(& p));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
}
else __gen_e_acsl_and_2 = 0;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
index d84585a438def65bbddfabf6fd213f19a16ae358..26fe680be04f9f5a32ed9b49e43e941e3a6751a8 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
@@ -16,7 +16,8 @@ int f(void)
/*@ assert \valid_read(S); */
{
int __gen_e_acsl_valid_read;
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)S,sizeof(char));
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)S,sizeof(char),
+ (void *)S,(void *)(& S));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"Assertion",(char *)"f",
(char *)"\\valid_read(S)",10);
}
@@ -29,7 +30,9 @@ int f(void)
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid_read_2;
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)s1,
- sizeof(char));
+ sizeof(char),
+ (void *)s1,
+ (void *)(& s1));
__gen_e_acsl_and = __gen_e_acsl_valid_read_2;
}
else __gen_e_acsl_and = 0;
@@ -45,7 +48,9 @@ int f(void)
if (__gen_e_acsl_initialized_2) {
int __gen_e_acsl_valid_read_3;
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)s2,
- sizeof(char));
+ sizeof(char),
+ (void *)s2,
+ (void *)(& s2));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_read_3;
}
else __gen_e_acsl_and_2 = 0;
@@ -63,15 +68,15 @@ void __e_acsl_globals_init(void)
__gen_e_acsl_literal_string_3 = "toto";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_3,sizeof("toto"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_3);
- __e_acsl_readonly((void *)__gen_e_acsl_literal_string_3);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_3);
__gen_e_acsl_literal_string = "foo";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string,sizeof("foo"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string);
- __e_acsl_readonly((void *)__gen_e_acsl_literal_string);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
__gen_e_acsl_literal_string_2 = "bar";
__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_mark_readonly((void *)__gen_e_acsl_literal_string_2);
__e_acsl_store_block((void *)(& S),(size_t)8);
__e_acsl_full_init((void *)(& S));
return;
@@ -105,7 +110,9 @@ int main(void)
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)s,
- sizeof(char));
+ sizeof(char),
+ (void *)s,
+ (void *)(& s));
__gen_e_acsl_and = __gen_e_acsl_valid_read;
}
else __gen_e_acsl_and = 0;
@@ -120,7 +127,8 @@ int main(void)
sizeof(char *));
if (__gen_e_acsl_initialized_2) {
int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)s,sizeof(char));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)s,sizeof(char),
+ (void *)s,(void *)(& s));
__gen_e_acsl_and_2 = __gen_e_acsl_valid;
}
else __gen_e_acsl_and_2 = 0;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c
index 5e8086f82bea77b224d55d81d889ebe7697f0768..4ea2172ad1471759b70afc0abce442beb023b5e5 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c
@@ -15,12 +15,12 @@ void __e_acsl_globals_init(void)
__e_acsl_store_block((void *)__gen_e_acsl_literal_string,
sizeof("Struct_G[1]"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string);
- __e_acsl_readonly((void *)__gen_e_acsl_literal_string);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
__gen_e_acsl_literal_string_2 = "Struct_G[0]";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,
sizeof("Struct_G[0]"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
- __e_acsl_readonly((void *)__gen_e_acsl_literal_string_2);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_2);
__e_acsl_store_block((void *)(_G),(size_t)32);
__e_acsl_full_init((void *)(& _G));
return;
@@ -40,7 +40,9 @@ int main(int argc, char **argv)
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)_G[0].str,
- sizeof(char));
+ sizeof(char),
+ (void *)_G[0].str,
+ (void *)(& _G[0].str));
__gen_e_acsl_and = __gen_e_acsl_valid_read;
}
else __gen_e_acsl_and = 0;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c
index f4dad2e66aaa4366edad123fbc03886896b6ccea..c56a8ba6a99fc28deda2c79dc3146c59fe5c74f0 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c
@@ -8,7 +8,7 @@ void __e_acsl_globals_init(void)
__gen_e_acsl_literal_string = "134";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string,sizeof("134"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string);
- __e_acsl_readonly((void *)__gen_e_acsl_literal_string);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
__e_acsl_store_block((void *)(& n),(size_t)8);
__e_acsl_full_init((void *)(& n));
return;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
index 40e382aaa79ce831c673bd5e35afe8397bfd07f2..c4b1763467a908e2b079af0fe924a827e6cb6584 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
@@ -14,7 +14,7 @@ void __e_acsl_globals_init(void)
__e_acsl_store_block((void *)__gen_e_acsl_literal_string,
sizeof("Test Code"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string);
- __e_acsl_readonly((void *)__gen_e_acsl_literal_string);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
return;
}
@@ -37,7 +37,9 @@ int main(void)
{
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(srcbuf + i),
- sizeof(char));
+ sizeof(char),
+ (void *)srcbuf,
+ (void *)(& srcbuf));
__e_acsl_assert(! __gen_e_acsl_valid_read,(char *)"Assertion",
(char *)"main",(char *)"!\\valid_read(srcbuf + i)",
16);
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 946f190171e905dfe251acbcae35c04d2d5dbf05..0be34f3867c94a594016eb9589084e0d1dd513c4 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
@@ -49,14 +49,17 @@ void g(int *p, int *q)
L1:
{
int __gen_e_acsl_valid_read_3;
- __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)q,sizeof(int));
+ __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)q,sizeof(int),
+ (void *)q,
+ (void *)(& q));
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"g",
(char *)"mem_access: \\valid_read(q)",28);
__gen_e_acsl_at_3 = *q;
}
{
int __gen_e_acsl_valid_read;
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)q,sizeof(int));
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)q,sizeof(int),
+ (void *)q,(void *)(& q));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"g",
(char *)"mem_access: \\valid_read(q)",26);
__gen_e_acsl_at = *q;
@@ -71,7 +74,8 @@ void g(int *p, int *q)
{
int __gen_e_acsl_valid_read_2;
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at),
- sizeof(int));
+ sizeof(int),(void *)p,
+ (void *)(& p));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"g",
(char *)"mem_access: \\valid_read(p + __gen_e_acsl_at)",
26);
@@ -86,7 +90,8 @@ void g(int *p, int *q)
{
int __gen_e_acsl_valid_read_4;
__gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at_3),
- sizeof(int));
+ sizeof(int),(void *)p,
+ (void *)(& p));
__e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",(char *)"g",
(char *)"mem_access: \\valid_read(p + __gen_e_acsl_at_3)",
28);
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 3a2801d937d13987851dbfb9077ff4049a036327..832354a78aa7c3b9a7165766abfc17b58e1206e8 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
@@ -106,14 +106,17 @@ void g(int *p, int *q)
L1:
{
int __gen_e_acsl_valid_read_3;
- __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)q,sizeof(int));
+ __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)q,sizeof(int),
+ (void *)q,
+ (void *)(& q));
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"g",
(char *)"mem_access: \\valid_read(q)",28);
__gen_e_acsl_at_3 = *q;
}
{
int __gen_e_acsl_valid_read;
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)q,sizeof(int));
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)q,sizeof(int),
+ (void *)q,(void *)(& q));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"g",
(char *)"mem_access: \\valid_read(q)",26);
__gen_e_acsl_at = *q;
@@ -129,7 +132,8 @@ void g(int *p, int *q)
int __gen_e_acsl_valid_read_2;
__e_acsl_mpz_t __gen_e_acsl_;
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at),
- sizeof(int));
+ sizeof(int),(void *)p,
+ (void *)(& p));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"g",
(char *)"mem_access: \\valid_read(p + __gen_e_acsl_at)",
26);
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c
index 807d9d488710d3686b2777ee7ed5745a9a630b6b..87cf1db55b4d8b9c98996d38cfc0f866b8f09e42 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c
@@ -201,7 +201,9 @@ int main(void)
{
int __gen_e_acsl_valid;
__gen_e_acsl_valid = __e_acsl_valid((void *)(& buf[__gen_e_acsl_i]),
- sizeof(int));
+ sizeof(int),
+ (void *)(& buf[__gen_e_acsl_i]),
+ (void *)(& buf[__gen_e_acsl_i]));
if (__gen_e_acsl_valid) ;
else {
__gen_e_acsl_forall_7 = 0;
@@ -227,7 +229,9 @@ int main(void)
{
int __gen_e_acsl_valid_2;
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& buf[__gen_e_acsl_i_2]),
- sizeof(int));
+ sizeof(int),
+ (void *)(& buf[__gen_e_acsl_i_2]),
+ (void *)(& buf[__gen_e_acsl_i_2]));
if (__gen_e_acsl_valid_2) ;
else {
__gen_e_acsl_forall_8 = 0;
@@ -253,7 +257,9 @@ int main(void)
{
int __gen_e_acsl_valid_3;
__gen_e_acsl_valid_3 = __e_acsl_valid((void *)(& buf[__gen_e_acsl_i_3]),
- sizeof(int));
+ sizeof(int),
+ (void *)(& buf[__gen_e_acsl_i_3]),
+ (void *)(& buf[__gen_e_acsl_i_3]));
if (__gen_e_acsl_valid_3) ;
else {
__gen_e_acsl_forall_9 = 0;
@@ -296,7 +302,9 @@ int main(void)
int __gen_e_acsl_valid_4;
__gen_e_acsl_i_5 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_i_4));
__gen_e_acsl_valid_4 = __e_acsl_valid((void *)(& buf[__gen_e_acsl_i_5]),
- sizeof(int));
+ sizeof(int),
+ (void *)(& buf[__gen_e_acsl_i_5]),
+ (void *)(& buf[__gen_e_acsl_i_5]));
if (__gen_e_acsl_valid_4) ;
else {
__gen_e_acsl_forall_10 = 0;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c
index f8c75fba789b78fd8380b2d0c7df285d847b7886..292fda22f4898a6937e641620ea4cf92ac185572 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c
@@ -621,7 +621,9 @@ int main(void)
int __gen_e_acsl_valid;
__gen_e_acsl_i_2 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_i));
__gen_e_acsl_valid = __e_acsl_valid((void *)(& buf[__gen_e_acsl_i_2]),
- sizeof(int));
+ sizeof(int),
+ (void *)(& buf[__gen_e_acsl_i_2]),
+ (void *)(& buf[__gen_e_acsl_i_2]));
if (__gen_e_acsl_valid) ;
else {
__gen_e_acsl_forall_7 = 0;
@@ -677,7 +679,9 @@ int main(void)
int __gen_e_acsl_valid_2;
__gen_e_acsl_i_4 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_i_3));
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& buf[__gen_e_acsl_i_4]),
- sizeof(int));
+ sizeof(int),
+ (void *)(& buf[__gen_e_acsl_i_4]),
+ (void *)(& buf[__gen_e_acsl_i_4]));
if (__gen_e_acsl_valid_2) ;
else {
__gen_e_acsl_forall_8 = 0;
@@ -733,7 +737,9 @@ int main(void)
int __gen_e_acsl_valid_3;
__gen_e_acsl_i_6 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_i_5));
__gen_e_acsl_valid_3 = __e_acsl_valid((void *)(& buf[__gen_e_acsl_i_6]),
- sizeof(int));
+ sizeof(int),
+ (void *)(& buf[__gen_e_acsl_i_6]),
+ (void *)(& buf[__gen_e_acsl_i_6]));
if (__gen_e_acsl_valid_3) ;
else {
__gen_e_acsl_forall_9 = 0;
@@ -789,7 +795,9 @@ int main(void)
int __gen_e_acsl_valid_4;
__gen_e_acsl_i_8 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_i_7));
__gen_e_acsl_valid_4 = __e_acsl_valid((void *)(& buf[__gen_e_acsl_i_8]),
- sizeof(int));
+ sizeof(int),
+ (void *)(& buf[__gen_e_acsl_i_8]),
+ (void *)(& buf[__gen_e_acsl_i_8]));
if (__gen_e_acsl_valid_4) ;
else {
__gen_e_acsl_forall_10 = 0;
diff --git a/src/plugins/e-acsl/tests/runtime/block_valid.c b/src/plugins/e-acsl/tests/runtime/block_valid.c
new file mode 100644
index 0000000000000000000000000000000000000000..16be7577c1028872881baebb97e579f0d6e47786
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/block_valid.c
@@ -0,0 +1,56 @@
+/* run.config
+ COMMENT: Check violations related to accessing an allocated memory block
+ COMMENT: through a pointer to another block
+*/
+
+#include <stdlib.h>
+#include <stdint.h>
+
+#define ADDROF(_a) ((uintptr_t)_a)
+
+int A = 1,
+ B = 2,
+ C = 3;
+
+int main(int argc, char **argv) {
+ int *p = NULL,
+ *q = NULL;
+
+ int a = 1,
+ b = 2,
+ c = 3;
+
+ p = &b;
+ /*@assert \valid(p); */
+ /* `p` points to `b`, `p+1` accesses either `a` or `c` */
+ /*@assert ! \valid(p+1); */
+
+ p = &B;
+ /*@assert \valid(p); */
+ /* `p` points to `B`, `p+1` accesses either `A` or `C` */
+ /*@assert ! \valid(p+1); */
+
+ char *pmin = (char*)malloc(sizeof(int));
+ char *pmax = (char*)malloc(sizeof(int));
+
+ /* Since `pmin` is allocated before `pmax` it is likely that the start
+ * address of `pmin` is less than the start address of `pmax`, still,
+ * just in case, make sure it is true and swap the addresses otherwise. */
+ if (ADDROF(pmin) > ADDROF(pmax)) {
+ char *t = pmin;
+ pmin = pmax;
+ pmax = t;
+ }
+
+ *pmin = 'P';
+ *pmax = 'L';
+
+ int diff = pmax - pmin;
+ /*@assert \valid(pmin); */
+ /*@assert \valid(pmax); */
+ /* Access `pmax` through `pmin` */
+ /*@assert ! \valid(pmin + diff); */
+ /* Access `pmin` through `pmax` */
+ /*@assert ! \valid(pmax - diff); */
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/block_valid.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/block_valid.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/block_valid.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/block_valid.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..f102d73fa2acd8532fc8b3156a5b88d60a33e687
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/oracle/block_valid.res.oracle
@@ -0,0 +1,8 @@
+[e-acsl] beginning translation.
+[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.
+tests/runtime/block_valid.c:39:[value] warning: pointer comparison. assert \pointer_comparable((void *)pmin, (void *)pmax);
+tests/runtime/block_valid.c:45:[value] warning: out of bounds write. assert \valid(pmin);
+tests/runtime/block_valid.c:46:[value] warning: out of bounds write. assert \valid(pmax);
+tests/runtime/block_valid.c:52:[value] warning: assertion got status unknown.
+tests/runtime/block_valid.c:54:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_block_valid.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_block_valid.c
new file mode 100644
index 0000000000000000000000000000000000000000..647000e85831e18a450745271bf223edacf7c23a
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_block_valid.c
@@ -0,0 +1,163 @@
+/* Generated by Frama-C */
+#include "stdlib.h"
+int A = 1;
+int B = 2;
+int C = 3;
+void __e_acsl_globals_init(void)
+{
+ __e_acsl_store_block((void *)(& B),(size_t)4);
+ __e_acsl_full_init((void *)(& B));
+ return;
+}
+
+int main(int argc, char **argv)
+{
+ int __retres;
+ __e_acsl_memory_init(& argc,& argv,(size_t)8);
+ __e_acsl_globals_init();
+ int *p = (int *)0;
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_full_init((void *)(& p));
+ int *q = (int *)0;
+ int a = 1;
+ int b = 2;
+ __e_acsl_store_block((void *)(& b),(size_t)4);
+ __e_acsl_full_init((void *)(& b));
+ int c = 3;
+ __e_acsl_full_init((void *)(& p));
+ p = & b;
+ /*@ assert \valid(p); */
+ {
+ int __gen_e_acsl_initialized;
+ int __gen_e_acsl_and;
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& p),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized) {
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),(void *)p,
+ (void *)(& p));
+ __gen_e_acsl_and = __gen_e_acsl_valid;
+ }
+ else __gen_e_acsl_and = 0;
+ __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(p)",24);
+ }
+ /*@ assert ¬\valid(p + 1); */
+ {
+ int __gen_e_acsl_valid_2;
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(p + 1),sizeof(int),
+ (void *)p,(void *)(& p));
+ __e_acsl_assert(! __gen_e_acsl_valid_2,(char *)"Assertion",
+ (char *)"main",(char *)"!\\valid(p + 1)",26);
+ }
+ __e_acsl_full_init((void *)(& p));
+ p = & B;
+ /*@ assert \valid(p); */
+ {
+ int __gen_e_acsl_initialized_2;
+ int __gen_e_acsl_and_2;
+ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& p),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_2) {
+ int __gen_e_acsl_valid_3;
+ __gen_e_acsl_valid_3 = __e_acsl_valid((void *)p,sizeof(int),(void *)p,
+ (void *)(& p));
+ __gen_e_acsl_and_2 = __gen_e_acsl_valid_3;
+ }
+ else __gen_e_acsl_and_2 = 0;
+ __e_acsl_assert(__gen_e_acsl_and_2,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(p)",29);
+ }
+ /*@ assert ¬\valid(p + 1); */
+ {
+ int __gen_e_acsl_valid_4;
+ __gen_e_acsl_valid_4 = __e_acsl_valid((void *)(p + 1),sizeof(int),
+ (void *)p,(void *)(& p));
+ __e_acsl_assert(! __gen_e_acsl_valid_4,(char *)"Assertion",
+ (char *)"main",(char *)"!\\valid(p + 1)",31);
+ }
+ char *pmin = malloc(sizeof(int));
+ __e_acsl_store_block((void *)(& pmin),(size_t)8);
+ __e_acsl_full_init((void *)(& pmin));
+ char *pmax = malloc(sizeof(int));
+ __e_acsl_store_block((void *)(& pmax),(size_t)8);
+ __e_acsl_full_init((void *)(& pmax));
+ /*@ assert
+ Value: ptr_comparison: \pointer_comparable((void *)pmin, (void *)pmax);
+ */
+ if ((unsigned long)pmin > (unsigned long)pmax) {
+ char *t = pmin;
+ __e_acsl_store_block((void *)(& t),(size_t)8);
+ __e_acsl_full_init((void *)(& t));
+ __e_acsl_full_init((void *)(& pmin));
+ pmin = pmax;
+ __e_acsl_full_init((void *)(& pmax));
+ pmax = t;
+ __e_acsl_delete_block((void *)(& t));
+ }
+ __e_acsl_initialize((void *)pmin,sizeof(char));
+ /*@ assert Value: mem_access: \valid(pmin); */
+ *pmin = (char)'P';
+ __e_acsl_initialize((void *)pmax,sizeof(char));
+ /*@ assert Value: mem_access: \valid(pmax); */
+ *pmax = (char)'L';
+ int diff = (int)(pmax - pmin);
+ /*@ assert \valid(pmin); */
+ {
+ int __gen_e_acsl_initialized_3;
+ int __gen_e_acsl_and_3;
+ __gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)(& pmin),
+ sizeof(char *));
+ if (__gen_e_acsl_initialized_3) {
+ int __gen_e_acsl_valid_5;
+ __gen_e_acsl_valid_5 = __e_acsl_valid((void *)pmin,sizeof(char),
+ (void *)pmin,(void *)(& pmin));
+ __gen_e_acsl_and_3 = __gen_e_acsl_valid_5;
+ }
+ else __gen_e_acsl_and_3 = 0;
+ __e_acsl_assert(__gen_e_acsl_and_3,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(pmin)",49);
+ }
+ /*@ assert \valid(pmax); */
+ {
+ int __gen_e_acsl_initialized_4;
+ int __gen_e_acsl_and_4;
+ __gen_e_acsl_initialized_4 = __e_acsl_initialized((void *)(& pmax),
+ sizeof(char *));
+ if (__gen_e_acsl_initialized_4) {
+ int __gen_e_acsl_valid_6;
+ __gen_e_acsl_valid_6 = __e_acsl_valid((void *)pmax,sizeof(char),
+ (void *)pmax,(void *)(& pmax));
+ __gen_e_acsl_and_4 = __gen_e_acsl_valid_6;
+ }
+ else __gen_e_acsl_and_4 = 0;
+ __e_acsl_assert(__gen_e_acsl_and_4,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(pmax)",50);
+ }
+ /*@ assert ¬\valid(pmin + diff); */
+ {
+ int __gen_e_acsl_valid_7;
+ __gen_e_acsl_valid_7 = __e_acsl_valid((void *)(pmin + diff),sizeof(char),
+ (void *)pmin,(void *)(& pmin));
+ __e_acsl_assert(! __gen_e_acsl_valid_7,(char *)"Assertion",
+ (char *)"main",(char *)"!\\valid(pmin + diff)",52);
+ }
+ /*@ assert ¬\valid(pmax - diff); */
+ {
+ int __gen_e_acsl_valid_8;
+ __gen_e_acsl_valid_8 = __e_acsl_valid((void *)(pmax - diff),sizeof(char),
+ (void *)pmax,(void *)(& pmax));
+ __e_acsl_assert(! __gen_e_acsl_valid_8,(char *)"Assertion",
+ (char *)"main",(char *)"!\\valid(pmax - diff)",54);
+ }
+ __retres = 0;
+ __e_acsl_delete_block((void *)(& B));
+ __e_acsl_delete_block((void *)(& pmax));
+ __e_acsl_delete_block((void *)(& pmin));
+ __e_acsl_delete_block((void *)(& b));
+ __e_acsl_delete_block((void *)(& p));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c
index 764f19cd894ff68db95cb5b0a205d84d6071ffe1..7787974a78645a3f0769e05b917875be64023ed0 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c
@@ -15,7 +15,8 @@ int main(int argc, char const **argv)
/*@ assert \valid(&p); */
{
int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)(& p),sizeof(int *));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)(& p),sizeof(int *),
+ (void *)(& p),(void *)(& p));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"main",
(char *)"\\valid(&p)",13);
__e_acsl_delete_block((void *)(& p));
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_compound_initializers.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_compound_initializers.c
index a16228735c86893207795bdcad39784861c62f2c..79bcb004e84c6ae14ff66c70a9327721f7b5fd89 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_compound_initializers.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_compound_initializers.c
@@ -24,24 +24,24 @@ void __e_acsl_globals_init(void)
__gen_e_acsl_literal_string_3 = "ZZ";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_3,sizeof("ZZ"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_3);
- __e_acsl_readonly((void *)__gen_e_acsl_literal_string_3);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_3);
__gen_e_acsl_literal_string = "YY";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string,sizeof("YY"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string);
- __e_acsl_readonly((void *)__gen_e_acsl_literal_string);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
__gen_e_acsl_literal_string_2 = "XX";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,sizeof("XX"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
- __e_acsl_readonly((void *)__gen_e_acsl_literal_string_2);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_2);
__gen_e_acsl_literal_string_4 = "Second";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_4,
sizeof("Second"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_4);
- __e_acsl_readonly((void *)__gen_e_acsl_literal_string_4);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_4);
__gen_e_acsl_literal_string_5 = "First";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_5,sizeof("First"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_5);
- __e_acsl_readonly((void *)__gen_e_acsl_literal_string_5);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_5);
__e_acsl_store_block((void *)(_G),(size_t)32);
__e_acsl_full_init((void *)(& _G));
__e_acsl_store_block((void *)(& _E),(size_t)4);
@@ -67,7 +67,8 @@ int main(int argc, char **argv)
/*@ assert \valid((char **)_A); */
{
int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)(_A),sizeof(char *));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)(_A),sizeof(char *),
+ (void *)(_A),(void *)(_A));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"main",
(char *)"\\valid((char **)_A)",33);
}
@@ -80,7 +81,9 @@ int main(int argc, char **argv)
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)_A[0],
- sizeof(char));
+ sizeof(char),
+ (void *)_A[0],
+ (void *)(_A));
__gen_e_acsl_and = __gen_e_acsl_valid_read;
}
else __gen_e_acsl_and = 0;
@@ -96,7 +99,9 @@ int main(int argc, char **argv)
if (__gen_e_acsl_initialized_2) {
int __gen_e_acsl_valid_read_2;
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)_A[1],
- sizeof(char));
+ sizeof(char),
+ (void *)_A[1],
+ (void *)(& _A[1]));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_read_2;
}
else __gen_e_acsl_and_2 = 0;
@@ -106,35 +111,41 @@ int main(int argc, char **argv)
/*@ assert \valid_read(_B); */
{
int __gen_e_acsl_valid_read_3;
- __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)_B,sizeof(char));
+ __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)_B,sizeof(char),
+ (void *)_B,
+ (void *)(& _B));
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"Assertion",
(char *)"main",(char *)"\\valid_read(_B)",36);
}
/*@ assert \valid(&_C); */
{
int __gen_e_acsl_valid_2;
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& _C),sizeof(char *));
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& _C),sizeof(char *),
+ (void *)(& _C),(void *)(& _C));
__e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Assertion",(char *)"main",
(char *)"\\valid(&_C)",37);
}
/*@ assert \valid((int *)_D); */
{
int __gen_e_acsl_valid_3;
- __gen_e_acsl_valid_3 = __e_acsl_valid((void *)(_D),sizeof(int));
+ __gen_e_acsl_valid_3 = __e_acsl_valid((void *)(_D),sizeof(int),
+ (void *)(_D),(void *)(_D));
__e_acsl_assert(__gen_e_acsl_valid_3,(char *)"Assertion",(char *)"main",
(char *)"\\valid((int *)_D)",38);
}
/*@ assert \valid(&_E); */
{
int __gen_e_acsl_valid_4;
- __gen_e_acsl_valid_4 = __e_acsl_valid((void *)(& _E),sizeof(int));
+ __gen_e_acsl_valid_4 = __e_acsl_valid((void *)(& _E),sizeof(int),
+ (void *)(& _E),(void *)(& _E));
__e_acsl_assert(__gen_e_acsl_valid_4,(char *)"Assertion",(char *)"main",
(char *)"\\valid(&_E)",39);
}
/*@ assert \valid(&_F); */
{
int __gen_e_acsl_valid_5;
- __gen_e_acsl_valid_5 = __e_acsl_valid((void *)(& _F),sizeof(int));
+ __gen_e_acsl_valid_5 = __e_acsl_valid((void *)(& _F),sizeof(int),
+ (void *)(& _F),(void *)(& _F));
__e_acsl_assert(__gen_e_acsl_valid_5,(char *)"Assertion",(char *)"main",
(char *)"\\valid(&_F)",40);
}
@@ -145,7 +156,8 @@ int main(int argc, char **argv)
{
int __gen_e_acsl_valid_6;
__gen_e_acsl_valid_6 = __e_acsl_valid((void *)(& _G),
- sizeof(struct ST [2]));
+ sizeof(struct ST [2]),
+ (void *)(& _G),(void *)(& _G));
__e_acsl_assert(__gen_e_acsl_valid_6,(char *)"Assertion",(char *)"main",
(char *)"\\valid(&_G)",42);
}
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_ctype_macros.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_ctype_macros.c
index 951c2559308ad3597666381bd03d960a5b65b43d..aaed0eb2d73a75f3af1620603b65fe959701555f 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_ctype_macros.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_ctype_macros.c
@@ -21,7 +21,8 @@ int main(int argc, char const **argv)
sizeof(char *));
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)d,sizeof(char));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)d,sizeof(char),(void *)d,
+ (void *)(& d));
__gen_e_acsl_and = __gen_e_acsl_valid;
}
else __gen_e_acsl_and = 0;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c
index 780fc3a88c485032c5b28a14fc41c147ebdec8d3..3f1e85b9d1564ccab6b073ed178b435cc1a9ac7d 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c
@@ -19,7 +19,8 @@ int goto_bts(void)
sizeof(int *));
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),(void *)p,
+ (void *)(& p));
__gen_e_acsl_and = __gen_e_acsl_valid;
}
else __gen_e_acsl_and = 0;
@@ -40,7 +41,8 @@ int goto_bts(void)
if (__gen_e_acsl_initialized_2) {
int __gen_e_acsl_valid_2;
/*@ assert Value: dangling_pointer: ¬\dangling(&p); */
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)p,sizeof(int),
+ (void *)p,(void *)(& p));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
}
else __gen_e_acsl_and_2 = 0;
@@ -104,7 +106,8 @@ int goto_valid(void)
sizeof(int *));
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),
+ (void *)p,(void *)(& p));
__gen_e_acsl_and = __gen_e_acsl_valid;
}
else __gen_e_acsl_and = 0;
@@ -120,7 +123,8 @@ int goto_valid(void)
if (__gen_e_acsl_initialized_2) {
int __gen_e_acsl_valid_2;
/*@ assert Value: dangling_pointer: ¬\dangling(&q); */
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)q,sizeof(int));
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)q,sizeof(int),
+ (void *)q,(void *)(& q));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
}
else __gen_e_acsl_and_2 = 0;
@@ -136,7 +140,8 @@ int goto_valid(void)
if (__gen_e_acsl_initialized_3) {
int __gen_e_acsl_valid_3;
/*@ assert Value: dangling_pointer: ¬\dangling(&r); */
- __gen_e_acsl_valid_3 = __e_acsl_valid((void *)r,sizeof(int));
+ __gen_e_acsl_valid_3 = __e_acsl_valid((void *)r,sizeof(int),
+ (void *)r,(void *)(& r));
__gen_e_acsl_and_3 = __gen_e_acsl_valid_3;
}
else __gen_e_acsl_and_3 = 0;
@@ -165,7 +170,8 @@ int goto_valid(void)
if (__gen_e_acsl_initialized_4) {
int __gen_e_acsl_valid_4;
/*@ assert Value: dangling_pointer: ¬\dangling(&p); */
- __gen_e_acsl_valid_4 = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_valid_4 = __e_acsl_valid((void *)p,sizeof(int),
+ (void *)p,(void *)(& p));
__gen_e_acsl_and_4 = __gen_e_acsl_valid_4;
}
else __gen_e_acsl_and_4 = 0;
@@ -181,7 +187,8 @@ int goto_valid(void)
if (__gen_e_acsl_initialized_5) {
int __gen_e_acsl_valid_5;
/*@ assert Value: dangling_pointer: ¬\dangling(&q); */
- __gen_e_acsl_valid_5 = __e_acsl_valid((void *)q,sizeof(int));
+ __gen_e_acsl_valid_5 = __e_acsl_valid((void *)q,sizeof(int),
+ (void *)q,(void *)(& q));
__gen_e_acsl_and_5 = __gen_e_acsl_valid_5;
}
else __gen_e_acsl_and_5 = 0;
@@ -197,7 +204,8 @@ int goto_valid(void)
if (__gen_e_acsl_initialized_6) {
int __gen_e_acsl_valid_6;
/*@ assert Value: dangling_pointer: ¬\dangling(&r); */
- __gen_e_acsl_valid_6 = __e_acsl_valid((void *)r,sizeof(int));
+ __gen_e_acsl_valid_6 = __e_acsl_valid((void *)r,sizeof(int),
+ (void *)r,(void *)(& r));
__gen_e_acsl_and_6 = __gen_e_acsl_valid_6;
}
else __gen_e_acsl_and_6 = 0;
@@ -247,7 +255,8 @@ int switch_valid(void)
sizeof(int *));
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),
+ (void *)p,(void *)(& p));
__gen_e_acsl_and = __gen_e_acsl_valid;
}
else __gen_e_acsl_and = 0;
@@ -262,7 +271,8 @@ int switch_valid(void)
sizeof(int *));
if (__gen_e_acsl_initialized_2) {
int __gen_e_acsl_valid_2;
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)q,sizeof(int));
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)q,sizeof(int),
+ (void *)q,(void *)(& q));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
}
else __gen_e_acsl_and_2 = 0;
@@ -277,7 +287,8 @@ int switch_valid(void)
sizeof(int *));
if (__gen_e_acsl_initialized_3) {
int __gen_e_acsl_valid_3;
- __gen_e_acsl_valid_3 = __e_acsl_valid((void *)s,sizeof(int));
+ __gen_e_acsl_valid_3 = __e_acsl_valid((void *)s,sizeof(int),
+ (void *)s,(void *)(& s));
__gen_e_acsl_and_3 = __gen_e_acsl_valid_3;
}
else __gen_e_acsl_and_3 = 0;
@@ -309,7 +320,8 @@ int switch_valid(void)
if (__gen_e_acsl_initialized_4) {
int __gen_e_acsl_valid_4;
/*@ assert Value: dangling_pointer: ¬\dangling(&q); */
- __gen_e_acsl_valid_4 = __e_acsl_valid((void *)q,sizeof(int));
+ __gen_e_acsl_valid_4 = __e_acsl_valid((void *)q,sizeof(int),(void *)q,
+ (void *)(& q));
__gen_e_acsl_and_4 = __gen_e_acsl_valid_4;
}
else __gen_e_acsl_and_4 = 0;
@@ -325,7 +337,8 @@ int switch_valid(void)
if (__gen_e_acsl_initialized_5) {
int __gen_e_acsl_valid_5;
/*@ assert Value: dangling_pointer: ¬\dangling(&p); */
- __gen_e_acsl_valid_5 = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_valid_5 = __e_acsl_valid((void *)p,sizeof(int),(void *)p,
+ (void *)(& p));
__gen_e_acsl_and_5 = __gen_e_acsl_valid_5;
}
else __gen_e_acsl_and_5 = 0;
@@ -340,7 +353,8 @@ int switch_valid(void)
sizeof(int *));
if (__gen_e_acsl_initialized_6) {
int __gen_e_acsl_valid_6;
- __gen_e_acsl_valid_6 = __e_acsl_valid((void *)s,sizeof(int));
+ __gen_e_acsl_valid_6 = __e_acsl_valid((void *)s,sizeof(int),(void *)s,
+ (void *)(& s));
__gen_e_acsl_and_6 = __gen_e_acsl_valid_6;
}
else __gen_e_acsl_and_6 = 0;
@@ -394,7 +408,8 @@ int while_valid(void)
sizeof(int *));
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),
+ (void *)p,(void *)(& p));
__gen_e_acsl_and = __gen_e_acsl_valid;
}
else __gen_e_acsl_and = 0;
@@ -409,7 +424,8 @@ int while_valid(void)
sizeof(int *));
if (__gen_e_acsl_initialized_2) {
int __gen_e_acsl_valid_2;
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)q,sizeof(int));
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)q,sizeof(int),
+ (void *)q,(void *)(& q));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
}
else __gen_e_acsl_and_2 = 0;
@@ -424,7 +440,8 @@ int while_valid(void)
sizeof(int *));
if (__gen_e_acsl_initialized_3) {
int __gen_e_acsl_valid_3;
- __gen_e_acsl_valid_3 = __e_acsl_valid((void *)r,sizeof(int));
+ __gen_e_acsl_valid_3 = __e_acsl_valid((void *)r,sizeof(int),
+ (void *)r,(void *)(& r));
__gen_e_acsl_and_3 = __gen_e_acsl_valid_3;
}
else __gen_e_acsl_and_3 = 0;
@@ -451,7 +468,8 @@ int while_valid(void)
int __gen_e_acsl_valid_4;
/*@ assert Value: initialisation: \initialized(&p); */
/*@ assert Value: dangling_pointer: ¬\dangling(&p); */
- __gen_e_acsl_valid_4 = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_valid_4 = __e_acsl_valid((void *)p,sizeof(int),
+ (void *)p,(void *)(& p));
__gen_e_acsl_and_4 = __gen_e_acsl_valid_4;
}
else __gen_e_acsl_and_4 = 0;
@@ -468,7 +486,8 @@ int while_valid(void)
int __gen_e_acsl_valid_5;
/*@ assert Value: initialisation: \initialized(&q); */
/*@ assert Value: dangling_pointer: ¬\dangling(&q); */
- __gen_e_acsl_valid_5 = __e_acsl_valid((void *)q,sizeof(int));
+ __gen_e_acsl_valid_5 = __e_acsl_valid((void *)q,sizeof(int),
+ (void *)q,(void *)(& q));
__gen_e_acsl_and_5 = __gen_e_acsl_valid_5;
}
else __gen_e_acsl_and_5 = 0;
@@ -483,7 +502,8 @@ int while_valid(void)
sizeof(int *));
if (__gen_e_acsl_initialized_6) {
int __gen_e_acsl_valid_6;
- __gen_e_acsl_valid_6 = __e_acsl_valid((void *)r,sizeof(int));
+ __gen_e_acsl_valid_6 = __e_acsl_valid((void *)r,sizeof(int),
+ (void *)r,(void *)(& r));
__gen_e_acsl_and_6 = __gen_e_acsl_valid_6;
}
else __gen_e_acsl_and_6 = 0;
@@ -523,7 +543,8 @@ void continue_valid(void)
sizeof(int *));
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),
+ (void *)p,(void *)(& p));
__gen_e_acsl_and = __gen_e_acsl_valid;
}
else __gen_e_acsl_and = 0;
@@ -538,7 +559,8 @@ void continue_valid(void)
sizeof(int *));
if (__gen_e_acsl_initialized_2) {
int __gen_e_acsl_valid_2;
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)q,sizeof(int));
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)q,sizeof(int),
+ (void *)q,(void *)(& q));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
}
else __gen_e_acsl_and_2 = 0;
@@ -558,7 +580,8 @@ void continue_valid(void)
sizeof(int *));
if (__gen_e_acsl_initialized_3) {
int __gen_e_acsl_valid_3;
- __gen_e_acsl_valid_3 = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_valid_3 = __e_acsl_valid((void *)p,sizeof(int),
+ (void *)p,(void *)(& p));
__gen_e_acsl_and_3 = __gen_e_acsl_valid_3;
}
else __gen_e_acsl_and_3 = 0;
@@ -573,7 +596,8 @@ void continue_valid(void)
sizeof(int *));
if (__gen_e_acsl_initialized_4) {
int __gen_e_acsl_valid_4;
- __gen_e_acsl_valid_4 = __e_acsl_valid((void *)q,sizeof(int));
+ __gen_e_acsl_valid_4 = __e_acsl_valid((void *)q,sizeof(int),
+ (void *)q,(void *)(& q));
__gen_e_acsl_and_4 = __gen_e_acsl_valid_4;
}
else __gen_e_acsl_and_4 = 0;
@@ -594,7 +618,8 @@ void continue_valid(void)
sizeof(int *));
if (__gen_e_acsl_initialized_5) {
int __gen_e_acsl_valid_5;
- __gen_e_acsl_valid_5 = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_valid_5 = __e_acsl_valid((void *)p,sizeof(int),
+ (void *)p,(void *)(& p));
__gen_e_acsl_and_5 = __gen_e_acsl_valid_5;
}
else __gen_e_acsl_and_5 = 0;
@@ -609,7 +634,8 @@ void continue_valid(void)
sizeof(int *));
if (__gen_e_acsl_initialized_6) {
int __gen_e_acsl_valid_6;
- __gen_e_acsl_valid_6 = __e_acsl_valid((void *)q,sizeof(int));
+ __gen_e_acsl_valid_6 = __e_acsl_valid((void *)q,sizeof(int),
+ (void *)q,(void *)(& q));
__gen_e_acsl_and_6 = __gen_e_acsl_valid_6;
}
else __gen_e_acsl_and_6 = 0;
@@ -636,7 +662,8 @@ void continue_valid(void)
sizeof(int *));
if (__gen_e_acsl_initialized_7) {
int __gen_e_acsl_valid_7;
- __gen_e_acsl_valid_7 = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_valid_7 = __e_acsl_valid((void *)p,sizeof(int),(void *)p,
+ (void *)(& p));
__gen_e_acsl_and_7 = __gen_e_acsl_valid_7;
}
else __gen_e_acsl_and_7 = 0;
@@ -651,7 +678,8 @@ void continue_valid(void)
sizeof(int *));
if (__gen_e_acsl_initialized_8) {
int __gen_e_acsl_valid_8;
- __gen_e_acsl_valid_8 = __e_acsl_valid((void *)q,sizeof(int));
+ __gen_e_acsl_valid_8 = __e_acsl_valid((void *)q,sizeof(int),(void *)q,
+ (void *)(& q));
__gen_e_acsl_and_8 = __gen_e_acsl_valid_8;
}
else __gen_e_acsl_and_8 = 0;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_errno.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_errno.c
index 9e580cdb8c410429dc4d9da2b4fb5c6a0cbdbbe2..789e410437316560413926af468f98ff0ab50dd9 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_errno.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_errno.c
@@ -25,7 +25,8 @@ int main(int argc, char const **argv)
sizeof(int *));
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),(void *)p,
+ (void *)(& p));
__gen_e_acsl_and = __gen_e_acsl_valid;
}
else __gen_e_acsl_and = 0;
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 0938ccde373718177bd3a8d9d140358c94a5b134..54dc8baee650a7c57447027315d087b70c139350 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
@@ -16,7 +16,8 @@ void f(void)
{
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(T + G),
- sizeof(char));
+ sizeof(char),(void *)T,
+ (void *)(& T));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"f",
(char *)"mem_access: \\valid_read(T + G)",11);
__e_acsl_assert(*(T + G) == 'b',(char *)"Assertion",(char *)"f",
@@ -39,28 +40,28 @@ void __e_acsl_globals_init(void)
__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);
+ __e_acsl_mark_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);
+ __e_acsl_mark_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);
- __e_acsl_readonly((void *)__gen_e_acsl_literal_string);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
__gen_e_acsl_literal_string_4 = "foo2";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_4,sizeof("foo2"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_4);
- __e_acsl_readonly((void *)__gen_e_acsl_literal_string_4);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_4);
__gen_e_acsl_literal_string_3 = "foo";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_3,sizeof("foo"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_3);
- __e_acsl_readonly((void *)__gen_e_acsl_literal_string_3);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_3);
__gen_e_acsl_literal_string_2 = "bar";
__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_mark_readonly((void *)__gen_e_acsl_literal_string_2);
__e_acsl_store_block((void *)(& l_str),(size_t)8);
__e_acsl_full_init((void *)(& l_str));
__e_acsl_store_block((void *)(& s_str),(size_t)8);
@@ -86,7 +87,8 @@ int main(void)
{
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(S + G2),
- sizeof(char));
+ sizeof(char),(void *)S,
+ (void *)(& S));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(S + G2)",25);
__e_acsl_assert(*(S + G2) == 'o',(char *)"Assertion",(char *)"main",
@@ -102,7 +104,9 @@ int main(void)
/*@ 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));
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)S2,sizeof(char),
+ (void *)S2,
+ (void *)(& S2));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"Assertion",
(char *)"main",(char *)"\\valid_read(S2)",27);
}
@@ -114,7 +118,8 @@ int main(void)
sizeof(char *));
if (__gen_e_acsl_initialized_2) {
int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)SS,sizeof(char));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)SS,sizeof(char),(void *)SS,
+ (void *)(& SS));
__gen_e_acsl_and = __gen_e_acsl_valid;
}
else __gen_e_acsl_and = 0;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_local_goto.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_local_goto.c
index f5a71822eb517779399c79fb801f5cc3f2f2211e..9e517c9ce5af02cd174e8b4a87c129e9c4b01516 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_local_goto.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_local_goto.c
@@ -11,19 +11,19 @@ void __e_acsl_globals_init(void)
__e_acsl_store_block((void *)__gen_e_acsl_literal_string,
sizeof("t is %d, going to %s\n"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string);
- __e_acsl_readonly((void *)__gen_e_acsl_literal_string);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
__gen_e_acsl_literal_string_3 = "UP";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_3,sizeof("UP"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_3);
- __e_acsl_readonly((void *)__gen_e_acsl_literal_string_3);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_3);
__gen_e_acsl_literal_string_2 = "RET";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,sizeof("RET"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
- __e_acsl_readonly((void *)__gen_e_acsl_literal_string_2);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_2);
__gen_e_acsl_literal_string_4 = "AGAIN";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_4,sizeof("AGAIN"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_4);
- __e_acsl_readonly((void *)__gen_e_acsl_literal_string_4);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_4);
return;
}
@@ -48,7 +48,8 @@ int main(int argc, char const **argv)
/*@ assert \valid(&a); */
{
int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)(& a),sizeof(int));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)(& a),sizeof(int),
+ (void *)(& a),(void *)(& a));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",
(char *)"main",(char *)"\\valid(&a)",25);
}
@@ -65,7 +66,8 @@ int main(int argc, char const **argv)
/*@ assert \valid(&b); */
{
int __gen_e_acsl_valid_2;
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& b),sizeof(int));
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& b),sizeof(int),
+ (void *)(& b),(void *)(& b));
__e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Assertion",
(char *)"main",(char *)"\\valid(&b)",36);
}
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
index 44028547cfb0109025238e8e249f6313f306f36a..f0a7e6b8479128adb4c0d2fe5d0290b0cf167f69 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
@@ -11,14 +11,16 @@ int main(int argc, char **argv)
int __gen_e_acsl_valid;
__e_acsl_store_block((void *)(& argv),(size_t)8);
__e_acsl_store_block((void *)(& argc),(size_t)4);
- __gen_e_acsl_valid = __e_acsl_valid((void *)(& argc),sizeof(int));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)(& argc),sizeof(int),
+ (void *)(& argc),(void *)(& argc));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"main",
(char *)"\\valid(&argc)",10);
}
/*@ assert \valid(&argv); */
{
int __gen_e_acsl_valid_2;
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& argv),sizeof(char **));
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& argv),sizeof(char **),
+ (void *)(& argv),(void *)(& argv));
__e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Assertion",(char *)"main",
(char *)"\\valid(&argv)",11);
}
@@ -33,7 +35,8 @@ int main(int argc, char **argv)
{
int __gen_e_acsl_valid_3;
__gen_e_acsl_valid_3 = __e_acsl_valid((void *)(argv + __gen_e_acsl_k),
- sizeof(char *));
+ sizeof(char *),(void *)argv,
+ (void *)(& argv));
if (__gen_e_acsl_valid_3) ;
else {
__gen_e_acsl_forall = 0;
@@ -68,7 +71,9 @@ int main(int argc, char **argv)
{
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(argv + argc),
- sizeof(char *));
+ sizeof(char *),
+ (void *)argv,
+ (void *)(& argv));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(argv + argc)",15);
/*@ assert Value: mem_access: \valid_read(argv + argc); */
@@ -85,12 +90,16 @@ int main(int argc, char **argv)
int __gen_e_acsl_valid_read_2;
int __gen_e_acsl_valid_4;
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(argv + argc),
- sizeof(char *));
+ sizeof(char *),
+ (void *)argv,
+ (void *)(& argv));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(argv + argc)",16);
/*@ assert Value: mem_access: \valid_read(argv + argc); */
__gen_e_acsl_valid_4 = __e_acsl_valid((void *)*(argv + argc),
- sizeof(char));
+ sizeof(char),
+ (void *)*(argv + argc),
+ (void *)(argv + argc));
__gen_e_acsl_and = __gen_e_acsl_valid_4;
}
else __gen_e_acsl_and = 0;
@@ -113,12 +122,16 @@ int main(int argc, char **argv)
int __gen_e_acsl_valid_read_3;
int __gen_e_acsl_valid_5;
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(argv + i),
- sizeof(char *));
+ sizeof(char *),
+ (void *)argv,
+ (void *)(& argv));
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",
(char *)"main",
(char *)"mem_access: \\valid_read(argv + i)",19);
__gen_e_acsl_valid_5 = __e_acsl_valid((void *)*(argv + i),
- sizeof(char));
+ sizeof(char),
+ (void *)*(argv + i),
+ (void *)(argv + i));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_5;
}
else __gen_e_acsl_and_2 = 0;
@@ -138,12 +151,16 @@ int main(int argc, char **argv)
int __gen_e_acsl_valid_6;
__gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(
argv + i),
- sizeof(char *));
+ sizeof(char *),
+ (void *)argv,
+ (void *)(& argv));
__e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",
(char *)"main",
(char *)"mem_access: \\valid_read(argv + i)",20);
__gen_e_acsl_valid_6 = __e_acsl_valid((void *)(*(argv + i) + __gen_e_acsl_k_2),
- sizeof(char));
+ sizeof(char),
+ (void *)*(argv + i),
+ (void *)(argv + i));
if (__gen_e_acsl_valid_6) ;
else {
__gen_e_acsl_forall_2 = 0;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c
index ed712a0a82450f97fbb6f5f00547118629087ca2..807689112cbd77112c5a1bc3d175ec53a772a656 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c
@@ -24,7 +24,8 @@ int main(int argc, char const **argv)
sizeof(char *));
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(char));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(char),(void *)p,
+ (void *)(& p));
__gen_e_acsl_and = __gen_e_acsl_valid;
}
else __gen_e_acsl_and = 0;
@@ -54,7 +55,8 @@ int main(int argc, char const **argv)
sizeof(char *));
if (__gen_e_acsl_initialized_2) {
int __gen_e_acsl_valid_2;
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)p,sizeof(char));
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)p,sizeof(char),(void *)p,
+ (void *)(& p));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
}
else __gen_e_acsl_and_2 = 0;
@@ -89,7 +91,8 @@ int main(int argc, char const **argv)
sizeof(char *));
if (__gen_e_acsl_initialized_3) {
int __gen_e_acsl_valid_3;
- __gen_e_acsl_valid_3 = __e_acsl_valid((void *)a,sizeof(char));
+ __gen_e_acsl_valid_3 = __e_acsl_valid((void *)a,sizeof(char),(void *)a,
+ (void *)(& a));
__gen_e_acsl_and_3 = __gen_e_acsl_valid_3;
}
else __gen_e_acsl_and_3 = 0;
@@ -119,7 +122,8 @@ int main(int argc, char const **argv)
sizeof(char *));
if (__gen_e_acsl_initialized_4) {
int __gen_e_acsl_valid_4;
- __gen_e_acsl_valid_4 = __e_acsl_valid((void *)a,sizeof(char));
+ __gen_e_acsl_valid_4 = __e_acsl_valid((void *)a,sizeof(char),(void *)a,
+ (void *)(& a));
__gen_e_acsl_and_4 = __gen_e_acsl_valid_4;
}
else __gen_e_acsl_and_4 = 0;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c
index 4e4c6777f405f23aa6f6af335f5b4c4ed0eee2e6..ecf41c7d55ec8f48443d951445a2cc4d0f5e1320 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c
@@ -21,7 +21,8 @@ int main(void)
sizeof(int *));
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid_read;
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)p,sizeof(int));
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)p,sizeof(int),
+ (void *)p,(void *)(& p));
__gen_e_acsl_and = __gen_e_acsl_valid_read;
}
else __gen_e_acsl_and = 0;
@@ -64,7 +65,9 @@ int main(void)
{
int __gen_e_acsl_valid_read_2;
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(& t[2] - i),
- sizeof(int));
+ sizeof(int),
+ (void *)(& t[2]),
+ (void *)(& t[2]));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",
(char *)"main",
(char *)"mem_access: \\valid_read(&t[2] - i)",19);
@@ -86,7 +89,9 @@ int main(void)
sizeof(int *));
if (__gen_e_acsl_initialized_2) {
int __gen_e_acsl_valid_read_3;
- __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)p,sizeof(int));
+ __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)p,sizeof(int),
+ (void *)p,
+ (void *)(& p));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_read_3;
}
else __gen_e_acsl_and_2 = 0;
@@ -100,7 +105,8 @@ int main(void)
{
int __gen_e_acsl_valid_read_4;
__gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(p + k),
- sizeof(int));
+ sizeof(int),(void *)p,
+ (void *)(& p));
__e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(p + k)",27);
__e_acsl_assert(*(p + k) == 3,(char *)"Assertion",(char *)"main",
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_stdout.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_stdout.c
index 98061b7b8c8272473ae5b24b21a41d38f7ce49bd..3d8afb1549cc2095e8526464479c915d7cb7febd 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_stdout.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_stdout.c
@@ -20,21 +20,24 @@ int main(void)
/*@ assert \valid(__fc_stderr); */
{
int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)stderr,sizeof(FILE));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)stderr,sizeof(FILE),
+ (void *)stderr,(void *)(& stderr));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"main",
(char *)"\\valid(__fc_stderr)",8);
}
/*@ assert \valid(__fc_stdin); */
{
int __gen_e_acsl_valid_2;
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)stdin,sizeof(FILE));
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)stdin,sizeof(FILE),
+ (void *)stdin,(void *)(& stdin));
__e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Assertion",(char *)"main",
(char *)"\\valid(__fc_stdin)",9);
}
/*@ assert \valid(__fc_stdout); */
{
int __gen_e_acsl_valid_3;
- __gen_e_acsl_valid_3 = __e_acsl_valid((void *)stdout,sizeof(FILE));
+ __gen_e_acsl_valid_3 = __e_acsl_valid((void *)stdout,sizeof(FILE),
+ (void *)stdout,(void *)(& stdout));
__e_acsl_assert(__gen_e_acsl_valid_3,(char *)"Assertion",(char *)"main",
(char *)"\\valid(__fc_stdout)",10);
}
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index d56b16f3667f0037ce4911fe0e6e254dd6fb1cf4..1406bd12d44cac9d147f89a172df1856963cb980 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -35,7 +35,7 @@ let handle_error f env =
Env.Context.restore env
(* internal to [named_predicate_to_exp] but put it outside in order to not add
- extra tedious parameter.
+ extra tedious parameter.
It is [true] iff we are currently visiting \valid. *)
let is_visiting_valid = ref false
@@ -163,8 +163,8 @@ let constant_to_exp ~loc t = function
| LStr s -> Cil.new_exp ~loc (Const (CStr s)), false
| LWStr s -> Cil.new_exp ~loc (Const (CWStr s)), false
| LChr c -> Cil.new_exp ~loc (Const (CChr c)), false
- | LReal {r_literal=s; r_nearest=f; r_lower=l; r_upper=u} ->
- if l <> u then
+ | LReal {r_literal=s; r_nearest=f; r_lower=l; r_upper=u} ->
+ if l <> u then
Options.warning ~current:true ~once:true
"approximating a real number by a float";
Cil.new_exp ~loc (Const (CReal (f, FLongDouble, Some s))), false
@@ -225,11 +225,11 @@ let cast_integer_to_float lty lty_t e =
e
let rec thost_to_host kf env = function
- | TVar { lv_origin = Some v } ->
+ | TVar { lv_origin = Some v } ->
Var (Cil.get_varinfo (Env.get_behavior env) v), env, v.vname
- | TVar ({ lv_origin = None } as logic_v) ->
+ | TVar ({ lv_origin = None } as logic_v) ->
Var (Env.Logic_binding.get env logic_v), env, logic_v.lv_name
- | TResult _typ ->
+ | TResult _typ ->
let vis = Env.get_visitor env in
let kf = Extlib.the vis#current_kf in
let lhost = Misc.result_lhost kf in
@@ -242,16 +242,16 @@ let rec thost_to_host kf env = function
and toffset_to_offset ?loc kf env = function
| TNoOffset -> NoOffset, env
- | TField(f, offset) ->
+ | TField(f, offset) ->
let offset, env = toffset_to_offset ?loc kf env offset in
Field(f, offset), env
- | TIndex(t, offset) ->
+ | TIndex(t, offset) ->
let e, env = term_to_exp kf env t in
let offset, env = toffset_to_offset kf env offset in
Index(e, offset), env
| TModel _ -> not_yet env "model"
-and tlval_to_lval kf env (host, offset) =
+and tlval_to_lval kf env (host, offset) =
let host, env, name = thost_to_host kf env host in
let offset, env = toffset_to_offset kf env offset in
let name = match offset with NoOffset -> name | Field _ | Index _ -> "" in
@@ -260,13 +260,13 @@ and tlval_to_lval kf env (host, offset) =
(* the returned boolean says that the expression is an mpz_string;
the returned string is the name of the generated variable corresponding to
the term. *)
-and context_insensitive_term_to_exp kf env t =
+and context_insensitive_term_to_exp kf env t =
let loc = t.term_loc in
match t.term_node with
| TConst c ->
let c, is_mpz_string = constant_to_exp ~loc t c in
c, env, is_mpz_string, ""
- | TLval lv ->
+ | TLval lv ->
let lv, env, name = tlval_to_lval kf env lv in
Cil.new_exp ~loc (Lval lv), env, false, name
| TSizeOf ty -> Cil.sizeOf ~loc ty, env, false, "sizeof"
@@ -287,7 +287,7 @@ and context_insensitive_term_to_exp kf env t =
| BNot -> "__gmpz_com", "bnot"
| LNot -> assert false
in
- let _, e, env =
+ let _, e, env =
Env.new_var_and_mpz_init
~loc
env
@@ -322,8 +322,8 @@ and context_insensitive_term_to_exp kf env t =
let name = name_of_mpz_arith_bop bop in
let mk_stmts _ e = [ Misc.mk_call ~loc name [ e; e1; e2 ] ] in
let name = name_of_binop bop in
- let _, e, env =
- Env.new_var_and_mpz_init ~loc ~name env (Some t) mk_stmts
+ let _, e, env =
+ Env.new_var_and_mpz_init ~loc ~name env (Some t) mk_stmts
in
e, env, false, ""
else
@@ -354,16 +354,16 @@ and context_insensitive_term_to_exp kf env t =
let name = name_of_binop bop ^ "_guard" in
comparison_to_exp ~loc kf env Typing.gmp ~e1:e2 ~name Eq t2 zero t
in
- let mk_stmts _v e =
+ let mk_stmts _v e =
assert (Gmpz.is_t ty);
let vis = Env.get_visitor env in
let kf = Extlib.the vis#current_kf in
- let cond =
- Misc.mk_e_acsl_guard
- (Env.annotation_kind env)
+ let cond =
+ Misc.mk_e_acsl_guard
+ (Env.annotation_kind env)
kf
guard
- (Logic_const.prel ~loc (Req, t2, zero))
+ (Logic_const.prel ~loc (Req, t2, zero))
in
Env.add_assert env cond (Logic_const.prel (Rneq, t2, zero));
let instr = Misc.mk_call ~loc name [ e; e1; e2 ] in
@@ -424,10 +424,10 @@ and context_insensitive_term_to_exp kf env t =
let e, env = add_cast ~loc ~name:"cast" env (Some ty) false (Some t) e in
e, env, false, ""
| TLogic_coerce _ -> assert false (* handle in [term_to_exp] *)
- | TAddrOf lv ->
+ | TAddrOf lv ->
let lv, env, _ = tlval_to_lval kf env lv in
Cil.mkAddrOf ~loc lv, env, false, "addrof"
- | TStartOf lv ->
+ | TStartOf lv ->
let lv, env, _ = tlval_to_lval kf env lv in
Cil.mkAddrOrStartOf ~loc lv, env, false, "startof"
| Tapp(li, [], args) when Builtins.mem li.l_var_info.lv_name ->
@@ -468,7 +468,7 @@ and context_insensitive_term_to_exp kf env t =
let res3 = term_to_exp kf (Env.push env2) t3 in
let e, env = conditional_to_exp loc (Some t) e1 res2 res3 in
e, env, false, ""
- | Tat(t, LogicLabel(_, label)) when label = "Here" ->
+ | Tat(t, LogicLabel(_, label)) when label = "Here" ->
let e, env = term_to_exp kf env t in
e, env, false, ""
| Tat(t', label) ->
@@ -503,7 +503,7 @@ and context_insensitive_term_to_exp kf env t =
constructs. *)
and term_to_exp kf env t =
let generate_rte = Env.generate_rte env in
- Options.feedback ~dkey ~level:4 "translating term %a (rte? %b)"
+ Options.feedback ~dkey ~level:4 "translating term %a (rte? %b)"
Printer.pp_term t generate_rte;
let env = Env.rte env false in
let t = match t.term_node with TLogic_coerce(_, t) -> t | _ -> t in
@@ -550,18 +550,27 @@ and comparison_to_exp
(* \base_addr, \block_length and \freeable annotations *)
and mmodel_call ~loc kf name ctx env t =
let e, env = term_to_exp kf (Env.rte env true) t in
- let _, res, env =
+ let _, res, env =
Env.new_var
~loc
~name
env
None
- ctx
- (fun v _ ->
+ ctx
+ (fun v _ ->
[ Misc.mk_call ~loc ~result:(Cil.var v) (Misc.mk_api_name name) [ e ] ])
in
res, env, false, name
+and get_c_term_type = function
+ | Ctype ty -> ty
+ | _ -> assert false
+
+and mk_ptr_sizeof typ loc =
+ match Cil.unrollType typ with
+ | TPtr (t', _) -> Cil.new_exp ~loc (SizeOf t')
+ | _ -> assert false
+
(* \valid, \offset and \initialized annotations *)
and mmodel_call_with_size ~loc kf name ctx env t =
let e, env = term_to_exp kf (Env.rte env true) t in
@@ -573,50 +582,68 @@ and mmodel_call_with_size ~loc kf name ctx env t =
None
ctx
(fun v _ ->
- let ty = match t.term_type with
- | Ctype ty -> ty
- | _ -> assert false
- in
- let sizeof = match Cil.unrollType ty with
- | TPtr (t', _) -> Cil.new_exp ~loc (SizeOf t')
- | _ -> assert false
- in
- [ Misc.mk_call
- ~loc ~result:(Cil.var v) (Misc.mk_api_name name) [ e; sizeof ] ])
+ let ty = get_c_term_type t.term_type in
+ let sizeof = mk_ptr_sizeof ty loc in
+ let fname = Misc.mk_api_name name in
+ [ Misc.mk_call ~loc ~result:(Cil.var v) fname [ e; sizeof ] ])
+ in
+ res, env
+
+and mmodel_call_valid ~loc kf name ctx env t =
+ let e, env = term_to_exp kf (Env.rte env true) t in
+ let base, _ = Misc.ptr_index ~loc e in
+ let base_addr = match base.enode with
+ | AddrOf _ | Const _ -> base
+ | Lval(lv) | StartOf(lv) -> Cil.mkAddrOrStartOf ~loc lv
+ | _ -> assert false
+ in
+ let _, res, env =
+ Env.new_var
+ ~loc
+ ~name
+ env
+ None
+ ctx
+ (fun v _ ->
+ let ty = get_c_term_type t.term_type in
+ let sizeof = mk_ptr_sizeof ty loc in
+ let fname = Misc.mk_api_name name in
+ let args = [ e; sizeof; base; base_addr ] in
+ [ Misc.mk_call ~loc ~result:(Cil.var v) fname args ])
in
res, env
and at_to_exp env t_opt label e =
let stmt = E_acsl_label.get_stmt (Env.get_visitor env) label in
(* generate a new variable denoting [\at(t',label)].
- That is this variable which is the resulting expression.
+ 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 loc = Stmt.loc stmt in
let res_v, res, new_env =
Env.new_var
~loc
- ~name:"at"
+ ~name:"at"
~scope:Env.Function
env
t_opt
- (Cil.typeOf e)
+ (Cil.typeOf e)
(fun _ _ -> [])
in
let env_ref = ref new_env in
(* visitor modifying in place the labeled statement in order to store [e]
in the resulting variable at this location (which is the only correct
one). *)
- let o = object
+ let o = object
inherit Visitor.frama_c_inplace
- method !vstmt_aux stmt =
+ method !vstmt_aux stmt =
(* either a standard C affectation or an mpz one according to type of
- [e] *)
+ [e] *)
let new_stmt = Gmpz.init_set ~loc (Cil.var res_v) res e in
assert (!env_ref == new_env);
(* generate the new block of code for the labeled statement and the
corresponding environment *)
- let block, new_env =
+ let block, new_env =
Env.pop_and_get new_env new_stmt ~global_clear:false Env.Middle
in
let pre = match label with
@@ -654,7 +681,7 @@ and named_predicate_content_to_exp ?name kf env p =
let env3 = Env.push env2 in
let name = match name with None -> "and" | Some n -> n in
conditional_to_exp ~name loc None e1 res2 (Cil.zero loc, env3)
- | Por(p1, p2) ->
+ | Por(p1, p2) ->
(* p1 || p2 <==> if p1 then true else p2 *)
let e1, env1 = named_predicate_to_exp kf (Env.rte env true) p1 in
let env' = Env.push env1 in
@@ -662,21 +689,21 @@ and named_predicate_content_to_exp ?name kf env p =
let name = match name with None -> "or" | Some n -> n in
conditional_to_exp ~name loc None e1 (Cil.one loc, env') res2
| Pxor _ -> not_yet env "xor"
- | Pimplies(p1, p2) ->
+ | Pimplies(p1, p2) ->
(* (p1 ==> p2) <==> !p1 || p2 *)
- named_predicate_to_exp
+ named_predicate_to_exp
~name:"implies"
kf
env
(Logic_const.por ~loc ((Logic_const.pnot ~loc p1), p2))
- | Piff(p1, p2) ->
+ | Piff(p1, p2) ->
(* (p1 <==> p2) <==> (p1 ==> p2 && p2 ==> p1) *)
- named_predicate_to_exp
+ named_predicate_to_exp
~name:"equiv"
kf
env
(Logic_const.pand ~loc
- (Logic_const.pimplies ~loc (p1, p2),
+ (Logic_const.pimplies ~loc (p1, p2),
Logic_const.pimplies ~loc (p2, p1)))
| Pnot p ->
let e, env = named_predicate_to_exp kf env p in
@@ -688,9 +715,9 @@ and named_predicate_content_to_exp ?name kf env p =
conditional_to_exp loc None e1 res2 res3
| Plet _ -> not_yet env "let _ = _ in _"
| Pforall _ | Pexists _ -> Quantif.quantif_to_exp kf env p
- | Pat(p, LogicLabel(_, label)) when label = "Here" ->
+ | Pat(p, LogicLabel(_, label)) when label = "Here" ->
named_predicate_to_exp kf env p
- | Pat(p', label) ->
+ | Pat(p', label) ->
(* convert [t'] to [e] in a separated local env *)
let e, env = named_predicate_to_exp kf (Env.push env) p' in
let e, env, is_string = at_to_exp env None label e in
@@ -698,13 +725,13 @@ and named_predicate_content_to_exp ?name kf env p =
e, env
| Pvalid_read(LogicLabel(_, label) as llabel, t) as pc
| (Pvalid(LogicLabel(_, label) as llabel, t) as pc) when label = "Here" ->
- let call_valid t =
+ let call_valid t =
let name = match pc with
| Pvalid _ -> "valid"
| Pvalid_read _ -> "valid_read"
| _ -> assert false
in
- mmodel_call_with_size ~loc kf name Cil.intType env t
+ mmodel_call_valid ~loc kf name Cil.intType env t
in
if !is_visiting_valid then begin
(* we already transformed \valid(t) into \initialized(&t) && \valid(t):
@@ -729,7 +756,7 @@ and named_predicate_content_to_exp ?name kf env p =
(match t.term_node with
(* optimisation when we know that the initialisation is ok *)
| TAddrOf (TResult _, TNoOffset) -> Cil.one ~loc, env
- | TAddrOf (TVar { lv_origin = Some vi }, TNoOffset)
+ | TAddrOf (TVar { lv_origin = Some vi }, TNoOffset)
when vi.vformal || vi.vglob || Misc.is_generated_varinfo vi ->
Cil.one ~loc, env
| _ -> mmodel_call_with_size ~loc kf "initialized" Cil.intType env t)
@@ -757,7 +784,7 @@ and named_predicate_to_exp ?name kf ?rte env p =
None
e
-and translate_rte_annots:
+and translate_rte_annots:
'a. (Format.formatter -> 'a -> unit) -> 'a ->
kernel_function -> Env.t -> code_annotation list -> Env.t =
fun pp elt kf env l ->
@@ -767,9 +794,9 @@ and translate_rte_annots:
let env =
List.fold_left
(fun env a -> match a.annot_content with
- | AAssert(_, p) ->
+ | AAssert(_, p) ->
handle_error
- (fun env ->
+ (fun env ->
Options.feedback ~dkey ~level:4 "prevent RTE from %a" pp elt;
translate_named_predicate kf (Env.rte env false) p)
env
@@ -786,20 +813,20 @@ and translate_rte kf env e =
translate_rte_annots Printer.pp_exp e kf env l
and translate_named_predicate kf env p =
- Options.feedback ~dkey ~level:3 "translating predicate %a"
+ Options.feedback ~dkey ~level:3 "translating predicate %a"
Printer.pp_predicate p;
let rte = Env.generate_rte env in
Typing.type_named_predicate ~must_clear:rte p;
let e, env = named_predicate_to_exp kf ~rte env p in
assert (Typ.equal (Cil.typeOf e) Cil.intType);
Env.add_stmt
- env
+ env
(Misc.mk_e_acsl_guard ~reverse:true (Env.annotation_kind env) kf e p)
-let named_predicate_to_exp ?name kf env p =
+let named_predicate_to_exp ?name kf env p =
named_predicate_to_exp ?name kf env p (* forget optional argument ?rte *)
-let () =
+let () =
Quantif.term_to_exp_ref := term_to_exp;
Quantif.predicate_to_exp_ref := named_predicate_to_exp
@@ -853,11 +880,11 @@ let assumes_predicate bhv =
let original_project_ref = ref Project_skeleton.dummy
let set_original_project p = original_project_ref := p
-let must_translate ppt =
+let must_translate ppt =
let selection =
State_selection.of_list [ Property_status.self; Options.Valid.self ]
in
- Project.on ~selection
+ Project.on ~selection
!original_project_ref
(fun ppt ->
match Property_status.get ppt with
@@ -867,14 +894,14 @@ let must_translate ppt =
let translate_preconditions kf kinstr env behaviors =
let env = Env.set_annotation_kind env Misc.Precondition in
- let do_behavior env b =
+ let do_behavior env b =
let assumes_pred = assumes_predicate b in
List.fold_left
(fun env p ->
let do_it env =
if must_translate (Property.ip_of_requires kf kinstr b p) then
let loc = p.ip_content.pred_loc in
- let p =
+ let p =
Logic_const.pimplies
~loc
(assumes_pred,
@@ -887,13 +914,13 @@ let translate_preconditions kf kinstr env behaviors =
handle_error do_it env)
env
b.b_requires
- in
+ in
List.fold_left do_behavior env behaviors
let translate_postconditions kf kinstr env behaviors =
let env = Env.set_annotation_kind env Misc.Postcondition in
(* generate one guard by postcondition of each behavior *)
- let do_behavior env b =
+ let do_behavior env b =
let assumes_pred = assumes_predicate b in
List.fold_left
(fun env (t, p as post) ->
@@ -901,23 +928,23 @@ let translate_postconditions kf kinstr env behaviors =
let env =
handle_error
(fun env ->
- if b.b_assigns <> WritesAny then
+ if b.b_assigns <> WritesAny then
not_yet env "assigns clause in behavior";
- if b.b_extended <> [] then
+ if b.b_extended <> [] then
not_yet env "grammar extensions in behavior";
env)
env
in
let do_it env =
match t with
- | Normal ->
+ | Normal ->
let loc = p.ip_content.pred_loc in
let p = p.ip_content in
- let p =
- Logic_const.pimplies
+ let p =
+ Logic_const.pimplies
~loc
- (Logic_const.pold ~loc assumes_pred,
- Logic_const.unamed ~loc p.pred_content)
+ (Logic_const.pold ~loc assumes_pred,
+ Logic_const.unamed ~loc p.pred_content)
in
translate_named_predicate kf env p
| Exits | Breaks | Continues | Returns ->
@@ -927,7 +954,7 @@ let translate_postconditions kf kinstr env behaviors =
else env)
env
b.b_post_cond
- in
+ in
List.fold_left do_behavior env behaviors
let translate_pre_spec kf kinstr env spec =
@@ -967,32 +994,32 @@ let translate_pre_spec kf kinstr env spec =
in
let env = convert_unsupported_clauses env in
handle_error
- (fun env -> translate_preconditions kf kinstr env spec.spec_behavior)
+ (fun env -> translate_preconditions kf kinstr env spec.spec_behavior)
env
-let translate_post_spec kf kinstr env spec =
+let translate_post_spec kf kinstr env spec =
handle_error
- (fun env -> translate_postconditions kf kinstr env spec.spec_behavior)
+ (fun env -> translate_postconditions kf kinstr env spec.spec_behavior)
env
let translate_pre_code_annotation kf stmt env annot =
let convert env = match annot.annot_content with
- | AAssert(l, p) ->
+ | AAssert(l, p) ->
if must_translate (Property.ip_of_code_annot_single kf stmt annot) then
let env = Env.set_annotation_kind env Misc.Assertion in
- if l <> [] then
+ if l <> [] then
not_yet env "@[assertion applied only on some behaviors@]";
translate_named_predicate kf env p
else
env
| AStmtSpec(l, spec) ->
- if l <> [] then
+ if l <> [] then
not_yet env "@[statement contract applied only on some behaviors@]";
translate_pre_spec kf (Kstmt stmt) env spec ;
| AInvariant(l, loop_invariant, p) ->
if must_translate (Property.ip_of_code_annot_single kf stmt annot) then
let env = Env.set_annotation_kind env Misc.Invariant in
- if l <> [] then
+ if l <> [] then
not_yet env "@[invariant applied only on some behaviors@]";
let env = translate_named_predicate kf env p in
if loop_invariant then Env.add_loop_invariant env p else env
@@ -1018,8 +1045,8 @@ let translate_pre_code_annotation kf stmt env annot =
let translate_post_code_annotation kf stmt env annot =
let convert env = match annot.annot_content with
| AStmtSpec(_, spec) -> translate_post_spec kf (Kstmt stmt) env spec
- | AAssert _
- | AInvariant _
+ | AAssert _
+ | AInvariant _
| AVariant _
| AAssigns _
| AAllocation _
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 314aa0702468475744cb6a23d7cb1a581d902394..a159cdea254416f7429a1357bf7b2fcfd9261655 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -114,8 +114,8 @@ class e_acsl_visitor prj generate = object (self)
val global_vars: init option Varinfo.Hashtbl.t = Varinfo.Hashtbl.create 7
(* Hashtable mapping global variables (as Cil_type.varinfo) to their
initializers aiming to capture memory allocated by global variable
- declarations and initilisation. At runtime the memory blocks corresponding
- to space occupied by global are recorded via a call to
+ declarations and initialization. At runtime the memory blocks
+ corresponding to space occupied by global are recorded via a call to
[__gen_e_acsl_globals_init] instrumented at the beginning of the
[main] function. Each variable stored by [global_vars] will be handled in
the body of [__gen_e_acsl_globals_init] as follows:
@@ -143,7 +143,7 @@ class e_acsl_visitor prj generate = object (self)
if generate then Project.copy ~selection ~src:cur prj;
Cil.DoChildrenPost
(fun f ->
- (* extend the main with forward initialization and put it at end *)
+ (* extend [main] with forward initialization and put it at end *)
if generate then begin
let must_init =
not (Literal_strings.is_empty ())
@@ -204,7 +204,7 @@ class e_acsl_visitor prj generate = object (self)
Cil.mkStmtOneInstr ~valid_sid:true (Set(Cil.var vi, e, loc))
:: Misc.mk_store_stmt ~str_size vi
:: Misc.mk_full_init_stmt ~addr:false vi
- :: Misc.mk_readonly vi
+ :: Misc.mk_mark_readonly vi
:: stmts)
stmts
in
@@ -291,10 +291,10 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
in
Project.on prj build_initializer ()
end; (* must_init *)
- (* Add a call to "__e_acsl_memory_init" that initializes memory
+ (* Add a call to [__e_acsl_memory_init] that initializes memory
storage and potentially records program arguments. Parameters to
- the "__e_acsl_memory_init" are addresses of program arguments or
- NULLs if main is declared without arguments. *)
+ [__e_acsl_memory_init] are addresses of program arguments or
+ NULLs if [main] is declared without arguments. *)
let build_mmodel_initializer () =
let loc = Location.unknown in
let nulls = [ Cil.zero loc ; Cil.zero loc ] in
@@ -354,7 +354,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
| g ->
let do_it = function
| GVar(vi, _, _) ->
- vi.vghost <- false; ()
+ vi.vghost <- false
| GFun({ svar = vi } as fundec, _) ->
vi.vghost <- false;
Builtins.update vi.vname vi;
@@ -380,7 +380,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
if generate then Cil.DoChildrenPost(fun g -> List.iter do_it g; g)
else Cil.DoChildren
- (* Add mappings from global variables to their initializers to [global_vars].
+ (* Add mappings from global variables to their initializers in [global_vars].
Note that the below function captures only [SingleInit]s. All compound
initializers (which contain single ones) are unrapped and thrown away. *)
method !vinit vi _off _i =
@@ -390,7 +390,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
Cil.DoChildrenPost
(fun i ->
(match is_initializer with
- (* Note the use of [add] instead [replace]. This is because a
+ (* Note the use of [add] instead of [replace]. This is because a
single variable can be associated with multiple initializers
and all of them need to be captured. *)
| true -> Varinfo.Hashtbl.add global_vars vi (Some i)
@@ -710,11 +710,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
| Var vi, NoOffset -> vi.vglob || vi.vformal
| _ -> false
in
-(* Options.feedback "%a? %a (%b && %b)"
- Printer.pp_lval assigned_lv
- Printer.pp_lval checked_lv
- (not (may_safely_ignore assigned_lv))
- (Pre_analysis.must_model_lval ~kf ~stmt checked_lv);*)
+
if not (may_safely_ignore assigned_lv) &&
Mmodel_analysis.must_model_lval ~kf ~stmt checked_lv
then
@@ -722,8 +718,8 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
(* must be in the new project to build a new stmt *)
Project.on
prj
- Misc.mk_debug_mmodel_stmt
- (Misc.mk_initialize loc assigned_lv)
+ (Misc.mk_initialize ~loc)
+ assigned_lv
in
let before = Cil.memo_stmt self#behavior stmt in
let new_stmt = Cil.memo_stmt self#behavior new_stmt in