Commit 99cc5514 authored by Andre Maroneze's avatar Andre Maroneze 💬
Browse files

sync with frama-c/frama-c!3512

parent ef0b5ef8
......@@ -1101,6 +1101,7 @@ size_t wcstombs(char * restrict s, int const * restrict pwcs, size_t n);
int posix_memalign(void **memptr, size_t alignment, size_t size);
/*@ requires valid_template: valid_string(templat);
requires template_len: strlen(templat) ≥ 6;
ensures
result_error_or_valid_fd: \result ≡ -1 ∨ (0 ≤ \result < 16);
assigns *(templat + (0 ..)), \result;
......@@ -1109,6 +1110,17 @@ int posix_memalign(void **memptr, size_t alignment, size_t size);
*/
int mkstemp(char *templat);
/*@ requires valid_template: valid_string(templat);
requires template_len: strlen(templat) ≥ 6 + suffixlen;
requires non_negative_suffixlen: suffixlen ≥ 0;
ensures
result_error_or_valid_fd: \result ≡ -1 ∨ (0 ≤ \result < 16);
assigns *(templat + (0 ..)), \result;
assigns *(templat + (0 ..)) \from \nothing;
assigns \result \from \nothing;
*/
int mkstemps(char *templat, int suffixlen);
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
/*@ requires \valid_read(this); */
......
......@@ -1070,6 +1070,7 @@ size_t wcstombs(char * restrict s, int const * restrict pwcs, size_t n);
int posix_memalign(void **memptr, size_t alignment, size_t size);
/*@ requires valid_template: valid_string(templat);
requires template_len: strlen(templat) ≥ 6;
ensures
result_error_or_valid_fd: \result ≡ -1 ∨ (0 ≤ \result < 16);
assigns *(templat + (0 ..)), \result;
......@@ -1078,4 +1079,15 @@ int posix_memalign(void **memptr, size_t alignment, size_t size);
*/
int mkstemp(char *templat);
/*@ requires valid_template: valid_string(templat);
requires template_len: strlen(templat) ≥ 6 + suffixlen;
requires non_negative_suffixlen: suffixlen ≥ 0;
ensures
result_error_or_valid_fd: \result ≡ -1 ∨ (0 ≤ \result < 16);
assigns *(templat + (0 ..)), \result;
assigns *(templat + (0 ..)) \from \nothing;
assigns \result \from \nothing;
*/
int mkstemps(char *templat, int suffixlen);
......@@ -3195,6 +3195,7 @@ size_t wcstombs(char * restrict s, int const * restrict pwcs, size_t n);
int posix_memalign(void **memptr, size_t alignment, size_t size);
/*@ requires valid_template: valid_string(templat);
requires template_len: strlen(templat) ≥ 6;
ensures
result_error_or_valid_fd: \result ≡ -1 ∨ (0 ≤ \result < 16);
assigns *(templat + (0 ..)), \result;
......@@ -3203,6 +3204,17 @@ int posix_memalign(void **memptr, size_t alignment, size_t size);
*/
int mkstemp(char *templat);
/*@ requires valid_template: valid_string(templat);
requires template_len: strlen(templat) ≥ 6 + suffixlen;
requires non_negative_suffixlen: suffixlen ≥ 0;
ensures
result_error_or_valid_fd: \result ≡ -1 ∨ (0 ≤ \result < 16);
assigns *(templat + (0 ..)), \result;
assigns *(templat + (0 ..)) \from \nothing;
assigns \result \from \nothing;
*/
int mkstemps(char *templat, int suffixlen);
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
/*@ requires \valid(this); */
......
......@@ -2974,6 +2974,7 @@ size_t wcstombs(char * restrict s, int const * restrict pwcs, size_t n);
int posix_memalign(void **memptr, size_t alignment, size_t size);
/*@ requires valid_template: valid_string(templat);
requires template_len: strlen(templat) ≥ 6;
ensures
result_error_or_valid_fd: \result ≡ -1 ∨ (0 ≤ \result < 16);
assigns *(templat + (0 ..)), \result;
......@@ -2982,6 +2983,17 @@ int posix_memalign(void **memptr, size_t alignment, size_t size);
*/
int mkstemp(char *templat);
/*@ requires valid_template: valid_string(templat);
requires template_len: strlen(templat) ≥ 6 + suffixlen;
requires non_negative_suffixlen: suffixlen ≥ 0;
ensures
result_error_or_valid_fd: \result ≡ -1 ∨ (0 ≤ \result < 16);
assigns *(templat + (0 ..)), \result;
assigns *(templat + (0 ..)) \from \nothing;
assigns \result \from \nothing;
*/
int mkstemps(char *templat, int suffixlen);
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
/*@ requires \valid(this); */
......
......@@ -2980,6 +2980,7 @@ size_t wcstombs(char * restrict s, int const * restrict pwcs, size_t n);
int posix_memalign(void **memptr, size_t alignment, size_t size);
/*@ requires valid_template: valid_string(templat);
requires template_len: strlen(templat) ≥ 6;
ensures
result_error_or_valid_fd: \result ≡ -1 ∨ (0 ≤ \result < 16);
assigns *(templat + (0 ..)), \result;
......@@ -2988,6 +2989,17 @@ int posix_memalign(void **memptr, size_t alignment, size_t size);
*/
int mkstemp(char *templat);
/*@ requires valid_template: valid_string(templat);
requires template_len: strlen(templat) ≥ 6 + suffixlen;
requires non_negative_suffixlen: suffixlen ≥ 0;
ensures
result_error_or_valid_fd: \result ≡ -1 ∨ (0 ≤ \result < 16);
assigns *(templat + (0 ..)), \result;
assigns *(templat + (0 ..)) \from \nothing;
assigns \result \from \nothing;
*/
int mkstemps(char *templat, int suffixlen);
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
/*@ requires \valid(this); */
......
......@@ -1774,6 +1774,8 @@ struct tm *gmtime(time_t const *timer);
ensures
result_null_or_internal_tm:
\result ≡ &__fc_time_tm ∨ \result ≡ \null;
ensures
maybe_error: __fc_errno ≡ \old(__fc_errno) ∨ __fc_errno ≡ 75;
assigns \result, __fc_time_tm;
assigns \result \from __fc_p_time_tm;
assigns __fc_time_tm \from *timer;
......@@ -1927,6 +1929,22 @@ int clock_nanosleep(clockid_t clock_id, int flags,
struct tm *gmtime_r(time_t const * restrict timer,
struct tm * restrict result);
/*@ requires valid_timer: \valid_read(timep);
requires valid_result: \valid(result);
ensures
initialization: result_null_or_initialized:
(\result ≡ \old(result) ∧ \initialized(\old(result))) ∨
\result ≡ \null;
ensures
maybe_error: __fc_errno ≡ \old(__fc_errno) ∨ __fc_errno ≡ 75;
assigns \result, *result, __fc_errno;
assigns \result \from (indirect: *timep), result;
assigns *result \from (indirect: *timep);
assigns __fc_errno \from (indirect: *timep);
*/
struct tm *localtime_r(time_t const * restrict timep,
struct tm * restrict result);
/*@ requires valid_request: \valid_read(rqtp);
requires
initialized_request: initialization:
......
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