summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2020-08-08 12:31:46 +0200
committerChristophe Grenier <grenier@cgsecurity.org>2020-08-08 12:31:46 +0200
commit8587bc1ddbcd3b0810e99c08e14b05d165668b11 (patch)
tree18290f07516c0df67ccf11876a189afea3e7c132
parentd19e5362783d2c1dbc3b6cdf3adde5703cc54176 (diff)
src/hdcache.c: add frama-c annotations
-rw-r--r--src/hdcache.c91
1 files changed, 66 insertions, 25 deletions
diff --git a/src/hdcache.c b/src/hdcache.c
index c7ae0ab..e2bc862 100644
--- a/src/hdcache.c
+++ b/src/hdcache.c
@@ -62,20 +62,16 @@ struct cache_struct
unsigned int last_io_error_nbr;
};
-static int cache_pread_aux(disk_t *disk_car, void *buffer, const unsigned int count, const uint64_t offset, const unsigned int read_ahead);
static int cache_pread(disk_t *disk_car, void *buffer, const unsigned int count, const uint64_t offset);
static int cache_pwrite(disk_t *disk_car, const void *buffer, const unsigned int count, const uint64_t offset);
static int cache_sync(disk_t *disk);
static void cache_clean(disk_t *disk);
-static const char *cache_description(disk_t *disk_car);
-static const char *cache_description_short(disk_t *disk_car);
-
-static int cache_pread(disk_t *disk_car, void *buffer, const unsigned int count, const uint64_t offset)
-{
- const struct cache_struct *data=(const struct cache_struct *)disk_car->data;
- return cache_pread_aux(disk_car, buffer, count, offset, (data->last_io_error_nbr==0));
-}
+/*@
+ @ requires \valid(disk_car);
+ @ requires \valid((char *)buffer + (0 .. count-1));
+ @ requires separation: \separated(disk_car, (char *)buffer + (0 .. count-1));
+ @*/
static int cache_pread_aux(disk_t *disk_car, void *buffer, const unsigned int count, const uint64_t offset, const unsigned int read_ahead)
{
struct cache_struct *data=(struct cache_struct *)disk_car->data;
@@ -184,6 +180,22 @@ static int cache_pread_aux(disk_t *disk_car, void *buffer, const unsigned int co
}
}
+/*@
+ @ requires \valid(disk_car);
+ @ requires \valid((char *)buffer + (0 .. count-1));
+ @ requires separation: \separated(disk_car, (char *)buffer + (0 .. count-1));
+ @*/
+static int cache_pread(disk_t *disk_car, void *buffer, const unsigned int count, const uint64_t offset)
+{
+ const struct cache_struct *data=(const struct cache_struct *)disk_car->data;
+ return cache_pread_aux(disk_car, buffer, count, offset, (data->last_io_error_nbr==0));
+}
+
+/*@
+ @ requires \valid(disk_car);
+ @ requires \valid_read((char *)buffer + (0 .. count-1));
+ @ requires separation: \separated(disk_car, (const char *)buffer + (0 .. count-1));
+ @*/
static int cache_pwrite(disk_t *disk_car, const void *buffer, const unsigned int count, const uint64_t offset)
{
struct cache_struct *data=(struct cache_struct *)disk_car->data;
@@ -201,6 +213,9 @@ static int cache_pwrite(disk_t *disk_car, const void *buffer, const unsigned int
return data->disk_car->pwrite(data->disk_car, buffer, count, offset);
}
+/*@
+ @ requires \valid(disk_car);
+ @*/
static void cache_clean(disk_t *disk_car)
{
if(disk_car->data)
@@ -225,12 +240,24 @@ static void cache_clean(disk_t *disk_car)
free(disk_car);
}
+/*@
+ @ requires \valid(disk_car);
+ @*/
static int cache_sync(disk_t *disk_car)
{
struct cache_struct *data=(struct cache_struct *)disk_car->data;
return data->disk_car->sync(data->disk_car);
}
+/*@
+ @ requires \valid_read(CHS_source);
+ @ requires \valid(CHS_dst);
+ @ requires separation: \separated(CHS_dst, CHS_source);
+ @ assigns CHS_dst->cylinders, CHS_dst->heads_per_cylinder, CHS_dst->sectors_per_head;
+ @ ensures CHS_dst->cylinders==CHS_source->cylinders;
+ @ ensures CHS_dst->heads_per_cylinder==CHS_source->heads_per_cylinder;
+ @ ensures CHS_dst->sectors_per_head==CHS_source->sectors_per_head;
+ @*/
static void dup_geometry(CHSgeometry_t * CHS_dst, const CHSgeometry_t * CHS_source)
{
CHS_dst->cylinders=CHS_source->cylinders;
@@ -238,6 +265,36 @@ static void dup_geometry(CHSgeometry_t * CHS_dst, const CHSgeometry_t * CHS_sour
CHS_dst->sectors_per_head=CHS_source->sectors_per_head;
}
+/*@
+ @ requires \valid(disk_car);
+ @ ensures valid_read_string(\result);
+ @*/
+static const char *cache_description(disk_t *disk_car)
+{
+ const char *tmp;
+ struct cache_struct *data=(struct cache_struct *)disk_car->data;
+ dup_geometry(&data->disk_car->geom,&disk_car->geom);
+ data->disk_car->disk_size=disk_car->disk_size;
+ tmp=data->disk_car->description(data->disk_car);
+ /*@ assert valid_read_string(tmp); */
+ return tmp;
+}
+
+/*@
+ @ requires \valid(disk_car);
+ @ ensures valid_read_string(\result);
+ @*/
+static const char *cache_description_short(disk_t *disk_car)
+{
+ const char *tmp;
+ struct cache_struct *data=(struct cache_struct *)disk_car->data;
+ dup_geometry(&data->disk_car->geom,&disk_car->geom);
+ data->disk_car->disk_size=disk_car->disk_size;
+ tmp=data->disk_car->description_short(data->disk_car);
+ /*@ assert valid_read_string(tmp); */
+ return tmp;
+}
+
disk_t *new_diskcache(disk_t *disk_car, const unsigned int testdisk_mode)
{
unsigned int i;
@@ -281,19 +338,3 @@ disk_t *new_diskcache(disk_t *disk_car, const unsigned int testdisk_mode)
}
return new_disk_car;
}
-
-static const char *cache_description(disk_t *disk_car)
-{
- struct cache_struct *data=(struct cache_struct *)disk_car->data;
- dup_geometry(&data->disk_car->geom,&disk_car->geom);
- data->disk_car->disk_size=disk_car->disk_size;
- return data->disk_car->description(data->disk_car);
-}
-
-static const char *cache_description_short(disk_t *disk_car)
-{
- struct cache_struct *data=(struct cache_struct *)disk_car->data;
- dup_geometry(&data->disk_car->geom,&disk_car->geom);
- data->disk_car->disk_size=disk_car->disk_size;
- return data->disk_car->description_short(data->disk_car);
-}