diff --git a/share/libc/stdlib.c b/share/libc/stdlib.c
index 72dd24cc238641547c7bdcd5f4855cc7f099936f..d9c40ce3983b2ad6ee27c15da26fba50d6889453 100644
--- a/share/libc/stdlib.c
+++ b/share/libc/stdlib.c
@@ -187,4 +187,19 @@ int unsetenv(const char *name)
char __fc_strerror[64];
#endif
+// Note: this implementation does not check the alignment, since it cannot
+// currently be specified in the memory model of most plug-ins
+int posix_memalign(void **memptr, size_t alignment, size_t size) {
+ // By default, specifications in the libc are ignored for defined functions,
+ // and since we do not actually use alignment, we need to check its validity.
+ // The assertion below is the requires in the specification.
+ /*@ assert alignment_is_a_suitable_power_of_two:
+ alignment >= sizeof(void*) &&
+ ((size_t)alignment & ((size_t)alignment - 1)) == 0;
+ */
+ *memptr = malloc(size);
+ if (!*memptr) return ENOMEM;
+ return 0;
+}
+
__POP_FC_STDLIB
diff --git a/share/libc/stdlib.h b/share/libc/stdlib.h
index acdbbf87f659a078e3a89127771f0089eb11704c..e69ed2aa5b7dd00a0a704e72dc6e398b8036dfe2 100644
--- a/share/libc/stdlib.h
+++ b/share/libc/stdlib.h
@@ -594,6 +594,34 @@ extern size_t wcstombs(char * restrict s,
size_t n);
+// Note: this specification should ideally use a more specific predicate,
+// such as 'is_allocable_aligned(alignment, size)'.
+/*@
+ requires valid_memptr: \valid(memptr);
+ requires alignment_is_a_suitable_power_of_two:
+ alignment >= sizeof(void*) &&
+ ((size_t)alignment & ((size_t)alignment - 1)) == 0;
+ allocates *memptr;
+ assigns __fc_heap_status \from indirect:alignment, size, __fc_heap_status;
+ assigns \result \from indirect:alignment, indirect:size,
+ indirect:__fc_heap_status;
+ behavior allocation:
+ assumes can_allocate: is_allocable(size);
+ assigns __fc_heap_status \from indirect:alignment, size, __fc_heap_status;
+ assigns \result \from indirect:alignment, indirect:size,
+ indirect:__fc_heap_status;
+ ensures allocation: \fresh(*memptr,size);
+ ensures result_zero: \result == 0;
+ behavior no_allocation:
+ assumes cannot_allocate: !is_allocable(size);
+ assigns \result \from indirect:alignment;
+ allocates \nothing;
+ ensures result_non_zero: \result < 0 || \result > 0;
+ complete behaviors;
+ disjoint behaviors;
+ */
+extern int posix_memalign(void **memptr, size_t alignment, size_t size);
+
__END_DECLS
__POP_FC_STDLIB
diff --git a/src/plugins/value/utils/library_functions.ml b/src/plugins/value/utils/library_functions.ml
index 0cb2c758547d844a1af22eb5b4376b1d3c459a98..f9abcf51c3c3ddeab1fdcc9152b23ce7cf61f99e 100644
--- a/src/plugins/value/utils/library_functions.ml
+++ b/src/plugins/value/utils/library_functions.ml
@@ -79,6 +79,7 @@ let unsupported_specifications =
"strdup", "string.c";
"strndup", "string.c";
"getenv", "stdlib.c";
+ "posix_memalign", "stdlib.c";
"putenv", "stdlib.c";
"setenv", "stdlib.c";
"unsetenv", "stdlib.c"
diff --git a/tests/libc/oracle/coverage.res.oracle b/tests/libc/oracle/coverage.res.oracle
index 022ec6cf4bf93925c11032ef63434f829269cac5..6c5fe3be202d1c7a64d8bd4f0dbc15e336cac7d4 100644
--- a/tests/libc/oracle/coverage.res.oracle
+++ b/tests/libc/oracle/coverage.res.oracle
@@ -28,7 +28,7 @@
main: 4 stmts out of 4 (100.0%)
[metrics] Eva coverage statistics
=======================
- Syntactically reachable functions = 2 (out of 75)
+ Syntactically reachable functions = 2 (out of 76)
Semantically reached functions = 2
Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 60e8d3f8a81faf8bef3d2ea162812f2ec0c00651..27fb20cb71c1294c6261d45bae24f3d04dceeef2 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -13,7 +13,7 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
-[metrics] Defined functions (73)
+[metrics] Defined functions (74)
======================
Frama_C_double_interval (0 call); Frama_C_float_interval (0 call);
Frama_C_interval (13 calls); Frama_C_nondet (11 calls);
@@ -28,14 +28,14 @@
isprint (0 call); ispunct (0 call); isspace (1 call); isupper (0 call);
isxdigit (0 call); localeconv (0 call); main (0 call); memchr (0 call);
memcmp (0 call); memcpy (2 calls); memmove (0 call); memrchr (0 call);
- memset (1 call); putenv (0 call); setenv (0 call); setlocale (0 call);
- strcasecmp (0 call); strcat (0 call); strchr (3 calls); strcmp (0 call);
- strcpy (0 call); strdup (0 call); strerror (0 call); strlen (6 calls);
- strncat (0 call); strncmp (0 call); strncpy (0 call); strndup (0 call);
- strnlen (0 call); strrchr (0 call); strstr (0 call); tolower (0 call);
- toupper (0 call); unsetenv (0 call); wcscat (0 call); wcscpy (0 call);
- wcslen (2 calls); wcsncat (0 call); wcsncpy (0 call); wmemcpy (0 call);
- wmemset (0 call);
+ memset (1 call); posix_memalign (0 call); putenv (0 call); setenv (0 call);
+ setlocale (0 call); strcasecmp (0 call); strcat (0 call); strchr (3 calls);
+ strcmp (0 call); strcpy (0 call); strdup (0 call); strerror (0 call);
+ strlen (6 calls); strncat (0 call); strncmp (0 call); strncpy (0 call);
+ strndup (0 call); strnlen (0 call); strrchr (0 call); strstr (0 call);
+ tolower (0 call); toupper (0 call); unsetenv (0 call); wcscat (0 call);
+ wcscpy (0 call); wcslen (2 calls); wcsncat (0 call); wcsncpy (0 call);
+ wmemcpy (0 call); wmemset (0 call);
Undefined functions (360)
=========================
@@ -104,7 +104,7 @@
localtime (0 call); log (0 call); log10 (0 call); log10f (0 call);
log10l (0 call); log2 (0 call); log2f (0 call); log2l (0 call);
logf (0 call); logl (0 call); longjmp (0 call); lrand48 (0 call);
- malloc (6 calls); mblen (0 call); mbstowcs (0 call); mbtowc (0 call);
+ malloc (7 calls); mblen (0 call); mbstowcs (0 call); mbtowc (0 call);
memoverlap (1 call); mkdir (0 call); mktime (0 call); nan (0 call);
nanf (0 call); nanl (0 call); nanosleep (0 call); ntohl (0 call);
ntohs (0 call); open (0 call); openat (0 call); opendir (0 call);
@@ -162,18 +162,18 @@
Global metrics
==============
- Sloc = 948
- Decision point = 183
+ Sloc = 956
+ Decision point = 184
Global variables = 58
- If = 174
+ If = 175
Loop = 40
- Goto = 78
- Assignment = 379
- Exit point = 73
- Function = 433
- Function call = 73
- Pointer dereferencing = 146
- Cyclomatic complexity = 256
+ Goto = 79
+ Assignment = 382
+ Exit point = 74
+ Function = 434
+ Function call = 74
+ Pointer dereferencing = 148
+ Cyclomatic complexity = 258
/* Generated by Frama-C */
#include "__fc_builtin.c"
#include "__fc_builtin.h"
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index ca6d82677730323b0caf2c381e8440319f4a8896..d649b563c77dcd5d8464e949284cad01c611a625 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -1906,6 +1906,8 @@ extern size_t mbstowcs(wchar_t * __restrict pwcs, char const * __restrict s,
extern size_t wcstombs(char * __restrict s, wchar_t const * __restrict pwcs,
size_t n);
+int posix_memalign(void **memptr, size_t alignment, size_t size);
+
int glob(char const *pattern, int flags,
int (*errfunc)(char const *epath, int eerrno), glob_t *pglob)
{
@@ -4346,6 +4348,59 @@ int unsetenv(char const *name)
return_label: return __retres;
}
+/*@ requires valid_memptr: \valid(memptr);
+ requires
+ alignment_is_a_suitable_power_of_two:
+ alignment ≥ sizeof(void *) ∧
+ ((unsigned int)alignment & ((unsigned int)alignment - 1)) ≡ 0;
+ assigns __fc_heap_status, \result;
+ assigns __fc_heap_status
+ \from (indirect: alignment), size, __fc_heap_status;
+ assigns \result
+ \from (indirect: alignment), (indirect: size),
+ (indirect: __fc_heap_status);
+ allocates *\old(memptr);
+
+ behavior allocation:
+ assumes can_allocate: is_allocable(size);
+ ensures allocation: \fresh{Old, Here}(*\old(memptr),\old(size));
+ ensures result_zero: \result ≡ 0;
+ assigns __fc_heap_status, \result;
+ assigns __fc_heap_status
+ \from (indirect: alignment), size, __fc_heap_status;
+ assigns \result
+ \from (indirect: alignment), (indirect: size),
+ (indirect: __fc_heap_status);
+
+ behavior no_allocation:
+ assumes cannot_allocate: ¬is_allocable(size);
+ ensures result_non_zero: \result < 0 ∨ \result > 0;
+ assigns \result;
+ assigns \result \from (indirect: alignment);
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+int posix_memalign(void **memptr, size_t alignment, size_t size)
+{
+ int __retres;
+ /*@
+ assert
+ alignment_is_a_suitable_power_of_two:
+ alignment ≥ sizeof(void *) ∧
+ ((unsigned int)alignment & ((unsigned int)alignment - 1)) ≡ 0;
+ */
+ ;
+ *memptr = malloc(size);
+ if (! *memptr) {
+ __retres = 12;
+ goto return_label;
+ }
+ __retres = 0;
+ return_label: return __retres;
+}
+
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
requires
diff --git a/tests/libc/oracle/stdlib_c.0.res.oracle b/tests/libc/oracle/stdlib_c.0.res.oracle
index b95eac34de167bf145daa4266e881ffb644afe7a..1a7d60180779c859e8ad53b009b2d574aa0ec047 100644
--- a/tests/libc/oracle/stdlib_c.0.res.oracle
+++ b/tests/libc/oracle/stdlib_c.0.res.oracle
@@ -76,9 +76,42 @@
[eva:malloc] tests/libc/stdlib_c.c:32:
resizing variable `__calloc_w_main_l32'
(0..31/34359738367) to fit 0..63/34359738367
+[eva] computing for function posix_memalign <- main.
+ Called from tests/libc/stdlib_c.c:37.
+[eva] share/libc/stdlib.c:197:
+ assertion 'alignment_is_a_suitable_power_of_two' got status valid.
+[eva] share/libc/stdlib.c:200: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:200: allocating variable __malloc_posix_memalign_l200
+[eva] Recording results for posix_memalign
+[eva] Done for function posix_memalign
+[eva] computing for function free <- main.
+ Called from tests/libc/stdlib_c.c:38.
+[eva] using specification for function free
+[eva] tests/libc/stdlib_c.c:38: Warning: ignoring unsupported \allocates clause
+[eva] tests/libc/stdlib_c.c:38:
+ function free: precondition 'freeable' got status valid.
+[eva] Done for function free
+[eva] computing for function posix_memalign <- main.
+ Called from tests/libc/stdlib_c.c:39.
+[eva] share/libc/stdlib.c:200: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:200:
+ allocating variable __malloc_posix_memalign_l200_0
+[eva] Recording results for posix_memalign
+[eva] Done for function posix_memalign
+[eva] computing for function free <- main.
+ Called from tests/libc/stdlib_c.c:40.
+[eva] tests/libc/stdlib_c.c:40: Warning: ignoring unsupported \allocates clause
+[eva] tests/libc/stdlib_c.c:40:
+ function free: precondition 'freeable' got status valid.
+[eva] Done for function free
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function posix_memalign:
+ __fc_heap_status ∈ [--..--]
+ p_al0 ∈ {{ NULL ; &__malloc_posix_memalign_l200[0] }}
+ p_al1 ∈ {{ NULL ; &__malloc_posix_memalign_l200_0[0] }} or UNINITIALIZED
+ __retres ∈ {0; 12}
[eva:final-states] Values at end of function main:
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
@@ -87,5 +120,9 @@
q ∈ {{ NULL ; &__calloc_main_l21[0] }}
r ∈ {0}
s ∈ {{ NULL ; &__calloc_w_main_l32[0] }}
+ p_al0 ∈ {{ NULL ; &__malloc_posix_memalign_l200[0] }}
+ p_al1 ∈ {{ NULL ; &__malloc_posix_memalign_l200_0[0] }}
+ p_memal_res ∈ {0; 12}
+ p_memal_res2 ∈ {0; 12}
__retres ∈ {0}
__calloc_w_main_l32[0..1073741823] ∈ {0; 42}
diff --git a/tests/libc/oracle/stdlib_c.1.res.oracle b/tests/libc/oracle/stdlib_c.1.res.oracle
index 8dd967128d5fac44717cbb3a39886115ce154149..9021fc4d9d1690f4816abb040418148419280ab1 100644
--- a/tests/libc/oracle/stdlib_c.1.res.oracle
+++ b/tests/libc/oracle/stdlib_c.1.res.oracle
@@ -95,9 +95,42 @@
[eva:malloc] tests/libc/stdlib_c.c:32:
resizing variable `__calloc_w_main_l32'
(0..31/34359738367) to fit 0..191/34359738367
+[eva] computing for function posix_memalign <- main.
+ Called from tests/libc/stdlib_c.c:37.
+[eva] share/libc/stdlib.c:197:
+ assertion 'alignment_is_a_suitable_power_of_two' got status valid.
+[eva] share/libc/stdlib.c:200: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:200: allocating variable __malloc_posix_memalign_l200
+[eva] Recording results for posix_memalign
+[eva] Done for function posix_memalign
+[eva] computing for function free <- main.
+ Called from tests/libc/stdlib_c.c:38.
+[eva] using specification for function free
+[eva] tests/libc/stdlib_c.c:38: Warning: ignoring unsupported \allocates clause
+[eva] tests/libc/stdlib_c.c:38:
+ function free: precondition 'freeable' got status valid.
+[eva] Done for function free
+[eva] computing for function posix_memalign <- main.
+ Called from tests/libc/stdlib_c.c:39.
+[eva] share/libc/stdlib.c:200: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:200:
+ allocating variable __malloc_posix_memalign_l200_0
+[eva] Recording results for posix_memalign
+[eva] Done for function posix_memalign
+[eva] computing for function free <- main.
+ Called from tests/libc/stdlib_c.c:40.
+[eva] tests/libc/stdlib_c.c:40: Warning: ignoring unsupported \allocates clause
+[eva] tests/libc/stdlib_c.c:40:
+ function free: precondition 'freeable' got status valid.
+[eva] Done for function free
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function posix_memalign:
+ __fc_heap_status ∈ [--..--]
+ p_al0 ∈ {{ &__malloc_posix_memalign_l200[0] }}
+ p_al1 ∈ {{ &__malloc_posix_memalign_l200_0[0] }} or UNINITIALIZED
+ __retres ∈ {0}
[eva:final-states] Values at end of function main:
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
@@ -106,5 +139,9 @@
q ∈ {{ NULL ; &__calloc_main_l21[0] }}
r ∈ {0}
s ∈ {{ NULL ; &__calloc_w_main_l32[0] }}
+ p_al0 ∈ {{ &__malloc_posix_memalign_l200[0] }}
+ p_al1 ∈ {{ &__malloc_posix_memalign_l200_0[0] }}
+ p_memal_res ∈ {0}
+ p_memal_res2 ∈ {0}
__retres ∈ {0}
__calloc_w_main_l32[0..1073741823] ∈ {0; 42}
diff --git a/tests/libc/oracle/stdlib_c.2.res.oracle b/tests/libc/oracle/stdlib_c.2.res.oracle
index 8d66691a343b130e4ffd82e0d83ffecc8421c366..c70cca5c9ec4c02a371d875dd9c5978ed6f15c83 100644
--- a/tests/libc/oracle/stdlib_c.2.res.oracle
+++ b/tests/libc/oracle/stdlib_c.2.res.oracle
@@ -94,6 +94,34 @@
[eva] Done for function memset
[eva] Recording results for calloc
[eva] Done for function calloc
+[eva] computing for function posix_memalign <- main.
+ Called from tests/libc/stdlib_c.c:37.
+[eva] share/libc/stdlib.c:197:
+ assertion 'alignment_is_a_suitable_power_of_two' got status valid.
+[eva] share/libc/stdlib.c:200: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:200: allocating variable __malloc_posix_memalign_l200
+[eva] Recording results for posix_memalign
+[eva] Done for function posix_memalign
+[eva] computing for function free <- main.
+ Called from tests/libc/stdlib_c.c:38.
+[eva] using specification for function free
+[eva] tests/libc/stdlib_c.c:38: Warning: ignoring unsupported \allocates clause
+[eva] tests/libc/stdlib_c.c:38:
+ function free: precondition 'freeable' got status valid.
+[eva] Done for function free
+[eva] computing for function posix_memalign <- main.
+ Called from tests/libc/stdlib_c.c:39.
+[eva] share/libc/stdlib.c:200: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:200:
+ allocating variable __malloc_posix_memalign_l200_0
+[eva] Recording results for posix_memalign
+[eva] Done for function posix_memalign
+[eva] computing for function free <- main.
+ Called from tests/libc/stdlib_c.c:40.
+[eva] tests/libc/stdlib_c.c:40: Warning: ignoring unsupported \allocates clause
+[eva] tests/libc/stdlib_c.c:40:
+ function free: precondition 'freeable' got status valid.
+[eva] Done for function free
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -110,6 +138,11 @@
__malloc_calloc_l72[0..3] ∈ [--..--] or UNINITIALIZED
__malloc_calloc_l72_0[0..4294967291] ∈ [--..--] or UNINITIALIZED
__malloc_w_calloc_l72_1[0..4294967291] ∈ [--..--] or UNINITIALIZED
+[eva:final-states] Values at end of function posix_memalign:
+ __fc_heap_status ∈ [--..--]
+ p_al0 ∈ {{ NULL ; &__malloc_posix_memalign_l200[0] }}
+ p_al1 ∈ {{ NULL ; &__malloc_posix_memalign_l200_0[0] }} or UNINITIALIZED
+ __retres ∈ {0; 12}
[eva:final-states] Values at end of function main:
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
@@ -118,6 +151,10 @@
q ∈ {{ NULL ; (int *)&__malloc_calloc_l72_0 }}
r ∈ {0}
s ∈ {{ NULL ; (int *)&__malloc_w_calloc_l72_1 }} or UNINITIALIZED
+ p_al0 ∈ {{ NULL ; &__malloc_posix_memalign_l200[0] }}
+ p_al1 ∈ {{ NULL ; &__malloc_posix_memalign_l200_0[0] }}
+ p_memal_res ∈ {0; 12}
+ p_memal_res2 ∈ {0; 12}
__retres ∈ {0}
__malloc_calloc_l72[0..3] ∈ [--..--] or UNINITIALIZED
__malloc_calloc_l72_0[0..4294967291] ∈ [--..--] or UNINITIALIZED
diff --git a/tests/libc/stdlib_c.c b/tests/libc/stdlib_c.c
index 3bb9f5f8b671b06e7652ac3745dc3dea1ccf0cfa..d265774bec565ed9ea9b83b45ff1620f44465221 100644
--- a/tests/libc/stdlib_c.c
+++ b/tests/libc/stdlib_c.c
@@ -33,5 +33,11 @@ int main() {
if (s) s[i-1] = 42;
}
+ char *p_al0, *p_al1;
+ int p_memal_res = posix_memalign((void**)&p_al0, 32, 0);
+ free(p_al0);
+ int p_memal_res2 = posix_memalign((void**)&p_al1, 32, 42);
+ free(p_al1);
+
return 0;
}