History log of /seL4-camkes-master/tools/cogent/cogent/examples/brutal/brutal.c
Revision Date Author Comments
# 3a2c53ec 23-Aug-2020 Craig McLaughlin <c.mclaughlin@unsw.edu.au>

[Example] Completed Cogent port of Carroll Morgan's minimal example.

Accompanying the Cogent implementation is my rendering of an idiomatic C
implementation (brutal.c) which we strive to produce, as much as
possible, from the Cogent code generator.

As far as the Cogent implementation goes: it utilises a lot of abstract
C functions to hide the pointer arithmetic and address comparisons for
bounds-checking. An additional thorny issue I ran into was translating
the flexible array member into an equivalent form that Cogent could
generate. The Cogent version uses a char pointer which means the number
of Entry structs which fit into the block is smaller since the pointer
takes up some additional space.