This directory contains code generated by Fiat and thus these files are licensed under the MIT license. (See LICENSE file.)
The files are imported from the fiat-c/src directory of the Fiat repository.
Their contents are #included into source files, so we rename them to .h.