Skip to content

Commit 2a285ee

Browse files
mtzguidomtzguido
committed
Update dist
1 parent adb6e58 commit 2a285ee

13 files changed

Lines changed: 98 additions & 21 deletions

‎krmllib/dist/generic/FStar_BitVector.h‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -71,6 +71,20 @@ extern Prims_list__bool
7171
krml_checked_int_t s
7272
);
7373

74+
extern Prims_list__bool
75+
*FStar_BitVector_rotate_left_vec(
76+
krml_checked_int_t n,
77+
Prims_list__bool *a,
78+
krml_checked_int_t s
79+
);
80+
81+
extern Prims_list__bool
82+
*FStar_BitVector_rotate_right_vec(
83+
krml_checked_int_t n,
84+
Prims_list__bool *a,
85+
krml_checked_int_t s
86+
);
87+
7488

7589
#define FStar_BitVector_H_DEFINED
7690
#endif /* FStar_BitVector_H */

‎krmllib/dist/generic/FStar_Int.h‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -138,6 +138,12 @@ FStar_Int_shift_arithmetic_right(
138138
krml_checked_int_t s
139139
);
140140

141+
extern krml_checked_int_t
142+
FStar_Int_rotate_left(krml_checked_int_t n, krml_checked_int_t a, krml_checked_int_t s);
143+
144+
extern krml_checked_int_t
145+
FStar_Int_rotate_right(krml_checked_int_t n, krml_checked_int_t a, krml_checked_int_t s);
146+
141147

142148
#define FStar_Int_H_DEFINED
143149
#endif /* FStar_Int_H */

‎krmllib/dist/generic/FStar_Int16.h‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,10 @@ extern int16_t FStar_Int16_shift_right(int16_t a, uint32_t s);
5050

5151
extern int16_t FStar_Int16_shift_left(int16_t a, uint32_t s);
5252

53+
extern int16_t FStar_Int16_rotate_right(int16_t a, uint32_t s);
54+
55+
extern int16_t FStar_Int16_rotate_left(int16_t a, uint32_t s);
56+
5357
extern bool FStar_Int16_eq(int16_t a, int16_t b);
5458

5559
extern bool FStar_Int16_ne(int16_t a, int16_t b);

‎krmllib/dist/generic/FStar_Int32.h‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,10 @@ extern int32_t FStar_Int32_shift_right(int32_t a, uint32_t s);
5050

5151
extern int32_t FStar_Int32_shift_left(int32_t a, uint32_t s);
5252

53+
extern int32_t FStar_Int32_rotate_right(int32_t a, uint32_t s);
54+
55+
extern int32_t FStar_Int32_rotate_left(int32_t a, uint32_t s);
56+
5357
extern bool FStar_Int32_eq(int32_t a, int32_t b);
5458

5559
extern bool FStar_Int32_ne(int32_t a, int32_t b);

‎krmllib/dist/generic/FStar_Int64.h‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,10 @@ extern int64_t FStar_Int64_shift_right(int64_t a, uint32_t s);
5050

5151
extern int64_t FStar_Int64_shift_left(int64_t a, uint32_t s);
5252

53+
extern int64_t FStar_Int64_rotate_right(int64_t a, uint32_t s);
54+
55+
extern int64_t FStar_Int64_rotate_left(int64_t a, uint32_t s);
56+
5357
extern bool FStar_Int64_eq(int64_t a, int64_t b);
5458

5559
extern bool FStar_Int64_ne(int64_t a, int64_t b);

‎krmllib/dist/generic/FStar_Int8.h‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,10 @@ extern int8_t FStar_Int8_shift_right(int8_t a, uint32_t s);
5050

5151
extern int8_t FStar_Int8_shift_left(int8_t a, uint32_t s);
5252

53+
extern int8_t FStar_Int8_rotate_right(int8_t a, uint32_t s);
54+
55+
extern int8_t FStar_Int8_rotate_left(int8_t a, uint32_t s);
56+
5357
extern bool FStar_Int8_eq(int8_t a, int8_t b);
5458

5559
extern bool FStar_Int8_ne(int8_t a, int8_t b);

‎krmllib/dist/generic/FStar_Monotonic_Heap.h‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -15,26 +15,26 @@
1515

1616
typedef void *FStar_Monotonic_Heap_tset;
1717

18-
typedef struct FStar_Pervasives_dtuple4_____FStar_Pervasives_Native_option____bool_any_s
18+
typedef struct FStar_Pervasives_dtuple4_____FStar_Pervasives_Native_option_____bool_any_s
1919
{
2020
FStar_Pervasives_Native_option__Prims_string_tags _2;
2121
bool _3;
2222
void *_4;
2323
}
24-
FStar_Pervasives_dtuple4_____FStar_Pervasives_Native_option____bool_any;
24+
FStar_Pervasives_dtuple4_____FStar_Pervasives_Native_option_____bool_any;
2525

2626
typedef struct
27-
FStar_Pervasives_Native_option__FStar_Pervasives_dtuple4____FStar_Pervasives_Native_option____bool_any_s
27+
FStar_Pervasives_Native_option__FStar_Pervasives_dtuple4_____FStar_Pervasives_Native_option_____bool_any_s
2828
{
2929
FStar_Pervasives_Native_option__Prims_string_tags tag;
30-
FStar_Pervasives_dtuple4_____FStar_Pervasives_Native_option____bool_any v;
30+
FStar_Pervasives_dtuple4_____FStar_Pervasives_Native_option_____bool_any v;
3131
}
32-
FStar_Pervasives_Native_option__FStar_Pervasives_dtuple4____FStar_Pervasives_Native_option____bool_any;
32+
FStar_Pervasives_Native_option__FStar_Pervasives_dtuple4_____FStar_Pervasives_Native_option_____bool_any;
3333

