frama-c validation attempt for serializer and deserializer

serializer.c

#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;
}