Re: [isabelle] [ExternalEmail] Proof of concept: BNF-based records



No sure what happened to the quoting in my email client, sorry. This is the relevant part:


> Can you point to the sources of a few such big record definitions?

They get produced by the C parser, e.g. at this call:

https://github.com/seL4/l4v/blob/3d225cde694ba60a/spec/cspec/X64/Kernel_C.thy#L78

The record becomes large, because Norbert's SIMPL framework expects one record field per local variable in the union of all functions of the program. The final state record is an extension of a default state record + these local variables.

We could synthesise a manual definition that simulates this situation if it helps.

Cheers,
Gerwin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.