1 /*
2  * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
3  *
4  * Licensed under the Apache License, Version 2.0 (the "License"). You may not use
5  * this file except in compliance with the License. A copy of the License is
6  * located at
7  *
8  *     http://aws.amazon.com/apache2.0/
9  *
10  * or in the "license" file accompanying this file. This file is distributed on an
11  * "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
12  * implied. See the License for the specific language governing permissions and
13  * limitations under the License.
14  */
15 
16 #undef posix_memalign
17 
18 #include <cbmc_proof/nondet.h>
19 #include <errno.h>
20 #include <stdint.h>
21 
22 /**
23  * Overrides the version of posix_memalign used by CBMC.
24  * The current CBMC model doesn't consider malloc may fail.
25  */
posix_memalign(void ** ptr,__CPROVER_size_t alignment,__CPROVER_size_t size)26 int posix_memalign(void **ptr, __CPROVER_size_t alignment, __CPROVER_size_t size)
27 {
28     __CPROVER_HIDE:;
29 
30     __CPROVER_size_t multiplier = alignment / sizeof(void *);
31     /* Modeling the posix_memalign checks on alignment. */
32     if (alignment % sizeof(void *) != 0 ||
33         ((multiplier) & (multiplier - 1)) != 0 || alignment == 0) {
34       return EINVAL;
35     }
36     void *tmp = malloc(size);
37     if(tmp != NULL) {
38         *ptr = tmp;
39         return 0;
40     }
41     return ENOMEM;
42 }
43