From ab11d8fff2d18b805cd404fd6a05ea7236d5012a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 4 Aug 2021 17:18:13 -0700 Subject: [PATCH] include paths Signed-off-by: Nikolaj Bjorner --- src/math/bigfix/{kremlib => }/FStar_UInt128_Verified.h | 0 src/math/bigfix/{kremlib => }/FStar_UInt_8_16_32_64.h | 6 +++--- src/math/bigfix/Hacl_Bignum.h | 10 +++++----- src/math/bigfix/Hacl_Bignum256.h | 6 +++--- src/math/bigfix/Hacl_Bignum_Base.h | 6 +++--- src/math/bigfix/Hacl_IntTypes_Intrinsics.h | 6 +++--- .../{kremlib/FStar_UInt128.h => fstar_uint128.h} | 6 +++--- src/math/bigfix/{kremlib => }/fstar_uint128_gcc64.h | 0 src/math/bigfix/{kremlib => }/fstar_uint128_msvc.h | 6 +++--- .../{kremlib => }/fstar_uint128_struct_endianness.h | 0 src/math/bigfix/{kremlin => }/lowstar_endianness.h | 0 src/math/bigfix/{kremlin/internal => }/target.h | 0 src/math/bigfix/{kremlin/internal => }/types.h | 10 +++++----- 13 files changed, 28 insertions(+), 28 deletions(-) rename src/math/bigfix/{kremlib => }/FStar_UInt128_Verified.h (100%) rename src/math/bigfix/{kremlib => }/FStar_UInt_8_16_32_64.h (94%) rename src/math/bigfix/{kremlib/FStar_UInt128.h => fstar_uint128.h} (94%) rename src/math/bigfix/{kremlib => }/fstar_uint128_gcc64.h (100%) rename src/math/bigfix/{kremlib => }/fstar_uint128_msvc.h (99%) rename src/math/bigfix/{kremlib => }/fstar_uint128_struct_endianness.h (100%) rename src/math/bigfix/{kremlin => }/lowstar_endianness.h (100%) rename src/math/bigfix/{kremlin/internal => }/target.h (100%) rename src/math/bigfix/{kremlin/internal => }/types.h (88%) diff --git a/src/math/bigfix/kremlib/FStar_UInt128_Verified.h b/src/math/bigfix/FStar_UInt128_Verified.h similarity index 100% rename from src/math/bigfix/kremlib/FStar_UInt128_Verified.h rename to src/math/bigfix/FStar_UInt128_Verified.h diff --git a/src/math/bigfix/kremlib/FStar_UInt_8_16_32_64.h b/src/math/bigfix/FStar_UInt_8_16_32_64.h similarity index 94% rename from src/math/bigfix/kremlib/FStar_UInt_8_16_32_64.h rename to src/math/bigfix/FStar_UInt_8_16_32_64.h index 12626858e..6f7bbc448 100644 --- a/src/math/bigfix/kremlib/FStar_UInt_8_16_32_64.h +++ b/src/math/bigfix/FStar_UInt_8_16_32_64.h @@ -8,9 +8,9 @@ #define __FStar_UInt_8_16_32_64_H #include #include -#include "math/bigfix/kremlin/lowstar_endianness.h" -#include "math/bigfix/kremlin/internal/types.h" -#include "math/bigfix/kremlin/internal/target.h" +#include "math/bigfix/lowstar_endianness.h" +#include "math/bigfix/types.h" +#include "math/bigfix/target.h" static inline uint64_t FStar_UInt64_eq_mask(uint64_t a, uint64_t b) { diff --git a/src/math/bigfix/Hacl_Bignum.h b/src/math/bigfix/Hacl_Bignum.h index e9f204d1a..453312856 100644 --- a/src/math/bigfix/Hacl_Bignum.h +++ b/src/math/bigfix/Hacl_Bignum.h @@ -29,13 +29,13 @@ extern "C" { #endif -#include "lib_intrinsics.h" -#include "kremlin/internal/types.h" -#include "kremlin/lowstar_endianness.h" +#include "math/bigfix/lib_intrinsics.h" +#include "math/bigfix/types.h" +#include "math/bigfix/lowstar_endianness.h" #include -#include "kremlin/internal/target.h" +#include "math/bigfix/target.h" -#include "Hacl_Bignum_Base.h" +#include "math/bigfix/Hacl_Bignum_Base.h" void Hacl_Bignum_Convert_bn_from_bytes_be_uint64(uint32_t len, uint8_t *b, uint64_t *res); diff --git a/src/math/bigfix/Hacl_Bignum256.h b/src/math/bigfix/Hacl_Bignum256.h index 032720eff..1d092a3b4 100644 --- a/src/math/bigfix/Hacl_Bignum256.h +++ b/src/math/bigfix/Hacl_Bignum256.h @@ -29,10 +29,10 @@ extern "C" { #endif -#include "math/bigfix/kremlin/internal/types.h" -#include "math/bigfix/kremlin/lowstar_endianness.h" +#include "math/bigfix/types.h" +#include "math/bigfix/lowstar_endianness.h" #include -#include "math/bigfix/kremlin/internal/target.h" +#include "math/bigfix/target.h" #include "math/bigfix/Hacl_Bignum.h" #include "math/bigfix/Hacl_Bignum_Base.h" diff --git a/src/math/bigfix/Hacl_Bignum_Base.h b/src/math/bigfix/Hacl_Bignum_Base.h index f22c22392..acae212ec 100644 --- a/src/math/bigfix/Hacl_Bignum_Base.h +++ b/src/math/bigfix/Hacl_Bignum_Base.h @@ -29,10 +29,10 @@ extern "C" { #endif -#include "kremlin/internal/types.h" -#include "kremlin/lowstar_endianness.h" +#include "math/bigfix/types.h" +#include "math/bigfix/lowstar_endianness.h" #include -#include "kremlin/internal/target.h" +#include "math/bigfix/target.h" static inline uint64_t Hacl_Bignum_Base_mul_wide_add_u64(uint64_t a, uint64_t b, uint64_t c_in, uint64_t *out) diff --git a/src/math/bigfix/Hacl_IntTypes_Intrinsics.h b/src/math/bigfix/Hacl_IntTypes_Intrinsics.h index 5faf4eddf..68bbfbef1 100644 --- a/src/math/bigfix/Hacl_IntTypes_Intrinsics.h +++ b/src/math/bigfix/Hacl_IntTypes_Intrinsics.h @@ -29,10 +29,10 @@ extern "C" { #endif -#include "kremlin/internal/types.h" -#include "kremlin/lowstar_endianness.h" +#include "math/bigfix/types.h" +#include "math/bigfix/lowstar_endianness.h" #include -#include "kremlin/internal/target.h" +#include "math/bigfix/target.h" static inline uint32_t Hacl_IntTypes_Intrinsics_add_carry_u32(uint32_t cin, uint32_t x, uint32_t y, uint32_t *r) diff --git a/src/math/bigfix/kremlib/FStar_UInt128.h b/src/math/bigfix/fstar_uint128.h similarity index 94% rename from src/math/bigfix/kremlib/FStar_UInt128.h rename to src/math/bigfix/fstar_uint128.h index 570832839..67d6a6070 100644 --- a/src/math/bigfix/kremlib/FStar_UInt128.h +++ b/src/math/bigfix/fstar_uint128.h @@ -8,9 +8,9 @@ #define __FStar_UInt128_H #include #include -#include "math/bigfix/kremlin/lowstar_endianness.h" -#include "math/bigfix/kremlin/internal/types.h" -#include "math/bigfix/kremlin/internal/target.h" +#include "math/bigfix/lowstar_endianness.h" +#include "math/bigfix/types.h" +#include "math/bigfix/target.h" diff --git a/src/math/bigfix/kremlib/fstar_uint128_gcc64.h b/src/math/bigfix/fstar_uint128_gcc64.h similarity index 100% rename from src/math/bigfix/kremlib/fstar_uint128_gcc64.h rename to src/math/bigfix/fstar_uint128_gcc64.h diff --git a/src/math/bigfix/kremlib/fstar_uint128_msvc.h b/src/math/bigfix/fstar_uint128_msvc.h similarity index 99% rename from src/math/bigfix/kremlib/fstar_uint128_msvc.h rename to src/math/bigfix/fstar_uint128_msvc.h index aa4f4c262..e8b5c390d 100644 --- a/src/math/bigfix/kremlib/fstar_uint128_msvc.h +++ b/src/math/bigfix/fstar_uint128_msvc.h @@ -11,9 +11,9 @@ #ifndef FSTAR_UINT128_MSVC #define FSTAR_UINT128_MSVC -#include "math/bigfix/kremlin/internal/types.h" -#include "math/bigfix/kremlib/FStar_UInt128.h" -#include "math/bigfix/kremlib/FStar_UInt_8_16_32_64.h" +#include "math/bigfix/types.h" +#include "math/bigfix/FStar_UInt128.h" +#include "math/bigfix/FStar_UInt_8_16_32_64.h" #ifndef _MSC_VER # error This file only works with the MSVC compiler diff --git a/src/math/bigfix/kremlib/fstar_uint128_struct_endianness.h b/src/math/bigfix/fstar_uint128_struct_endianness.h similarity index 100% rename from src/math/bigfix/kremlib/fstar_uint128_struct_endianness.h rename to src/math/bigfix/fstar_uint128_struct_endianness.h diff --git a/src/math/bigfix/kremlin/lowstar_endianness.h b/src/math/bigfix/lowstar_endianness.h similarity index 100% rename from src/math/bigfix/kremlin/lowstar_endianness.h rename to src/math/bigfix/lowstar_endianness.h diff --git a/src/math/bigfix/kremlin/internal/target.h b/src/math/bigfix/target.h similarity index 100% rename from src/math/bigfix/kremlin/internal/target.h rename to src/math/bigfix/target.h diff --git a/src/math/bigfix/kremlin/internal/types.h b/src/math/bigfix/types.h similarity index 88% rename from src/math/bigfix/kremlin/internal/types.h rename to src/math/bigfix/types.h index 885d956c4..c1bd7a56e 100644 --- a/src/math/bigfix/kremlin/internal/types.h +++ b/src/math/bigfix/types.h @@ -50,7 +50,7 @@ typedef struct FStar_UInt128_uint128_s { * latter is for internal use. */ typedef FStar_UInt128_uint128 FStar_UInt128_t, uint128_t; -#include "math/bigfix/kremlin/lowstar_endianness.h" +#include "math/bigfix/lowstar_endianness.h" #endif @@ -59,12 +59,12 @@ typedef FStar_UInt128_uint128 FStar_UInt128_t, uint128_t; #ifndef __FStar_UInt_8_16_32_64_H #if !defined(KRML_VERIFIED_UINT128) && defined(IS_MSVC64) -#include "math/bigfix/kremlib/fstar_uint128_msvc.h" +#include "math/bigfix/fstar_uint128_msvc.h" #elif !defined(KRML_VERIFIED_UINT128) && defined(HAS_INT128) -#include "math/bigfix/kremlib/fstar_uint128_gcc64.h" +#include "math/bigfix/fstar_uint128_gcc64.h" #else -#include "math/bigfix/kremlib/FStar_UInt128_Verified.h" -#include "math/bigfix/kremlib/fstar_uint128_struct_endianness.h" +#include "math/bigfix/FStar_UInt128_Verified.h" +#include "math/bigfix/fstar_uint128_struct_endianness.h" #endif #endif