Commit 1bd019f5 authored by Andreas Werner's avatar Andreas Werner
Browse files

frama-c: add shm proofs

parent 2a8be9c1
Pipeline #9747 passed with stages
in 2 minutes and 55 seconds
......@@ -15,11 +15,22 @@ union conv {
float f;
};
/*@
requires \valid(base);
ensures shm1.base == base;
ensures \valid(\result);
*/
struct shm *shm_init(uint8_t *base) {
shm1.base = base;
return &shm1;
}
/*@
requires \valid(shm) && \valid(shm->base);
requires \valid(data);
requires \valid((uint32_t *) (shm->base + offset));
ensures *data == *((uint32_t *)(shm->base + offset));
*/
int32_t shm_read32(struct shm *shm, uint32_t offset, uint32_t *data) {
uint32_t *reg = (uint32_t *) (shm->base + offset);
*data = *reg;
......@@ -27,6 +38,11 @@ int32_t shm_read32(struct shm *shm, uint32_t offset, uint32_t *data) {
return 0;
}
/*@
requires \valid(shm) && \valid(shm->base);
requires \valid((uint32_t *) (shm->base + offset));
ensures *((uint32_t *)(shm->base + offset)) == data;
*/
int32_t shm_write32(struct shm *shm, uint32_t offset, uint32_t data) {
uint32_t *reg = (uint32_t *) (shm->base + offset);
PRINTF("write: %p %lu\n", reg, data);
......@@ -34,6 +50,12 @@ int32_t shm_write32(struct shm *shm, uint32_t offset, uint32_t data) {
return 0;
}
/*@
requires \valid(shm) && \valid(shm->base);
requires \valid(data);
requires \valid((float *) (shm->base + offset));
ensures *data == *(((float *)(shm->base + offset)));
*/
int32_t shm_readFloat(struct shm *shm, uint32_t offset, float *data) {
union conv c;
shm_read32(shm, offset, &c.i);
......@@ -41,6 +63,11 @@ int32_t shm_readFloat(struct shm *shm, uint32_t offset, float *data) {
return 0;
}
/*@
requires \valid(shm) && \valid(shm->base);
requires \valid((float *) (shm->base + offset));
ensures *(((float *)(shm->base + offset))) == data;
*/
int32_t shm_writeFloat(struct shm *shm, uint32_t offset, float data) {
union conv c;
c.f = data;
......@@ -48,6 +75,14 @@ int32_t shm_writeFloat(struct shm *shm, uint32_t offset, float data) {
return 0;
}
#ifdef __FRAMAC__
extern TickType_t ticksSinceStart;
#endif
/*@
requires \valid(shm) && \valid(shm->base);
requires \valid((uint32_t *) (shm->base + offset));
ensures *((uint32_t *)(shm->base + offset)) == ticksSinceStart;
*/
int32_t shm_updateTime(struct shm *shm, uint32_t offset) {
TickType_t time = xTaskGetTickCount();
return shm_write32(shm, offset, time);
......
Supports Markdown
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