3434
typedef struct FStar_Monotonic_Heap_heap_rec_s
3535
{
3636
krml_checked_int_t next_addr;
37-
FStar_Pervasives_Native_option__FStar_Pervasives_dtuple4____FStar_Pervasives_Native_option____bool_any
37+
FStar_Pervasives_Native_option__FStar_Pervasives_dtuple4_____FStar_Pervasives_Native_option_____bool_any
3838
(*memory)(krml_checked_int_t x0);
3939
}
4040
FStar_Monotonic_Heap_heap_rec;

‎krmllib/dist/generic/FStar_UInt.h‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -126,6 +126,12 @@ FStar_UInt_shift_left(krml_checked_int_t n, krml_checked_int_t a, krml_checked_i
126126
extern krml_checked_int_t
127127
FStar_UInt_shift_right(krml_checked_int_t n, krml_checked_int_t a, krml_checked_int_t s);
128128

129+
extern krml_checked_int_t
130+
FStar_UInt_rotate_left(krml_checked_int_t n, krml_checked_int_t a, krml_checked_int_t s);
131+
132+
extern krml_checked_int_t
133+
FStar_UInt_rotate_right(krml_checked_int_t n, krml_checked_int_t a, krml_checked_int_t s);
134+
129135
extern bool FStar_UInt_msb(krml_checked_int_t n, krml_checked_int_t a);
130136

131137
extern Prims_list__bool *FStar_UInt_zero_extend_vec(krml_checked_int_t n, Prims_list__bool *a);

‎krmllib/dist/generic/FStar_UInt_8_16_32_64.h‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,10 @@ extern uint64_t FStar_UInt64_zero;
2828

2929
extern uint64_t FStar_UInt64_one;
3030

31+
extern uint64_t FStar_UInt64_rotate_right(uint64_t a, uint32_t s);
32+
33+
extern uint64_t FStar_UInt64_rotate_left(uint64_t a, uint32_t s);
34+
3135
extern bool FStar_UInt64_ne(uint64_t a, uint64_t b);
3236

3337
extern uint64_t FStar_UInt64_minus(uint64_t a);
@@ -80,6 +84,10 @@ extern uint32_t FStar_UInt32_zero;
8084

8185
extern uint32_t FStar_UInt32_one;
8286

87+
extern uint32_t FStar_UInt32_rotate_right(uint32_t a, uint32_t s);
88+
89+
extern uint32_t FStar_UInt32_rotate_left(uint32_t a, uint32_t s);
90+
8391
extern bool FStar_UInt32_ne(uint32_t a, uint32_t b);
8492

8593
extern uint32_t FStar_UInt32_minus(uint32_t a);
@@ -132,6 +140,10 @@ extern uint16_t FStar_UInt16_zero;
132140

133141
extern uint16_t FStar_UInt16_one;
134142

143+
extern uint16_t FStar_UInt16_rotate_right(uint16_t a, uint32_t s);
144+
145+
extern uint16_t FStar_UInt16_rotate_left(uint16_t a, uint32_t s);
146+
135147
extern bool FStar_UInt16_ne(uint16_t a, uint16_t b);
136148

137149
extern uint16_t FStar_UInt16_minus(uint16_t a);
@@ -184,6 +196,10 @@ extern uint8_t FStar_UInt8_zero;
184196

185197
extern uint8_t FStar_UInt8_one;
186198

199+
extern uint8_t FStar_UInt8_rotate_right(uint8_t a, uint32_t s);
200+
201+
extern uint8_t FStar_UInt8_rotate_left(uint8_t a, uint32_t s);
202+
187203
extern bool FStar_UInt8_ne(uint8_t a, uint8_t b);
188204

189205
extern uint8_t FStar_UInt8_minus(uint8_t a);

‎krmllib/dist/generic/Makefile.basic‎

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -7,11 +7,12 @@
77

88
include Makefile.include
99

10-
ifeq (,$(KRML_HOME))
11-
$(error please define KRML_HOME to point to the root of your KaRaMeL git checkout)
12-
endif
10+
KRML_EXE ?= krml
11+
12+
KRML_INCLUDE != $(KRML_EXE) -locate-include
13+
KRML_LIB != $(KRML_EXE) -locate-krmllib
1314

14-
CFLAGS += -I. -I $(KRML_HOME)/include -I $(KRML_HOME)/krmllib/dist/minimal
15+
CFLAGS += -I. -I $(KRML_INCLUDE) -I $(KRML_LIB)/dist/minimal
1516
CFLAGS += -Wall -Wextra -Werror -std=c11 \
1617
-Wno-unknown-warning-option \
1718
-Wno-infinite-recursion \
@@ -39,7 +40,7 @@ AR ?= ar
3940
$(AR) cr $@ $^
4041

4142
%.exe:
42-
$(CC) $(CFLAGS) -o $@ $^ $(KRML_HOME)/krmllib/dist/generic/libkrmllib.a
43+
$(CC) $(CFLAGS) -o $@ $^ $(KRML_LIB)/dist/generic/libkrmllib.a
4344

4445
%.so:
4546
$(CC) $(CFLAGS) -shared -o $@ $^

0 commit comments

Comments
 (0)