Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
frama-c validation attempt for serializer and deserializer
#include <stdlib.h>
#include <stdint.h>
#include <stdbool.h>
#include <stdio.h>
const uint16_t MESSAGE_TYPE_A = 123;
typedef struct {
uint16_t messageType;
} Message;
typedef struct {
Message super;
uint16_t value;
} MessageTypeA;
MessageTypeA staticAlloc[2];
int staticAllocCounter;
MessageTypeA * allocate() {
if (staticAllocCounter > 2) abort();
return &staticAlloc[staticAllocCounter++];
}
MessageTypeA * MessageTypeA_create(uint16_t value) {
//MessageTypeA * evt = malloc(sizeof(MessageTypeA));
MessageTypeA * evt = allocate();
evt->super.messageType = MESSAGE_TYPE_A;
evt->value = value;
return evt;
}
/*@ requires \valid(e);
@ requires \valid(data_out+(0..100));
@*/
void MessageTypeA_serialize(Message const * const e, uint8_t *data_out, size_t *length_out) {
// TODO length in variable
uint8_t * out = data_out;
(*out++) = (uint8_t)(0xFF & (e->messageType >> 8));
(*out++) = (uint8_t)(0xFF & (e->messageType >> 0));
MessageTypeA const * const evt = (MessageTypeA const * const)e;
(*out++) = (uint8_t)(0xFF & (evt->value >> 8));
(*out++) = (uint8_t)(0xFF & (evt->value >> 0));
if (length_out != NULL) *length_out = (out-data_out);
//if (length_out != NULL) *length_out = 0;
}
/*@ requires \valid(data_in+(0..10));
@*/
MessageTypeA * MessageTypeA_deserialize(uint8_t const *data_in, size_t *length_out) {
// TODO length in variable
uint8_t const * in = data_in;
uint16_t msgType = (*in++)<<8;
msgType += (*in++);
// TODO assert message type matches this deserializer
MessageTypeA * evt = allocate();
evt->super.messageType = msgType;
evt->value = (*in++)<<8;
evt->value += (*in++);
if (length_out != NULL) *length_out = (in-data_in);
//if (length_out != NULL) *length_out = 0;
return evt;
}
bool MessageTypeA_equals( MessageTypeA const * const me, Message const * const other) {
if (me->super.messageType != other->messageType) return false;
MessageTypeA * e = ( MessageTypeA *) other;
bool result = (e->value == me->value);
return result;
}
/*@ ensures \result != 0;
@*/
static bool MessageTypeA_test(uint16_t input) {
MessageTypeA * evt = MessageTypeA_create(input);
uint8_t outBuffer[1024];
MessageTypeA_serialize((Message *) evt, outBuffer, NULL);
MessageTypeA * evt2 = MessageTypeA_deserialize(outBuffer, NULL);
bool equal = MessageTypeA_equals(evt, (Message *)evt2);
//free(evt);
//free(evt2);
staticAllocCounter = 0;
return equal;
}
int main(int argc, char **argv) {
uint16_t input = 456;
bool equal = MessageTypeA_test(input);
if (!equal) return 1;
/*for (int i = 0 ; i<= 0xFFFF ; i++) {
if (i % 100 == 0) printf("Testing %d\n", i);
bool equal = MessageTypeA_test((uint16_t)i);
if (!equal) return i;
}*/
return 0;
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment