Commit e1215a66 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[tests] fix options for launching test

parent d9d05e18
/* run.config
OPT: @MACHDEP@ -deps -print
OPT: @CXX@ @MACHDEP@ -print -deps
*/
// Function func should be analysed based on its source definition. Generating
......
......@@ -256,11 +256,11 @@ Now output intermediate result
{0}
[eva] tests/stl/stl_unique_ptr.cpp:9:
allocating variable __malloc_test_primitive_payload_l9
[eva:alarm] FRAMAC_SHARE/frama-clang/libc++/memory:477: Warning:
[eva:alarm] share/libc++/memory:477: Warning:
function operator*: postcondition got status unknown.
[eva] tests/stl/stl_unique_ptr.cpp:15:
allocating variable __malloc_test_primitive_payload_l15
[eva:alarm] FRAMAC_SHARE/frama-clang/libc++/memory:577: Warning:
[eva:alarm] share/libc++/memory:577: Warning:
function operator[]: postcondition got status unknown.
[eva:alarm] tests/stl/stl_unique_ptr.cpp:17: Warning:
signed overflow.
......@@ -1794,6 +1794,23 @@ void *memchr(void const *s, int c, size_t n);
*/
void *memcpy(void * restrict dest, void const * restrict src, size_t n);
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
requires
separation:
\separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
ensures
copied_contents:
memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
0;
ensures result_next_byte: \result ≡ \old(dest) + \old(n);
assigns *((char *)dest + (0 .. n - 1)), \result;
assigns *((char *)dest + (0 .. n - 1))
\from *((char *)src + (0 .. n - 1));
assigns \result \from dest, n;
*/
void *mempcpy(void * restrict dest, void const * restrict src, size_t n);
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
ensures
......
/* run.config
OPT: @MACHDEP@ -deps -print
STDOPT: #"-deps"
*/
#include <memory>
......
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