Skip to content

make cases for lowstar_endianness consistent#252

Open
franziskuskiefer wants to merge 3 commits into
masterfrom
franziskus/fix-path-cases
Open

make cases for lowstar_endianness consistent#252
franziskuskiefer wants to merge 3 commits into
masterfrom
franziskus/fix-path-cases

Conversation

@franziskuskiefer
Copy link
Copy Markdown
Member

I don't mind which version to use but the warnings about this are annoying, let's decide on a casing.

@msprotz
Copy link
Copy Markdown
Contributor

msprotz commented Apr 14, 2022

PascalCase = kremlin-generated file
snake_case = hand-written

there are two such files: the snake_case one is in include/kremlin, the PascalCase one is in dist/generic/*

The correct fix is probably to rename the snake_case one to something more meaningful, such as lowstar_endianness_builtins.h to indicate that it contains hand-written prototypes that "fill out" the endianness functions on a per-platform basis.

The auto-generated one contains function prototypes to be implemented by hand and allows making sure that the implementation of e.g. load128_le (in kremlib/c/fstar_uint128_gcc64.h) is correct with regards to what is claimed in the F* file (as extracted in kremlib/dist/generic/LowStar_Endianness.h).

Hope this makes sense!

Copy link
Copy Markdown
Contributor

@msprotz msprotz left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is good, thanks. The files you modified are for a large part auto-generated or copied from another directory. Can you modify the source files in krmllib/c/{fstar_uint128*.h} rather? Then I can take care of refreshing dist after that and check that it's alright. Thanks!


#include "FStar_UInt128.h"
#include "FStar_UInt_8_16_32_64.h"
#include "lowstar_endianness.h"
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this one seems wrong

Comment thread krmllib/dist/minimal/Makefile.include Outdated
USER_CFLAGS=
USER_C_FILES=fstar_uint128.c
ALL_C_FILES=
ALL_H_FILES=FStar_UInt128.h FStar_UInt_8_16_32_64.h lowstar_endianness.h
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

same here should be the builtin one


#include "FStar_UInt128.h"
#include "FStar_UInt_8_16_32_64.h"
#include "lowstar_endianness.h"
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

same

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants