Commit 92c096e9 authored by Kostyantyn Vorobyov's avatar Kostyantyn Vorobyov
Browse files

Changes as per MR review

parent e16d250e
......@@ -324,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 \
......
......@@ -293,22 +293,6 @@ let rec ptr_index ?(loc=Location.unknown) ?(index=(Cil.zero loc)) exp =
| SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _
-> assert false
(* ************************************************************************** *)
(** {2 Debug} *)
(* ************************************************************************** *)
let stringify_type = function
| TVoid(_) -> "TVoid" | TInt(_) -> "TInt" | TFloat(_) -> "TFloat"
| TPtr(_) -> "TPtr" | TArray(_) -> "TArray" | TFun(_) -> "TFun"
| TNamed(_) -> "TNamed" | TComp(_) -> "TComp" | TEnum(_) -> "TEnum"
| TBuiltin_va_list(_) -> "TBuiltin_va_list"
let stringify_enode = function
| Const(_) -> "Const" | Lval(_) -> "Lval" | SizeOf(_) -> "SizeOf"
| SizeOfE(_) -> "SizeOfE" | SizeOfStr(_) -> "SizeOfStr"
| AlignOf(_) -> "AlignOf" | AlignOfE(_) -> "AlignOfE" | UnOp(_) -> "UnOp"
| BinOp(_) -> "BinOp" | CastE(_) -> "CastE" | AddrOf(_) -> "AddrOf"
| StartOf(_) -> "StartOf" | Info(_) -> "Info"
(*
Local Variables:
compile-command: "make"
......
......@@ -126,16 +126,6 @@ val is_generated_literal_string_varinfo: varinfo -> bool
val is_generated_kf: kernel_function -> bool
(** Same as [is_generated_varinfo] but for kernel functions *)
(* ************************************************************************** *)
(** {2 Debug} *)
(* ************************************************************************** *)
val stringify_type: typ -> string
(** Return a string coresponding to a given Cil_types.typ *)
val stringify_enode: exp_node -> string
(** Return a string coresponding to a given Cil_types.exp_enode *)
(*
Local Variables:
compile-command: "make"
......
......@@ -199,7 +199,7 @@ 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
......
......@@ -298,17 +298,17 @@ static void validate_memory_layout() {
/* Assert that `_addr` is on heap and it is the base address of an allocated
* heap memory block */
#define DVALIATE_FREEABLE(_addr) \
DVASSERT(IS_ON_HEAP(_addr), "Expected heap location: %a\n ", _addr); \
#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);
"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, (uintptr_t)_addr), \
"Operation on unallocated heap block [%a + %lu]\n ", _addr, _size)
"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)
......@@ -318,22 +318,24 @@ static void validate_memory_layout() {
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); \
"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 static location: %a\n ", _addr); \
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)
"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 static 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 static 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)
......@@ -341,9 +343,10 @@ static void validate_memory_layout() {
# 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: %a\n", a + 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: [%a + %lu]\n ", a, i); \
"Expected static unallocated location in freea: [%a + %lu]\n", a, i); \
} \
}
......@@ -355,7 +358,7 @@ static void validate_memory_layout() {
/* 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 ", \
"Operation on unallocated block [%a + %lu] with base %a\n", \
_addr, _size, _base)
/* Assert that memory block [_addr, _addr + _size] is allocated
......@@ -384,7 +387,7 @@ static void validate_memory_layout() {
# define DVALIDATE_IS_ON_GLOBAL
# define DVALIDATE_IS_ON_TLS
# define DVALIDATE_IS_ON_STATIC
# define DVALIATE_FREEABLE
# define DVALIDATE_FREEABLE
# define DVALIDATE_STATIC_FREE
# define DVALIDATE_HEAP_FREE
# define DVALIDATE_RO_ACCESS
......@@ -450,11 +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 */
/*! \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 */
/*! \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 `_addr` within its block */
/*! \brief Return the byte offset of `_addr` within its block */
#define offset(_addr) predicate((uintptr_t)_addr, 'O')
/* }}} */
......@@ -854,7 +857,7 @@ static void* shadow_calloc(size_t nmemb, size_t size) {
* 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) {
DVALIATE_FREEABLE(((uintptr_t)ptr));
DVALIDATE_FREEABLE(((uintptr_t)ptr));
/* Base address of shadow block */
uintptr_t *base_shadow = (uintptr_t*)HEAP_SHADOW(ptr);
/* Physical allocation size */
......
......@@ -81,7 +81,7 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(*__gen_e_acsl_at_6),
sizeof(int),
(void *)(*__gen_e_acsl_at_6),
(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)",
......
......@@ -68,7 +68,7 @@ int main(int argc, char **argv)
{
int __gen_e_acsl_valid;
__gen_e_acsl_valid = __e_acsl_valid((void *)(_A),sizeof(char *),
(void *)(_A),(void *)(& _A));
(void *)(_A),(void *)(_A));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"main",
(char *)"\\valid((char **)_A)",33);
}
......@@ -129,7 +129,7 @@ int main(int argc, char **argv)
{
int __gen_e_acsl_valid_3;
__gen_e_acsl_valid_3 = __e_acsl_valid((void *)(_D),sizeof(int),
(void *)(_D),(void *)(& _D));
(void *)(_D),(void *)(_D));
__e_acsl_assert(__gen_e_acsl_valid_3,(char *)"Assertion",(char *)"main",
(char *)"\\valid((int *)_D)",38);
}
......
......@@ -594,7 +594,7 @@ and mmodel_call_valid ~loc kf name ctx env t =
let base, _ = Misc.ptr_index ~loc e in
let base_addr = match base.enode with
| AddrOf _ | Const _ -> base
| Lval(lv) | StartOf(lv) -> Cil.mkAddrOf ~loc lv
| Lval(lv) | StartOf(lv) -> Cil.mkAddrOrStartOf ~loc lv
| _ -> assert false
in
let _, res, env =
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment