summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2019-10-12 17:01:26 +0200
committerChristophe Grenier <grenier@cgsecurity.org>2019-10-12 17:01:26 +0200
commit0004d616726747770bf18a9df9234dea6bcbe6da (patch)
tree4ddc8bdabf9d8d9721f474b7e189fec5ac2357ae
parentc315a2a6a73e8dcea9f14485082c2ad7e9118ceb (diff)
src/common.c: add frama-c annotations for MALLOC()
-rw-r--r--src/common.c4
-rw-r--r--src/common.h6
2 files changed, 8 insertions, 2 deletions
diff --git a/src/common.c b/src/common.c
index 3b1f45b..1cb866a 100644
--- a/src/common.c
+++ b/src/common.c
@@ -61,7 +61,7 @@ void *MALLOC(size_t size)
/* Warning, memory leak checker must be posix_memalign/memalign aware, otherwise *
* reports may look strange. Aligned memory is required if the buffer is *
* used for read/write operation with a file opened with O_DIRECT */
-#if defined(HAVE_POSIX_MEMALIGN)
+#if defined(HAVE_POSIX_MEMALIGN) && !defined(__FRAMAC__)
if(size>=512)
{
if(posix_memalign(&res,4096,size)==0)
@@ -70,7 +70,7 @@ void *MALLOC(size_t size)
return res;
}
}
-#elif defined(HAVE_MEMALIGN)
+#elif defined(HAVE_MEMALIGN) && !defined(__FRAMAC__)
if(size>=512)
{
if((res=memalign(4096, size))!=NULL)
diff --git a/src/common.h b/src/common.h
index 67645f5..46e9d7f 100644
--- a/src/common.h
+++ b/src/common.h
@@ -438,7 +438,13 @@ struct my_data_struct
uint64_t offset;
};
+/*@
+ @ requires size > 0;
+ @ ensures \valid(((char *)\result)+(0..size-1));
+ @ ensures zero_initialization: \subset(((char *)\result)[0..size-1], {0});
+ @*/
void *MALLOC(size_t size);
+
unsigned int up2power(const unsigned int number);
void set_part_name(partition_t *partition, const char *src, const unsigned int max_size);
void set_part_name_chomp(partition_t *partition, const unsigned char *src, const unsigned int max_size);