Skip to content

GitLab

Commit 501e7012 authored by Julien Signoles's avatar Julien Signoles
Browse files

[runtime] better ACSL contracts for RTL API

parent 3c92c4cf
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/share/e-acsl/e_acsl.h
View file @ 501e7012
......@@ -191,7 +191,8 @@ void memory_clean(void)
*
* \param ptr base address of the tracked memory block
* \param size size of the tracked block in bytes */
/*@ assigns \result \from *(((char*)ptr)+(0..size-1)); */
/*@ ensures \result == ptr;
@ assigns \result \from *(((char*)ptr)+(0..size-1)), ptr, size; */
void * store_block(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
......@@ -201,7 +202,8 @@ void * store_block(void * ptr, size_t size)
*
* \param ptr base address of the tracked memory block
* \param size size of the tracked block in bytes */
/*@ assigns \result \from *(((char*)ptr)+(0..size-1)); */
/*@ ensures \result == ptr;
@ assigns \result \from *(((char*)ptr)+(0..size-1)), ptr, size; */
void * store_block_duplicate(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
......@@ -228,19 +230,18 @@ void full_init(void * ptr)
void mark_readonly(void * ptr)
__attribute__((FC_BUILTIN));
/*@ ghost int extern __e_acsl_internal_heap; */
/*! \brief Return the cumulative size (in bytes) of tracked heap allocation. */
/*@ assigns \result \from __e_acsl_internal_heap; */
size_t get_heap_allocation_size(void)
__attribute__((FC_BUILTIN));
/*! \brief A variable holding a byte size of tracked heap allocation. */
extern size_t heap_allocation_size;
/*@ predicate diffSize{L1,L2}(integer i) =
\at(heap_allocation_size, L1)
- \at(heap_allocation_size, L2) == i; */
/*! \brief Return the cumulative size (in bytes) of tracked heap allocation. */
/*@ assigns \result \from heap_allocation_size; */
size_t get_heap_allocation_size(void)
__attribute__((FC_BUILTIN));
/* }}} */
/************************************************************************/
......@@ -266,10 +267,10 @@ int freeable(void * ptr)
* needs to be valid
* @param base - if `ptr` can be represented by the expression `p+i` then
* `base` refers to `p`
* @param addrof_base - if `ptr` can be represented by the expression `p+i`
* then `addrof_base` refers to `&p`. For the cases when the address of `p`
* cannot be taken (e.g., address of a static array or a constant value
* casted to a pointer) then `addrof_base` is zero.
* @param addrof_base - if `ptr` can be represented by the expression `p+i`
* then `addrof_base` refers to `&p`. For the cases when the address of `p`
* cannot be taken (e.g., address of a static array or a constant value
* casted to a pointer) then `addrof_base` is zero.
*
* @returns
* `true` if regions `[ptr, ptr + size]` and `[base, base + size]` are
......@@ -278,12 +279,25 @@ int freeable(void * ptr)
* then only region `[ptr, ptr + size]` should lie within the same block
* and be writable.
*/
/* FIXME: The following E-ACSL contract is obsolete and needs to be
synchronized with the above description. */
/*@ ensures \result == 0 || \result == 1;
@ ensures \result == 1 ==> \valid(((char *)ptr)+(0..size-1));
@ assigns \result \from *(((char*)ptr)+(0..size-1)); */
/*@ assigns \result \from *(((char*)ptr)+(0..size-1)), ptr, size;
@ behavior valid:
@ assumes \valid(((char *)ptr)+(0..size-1));
@ assumes
@ size <= 0 ||
@ ! \separated(((char *)ptr)+(0..size-1),
@ ((char *)\base_addr(base))+(0..\block_length(base)-1));
@ ensures \result == 1;
@ behavior invalid_ptr:
@ assumes ! \valid(((char *)ptr)+(0..size-1));
@ ensures \result == 0;
@ behavior separated_ptr:
@ assumes size > 0;
@ assumes \separated(((char *)ptr)+(0..size-1),
@ ((char *)\base_addr(base))+(0..\block_length(base)-1));
@ ensures \result == 0;
@ complete behaviors;
@ disjoint behaviors;
@ */
int valid(void * ptr, size_t size, void *base, void *addrof_base)
__attribute__((FC_BUILTIN));
......@@ -291,13 +305,26 @@ int valid(void * ptr, size_t size, void *base, void *addrof_base)
*
* Same as ::valid except the checked memory locations are only
* required to be allocated. */
/* FIXME: The following E-ACSL contract is obsolete and needs to be
synchronized with the above description. */
/*@ ensures \result == 0 || \result == 1;
@ ensures \result == 1 ==> \valid_read(((char *)ptr)+(0..size-1));
@ assigns \result \from *(((char*)ptr)+(0..size-1)); */
int valid_read(void * ptr, size_t size, void *ptr_base, void *addrof_base)
/*@ assigns \result \from *(((char*)ptr)+(0..size-1)), ptr, size;
@ behavior valid:
@ assumes \valid_read(((char *)ptr)+(0..size-1));
@ assumes
@ size <= 0 ||
@ ! \separated(((char *)ptr)+(0..size-1),
@ ((char *)\base_addr(base))+(0..\block_length(base)-1));
@ ensures \result == 1;
@ behavior invalid_ptr:
@ assumes ! \valid_read(((char *)ptr)+(0..size-1));
@ ensures \result == 0;
@ behavior separated_ptr:
@ assumes size > 0;
@ assumes \separated(((char *)ptr)+(0..size-1),
@ ((char *)\base_addr(base))+(0..\block_length(base)-1));
@ ensures \result == 0;
@ complete behaviors;
@ disjoint behaviors;
@ */
int valid_read(void * ptr, size_t size, void *base, void *addrof_base)
__attribute__((FC_BUILTIN));
/*! \brief Implementation of the \b \\base_addr predicate of E-ACSL.
......@@ -327,9 +354,16 @@ size_t offset(void * ptr)
/*! \brief Implementation of the \b \\initialized predicate of E-ACSL.
* Return a non-zero value if \p size bytes starting from an address given by
* \p ptr are initialized and zero otherwise. */
/*@ ensures \result == 0 || \result == 1;
@ ensures \result == 1 ==> \initialized(((char *)ptr)+(0..size-1));
@ assigns \result \from *(((char*)ptr)+(0..size-1)); */
/*@ assigns \result \from *(((char*)ptr)+(0..size-1)), ptr, size;
@ behavior initialized:
@ assumes \initialized(((char *)ptr)+(0..size-1));
@ ensures \result == 1;
@ behavior uninitialized:
@ assumes ! \initialized(((char *)ptr)+(0..size-1));
@ ensures \result == 0;
@ complete behaviors;
@ disjoint behaviors;
@ */
int initialized(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
/* }}} */
......@@ -338,38 +372,64 @@ int initialized(void * ptr, size_t size)
/*** Drop-in replacement functions {{{ ***/
/************************************************************************/
/*@ assigns dest[0..] \from src[0..];
@ assigns \result \from dest;
@ ensures \result == dest; */
char *builtin_strcpy(char *dest, const char *src)
__attribute__((FC_BUILTIN));
/*@ assigns dest[0..n - 1] \from src[0..n-1];
@ assigns \result \from dest;
@ ensures \result == dest; */
char *builtin_strncpy(char *dest, const char *src, size_t n)
__attribute__((FC_BUILTIN));
/*@ assigns \result \from s[0..]; */
size_t builtin_strlen(const char *s)
__attribute__((FC_BUILTIN));
/*@ assigns dest[..] \from src[0..];
@ assigns \result \from dest;
@ ensures \result == dest; */
char *builtin_strcat(char *dest, const char *src)
__attribute__((FC_BUILTIN));
/*@ assigns dest[..] \from src[0..n];
@ assigns \result \from dest;
@ ensures \result == dest; */
char *builtin_strncat(char *dest, const char *src, size_t n)
__attribute__((FC_BUILTIN));
/*@ assigns \result \from s1[0..], s2[0..]; */
int builtin_strcmp(const char *s1, const char *s2)
__attribute__((FC_BUILTIN));
/*@ assigns \result \from s1[0..n-1], s2[0..n-1]; */
int builtin_strncmp(const char *s1, const char *s2, size_t n)
__attribute__((FC_BUILTIN));
/*@ assigns ((char*)dest)[0..n-1] \from ((char*)src)[0..n-1];
@ assigns \result \from dest;
@ ensures \result == dest; */
void *builtin_memcpy(void *dest, const void *src, size_t n)
__attribute__((FC_BUILTIN));
/*@ assigns ((char*)s)[0..n-1] \from c;
@ assigns \result \from s;
@ ensures \result == s; */
void *builtin_memset(void *s, int c, size_t n)
__attribute__((FC_BUILTIN));
/*@ assigns ((char*)dest)[0..n-1] \from ((char*)src)[0..n-1];
@ assigns \result \from dest;
@ ensures \result == dest; */
void *builtin_memmove(void *dest, const void *src, size_t n)
__attribute__((FC_BUILTIN));
/*@ assigns \result \from ((char*)s1)[0..n-1], ((char*)s2)[0..n-1]; */
int builtin_memcmp(const void *s1, const void *s2, size_t n)
__attribute__((FC_BUILTIN));
/* }}} */
/************************************************************************/
......
src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle
View file @ 501e7012
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
tests/bts/bts1304.i:23:[value] warning: assertion got status unknown.
tests/bts/bts1304.i:23:[value] warning: function __e_acsl_assert: precondition got status unknown.
src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
View file @ 501e7012
......@@ -16,12 +16,3 @@ tests/bts/bts1307.i:11:[e-acsl] warning: E-ACSL construct `logic function applic
tests/bts/bts1307.i:11:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
tests/bts/bts1307.i:5:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/bts/bts1307.i:6:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/bts/bts1307.i:7:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/bts/bts1307.i:11:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/bts/bts1307.i:17:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/bts/bts1307.i:18:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/bts/bts1307.i:19:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/bts/bts1307.i:23:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/bts/bts1307.i:23:[value] warning: function __e_acsl_assert: precondition got status unknown.
src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle
View file @ 501e7012
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
tests/bts/bts1326.i:8:[value] warning: function __e_acsl_assert: precondition got status unknown.
src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
View file @ 501e7012
......@@ -2,6 +2,5 @@
[e-acsl] translation done in project "e-acsl".
tests/bts/bts1390.c:12:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/bts/bts1390.c:9:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/bts/bts1390.c:10:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/bts/bts1390.c:13:[value] warning: function __gen_e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/bts/bts1390.c:18:[value] warning: out of bounds read. assert \valid_read(s);
src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle
View file @ 501e7012
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
tests/bts/bts1399.c:22:[value] warning: function __e_acsl_assert: precondition got status unknown.
src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle
View file @ 501e7012
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
tests/bts/bts1478.c:10:[value] warning: function __e_acsl_assert: precondition got status unknown.
src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle
View file @ 501e7012
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
tests/bts/bts1700.i:9:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/bts/bts1700.i:12:[value] warning: function __e_acsl_assert: precondition got status unknown.
src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle
View file @ 501e7012
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
tests/bts/bts1717.i:10:[value] warning: function __e_acsl_assert: precondition got status unknown.
src/plugins/e-acsl/tests/bts/oracle/bts1718.res.oracle
View file @ 501e7012
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
tests/bts/bts1718.i:13:[value] warning: function __e_acsl_assert: precondition got status unknown.
src/plugins/e-acsl/tests/bts/oracle/bts1740.res.oracle
View file @ 501e7012
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
tests/bts/bts1740.i:11:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/bts/bts1740.i:12:[value] warning: locals {a} escaping the scope of a block of main through p
tests/bts/bts1740.i:16:[value] warning: accessing left-value that contains escaping addresses.
assert ¬\dangling(&p);
src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle
View file @ 501e7012
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
tests/bts/bts1837.i:20:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/bts/bts1837.i:21:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/bts/bts1837.i:18:[value] warning: signed overflow. assert -2147483648 ≤ i - 1;
tests/bts/bts1837.i:10:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/bts/bts1837.i:11:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/bts/bts1837.i:12:[value] warning: function __e_acsl_assert: precondition got status unknown.
src/plugins/e-acsl/tests/bts/oracle/bts2191.res.oracle
View file @ 501e7012
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
tests/bts/bts2191.c:22:[value] warning: function __e_acsl_assert: precondition got status unknown.
src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle
View file @ 501e7012
......@@ -5,4 +5,3 @@
FRAMAC_SHARE/libc/stdlib.h:76:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/libc/stdlib.h:76:[value] warning: function __e_acsl_assert: precondition got status unknown.
src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle
View file @ 501e7012
......@@ -2,5 +2,4 @@ tests/bts/bts2252.c:22:[kernel] warning: Calling undeclared function strncpy. Ol
[e-acsl] beginning translation.
tests/bts/bts2252.c:22:[kernel] warning: Neither code nor specification for function strncpy, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
tests/bts/bts2252.c:16:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/bts/bts2252.c:17:[value] warning: out of bounds read. assert \valid_read(srcbuf + i);
src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle
View file @ 501e7012
......@@ -47,7 +47,6 @@ FRAMAC_SHARE/libc/string.h:359:[e-acsl] warning: E-ACSL construct `assigns claus
__e_acsl_init ∈ [--..--]
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_allocation_size ∈ [--..--]
__e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
__e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
......
src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
View file @ 501e7012
......@@ -55,7 +55,6 @@ FRAMAC_SHARE/libc/stdlib.h:415:[e-acsl] warning: E-ACSL construct `assigns claus
stderr ∈ {{ NULL ; &S___fc_stderr[0] }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_allocation_size ∈ [--..--]
__e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
__e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
......@@ -101,7 +100,6 @@ FRAMAC_SHARE/libc/stdlib.h:415:[e-acsl] warning: E-ACSL construct `assigns claus
[value] using specification for function __e_acsl_full_init
[value] using specification for function __e_acsl_mark_readonly
[value] using specification for function strdup
FRAMAC_SHARE/libc/string.h:401:[value] warning: no 'assigns \result \from ...' clause specified for function strdup
FRAMAC_SHARE/libc/string.h:396:[value] warning: ignoring unsupported \allocates clause
FRAMAC_SHARE/libc/string.h:399:[value] warning: function strdup: this postcondition evaluates to false in this context.
If it is valid, either a precondition was not verified for this call,
......
src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
View file @ 501e7012
......@@ -50,7 +50,6 @@ FRAMAC_SHARE/libc/string.h:316:[e-acsl] warning: E-ACSL construct `assigns claus
__e_acsl_init ∈ [--..--]
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_allocation_size ∈ [--..--]
__e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
__e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
......@@ -87,7 +86,6 @@ FRAMAC_SHARE/libc/string.h:316:[e-acsl] warning: E-ACSL construct `assigns claus
[value] using specification for function __e_acsl_full_init
[value] using specification for function __e_acsl_mark_readonly
[value] using specification for function strdup
FRAMAC_SHARE/libc/string.h:401:[value] warning: no 'assigns \result \from ...' clause specified for function strdup
FRAMAC_SHARE/libc/string.h:396:[value] warning: ignoring unsupported \allocates clause
FRAMAC_SHARE/libc/string.h:399:[value] warning: function strdup: this postcondition evaluates to false in this context.
If it is valid, either a precondition was not verified for this call,
......
src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
View file @ 501e7012
......@@ -40,7 +40,6 @@ FRAMAC_SHARE/libc/stdlib.h:415:[e-acsl] warning: E-ACSL construct `assigns claus
__e_acsl_init ∈ [--..--]
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_allocation_size ∈ [--..--]
__e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
__e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
......@@ -68,7 +67,6 @@ FRAMAC_SHARE/libc/stdlib.h:415:[e-acsl] warning: E-ACSL construct `assigns claus
[value] using specification for function __e_acsl_full_init
[value] using specification for function __e_acsl_mark_readonly
[value] using specification for function strdup
FRAMAC_SHARE/libc/string.h:401:[value] warning: no 'assigns \result \from ...' clause specified for function strdup
FRAMAC_SHARE/libc/string.h:396:[value] warning: ignoring unsupported \allocates clause
FRAMAC_SHARE/libc/string.h:399:[value] warning: function strdup: this postcondition evaluates to false in this context.
If it is valid, either a precondition was not verified for this call,
......
src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
View file @ 501e7012
......@@ -42,7 +42,6 @@ FRAMAC_SHARE/libc/stdio.h:89:[e-acsl] warning: E-ACSL construct `assigns clause
stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_allocation_size ∈ [--..--]
__e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
__e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
......
Supports Markdown
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