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)26int 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