Skip to content

Commit 6942429

Browse files
gebnergebner
committed
Fix tests.
1 parent 99ba102 commit 6942429

File tree

2 files changed

+25
-25
lines changed

2 files changed

+25
-25
lines changed

‎test/Example_Hashtable.c.expected‎

Lines changed: 19 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -97,14 +97,14 @@ typedef struct option__size_t_s
9797
option__size_t;
9898

9999
typedef struct
100-
__Pulse_Lib_HashTable_Type_ht_t_size_t_Example_Hashtable_data_FStar_Pervasives_Native_option_size_t_s
100+
__Pulse_Lib_HashTable_Type_ht_t__size_t_Example_Hashtable_data_FStar_Pervasives_Native_option__size_t_s
101101
{
102102
ht_t__size_t_Example_Hashtable_data fst;
103103
option__size_t snd;
104104
}
105-
__Pulse_Lib_HashTable_Type_ht_t_size_t_Example_Hashtable_data_FStar_Pervasives_Native_option_size_t;
105+
__Pulse_Lib_HashTable_Type_ht_t__size_t_Example_Hashtable_data_FStar_Pervasives_Native_option__size_t;
106106

107-
static __Pulse_Lib_HashTable_Type_ht_t_size_t_Example_Hashtable_data_FStar_Pervasives_Native_option_size_t
107+
static __Pulse_Lib_HashTable_Type_ht_t__size_t_Example_Hashtable_data_FStar_Pervasives_Native_option__size_t
108108
lookup__size_t_Example_Hashtable_data(ht_t__size_t_Example_Hashtable_data ht, size_t k)
109109
{
110110
size_t (*hashf)(size_t x0) = ht.hashf;
@@ -183,7 +183,7 @@ lookup__size_t_Example_Hashtable_data(ht_t__size_t_Example_Hashtable_data ht, si
183183
ht1 = mk_ht__size_t_Example_Hashtable_data(ht.sz, ht.hashf, vcontents);
184184
return
185185
(
186-
(__Pulse_Lib_HashTable_Type_ht_t_size_t_Example_Hashtable_data_FStar_Pervasives_Native_option_size_t){
186+
(__Pulse_Lib_HashTable_Type_ht_t__size_t_Example_Hashtable_data_FStar_Pervasives_Native_option__size_t){
187187
.fst = ht1,
188188
.snd = o
189189
}
@@ -192,7 +192,7 @@ lookup__size_t_Example_Hashtable_data(ht_t__size_t_Example_Hashtable_data ht, si
192192

193193
static ht_t__size_t_Example_Hashtable_data
194194
fst__Pulse_Lib_HashTable_Type_ht_t_size_t_Example_Hashtable_data_FStar_Pervasives_Native_option_size_t(
195-
__Pulse_Lib_HashTable_Type_ht_t_size_t_Example_Hashtable_data_FStar_Pervasives_Native_option_size_t
195+
__Pulse_Lib_HashTable_Type_ht_t__size_t_Example_Hashtable_data_FStar_Pervasives_Native_option__size_t
196196
x
197197
)
198198
{
@@ -201,7 +201,7 @@ fst__Pulse_Lib_HashTable_Type_ht_t_size_t_Example_Hashtable_data_FStar_Pervasive
201201

202202
static option__size_t
203203
snd__Pulse_Lib_HashTable_Type_ht_t_size_t_Example_Hashtable_data_FStar_Pervasives_Native_option_size_t(
204-
__Pulse_Lib_HashTable_Type_ht_t_size_t_Example_Hashtable_data_FStar_Pervasives_Native_option_size_t
204+
__Pulse_Lib_HashTable_Type_ht_t__size_t_Example_Hashtable_data_FStar_Pervasives_Native_option__size_t
205205
x
206206
)
207207
{
@@ -214,14 +214,14 @@ mk_used_cell__size_t_Example_Hashtable_data(size_t k, Example_Hashtable_data v)
214214
return ((cell__size_t_Example_Hashtable_data){ .tag = Used, .k = k, .v = v });
215215
}
216216

217-
typedef struct __Pulse_Lib_HashTable_Type_ht_t_size_t_Example_Hashtable_data_bool_s
217+
typedef struct __Pulse_Lib_HashTable_Type_ht_t__size_t_Example_Hashtable_data_bool_s
218218
{
219219
ht_t__size_t_Example_Hashtable_data fst;
220220
bool snd;
221221
}
222-
__Pulse_Lib_HashTable_Type_ht_t_size_t_Example_Hashtable_data_bool;
222+
__Pulse_Lib_HashTable_Type_ht_t__size_t_Example_Hashtable_data_bool;
223223

224-
static __Pulse_Lib_HashTable_Type_ht_t_size_t_Example_Hashtable_data_bool
224+
static __Pulse_Lib_HashTable_Type_ht_t__size_t_Example_Hashtable_data_bool
225225
insert__size_t_Example_Hashtable_data(
226226
ht_t__size_t_Example_Hashtable_data ht,
227227
size_t k,
@@ -287,7 +287,7 @@ insert__size_t_Example_Hashtable_data(
287287
cell__size_t_Example_Hashtable_data *vcontents = contents;
288288
ht_t__size_t_Example_Hashtable_data
289289
ht1 = { .sz = ht.sz, .hashf = hashf, .contents = vcontents };
290-
__Pulse_Lib_HashTable_Type_ht_t_size_t_Example_Hashtable_data_FStar_Pervasives_Native_option_size_t
290+
__Pulse_Lib_HashTable_Type_ht_t__size_t_Example_Hashtable_data_FStar_Pervasives_Native_option__size_t
291291
res = lookup__size_t_Example_Hashtable_data(ht1, k);
292292
contents =
293293
fst__Pulse_Lib_HashTable_Type_ht_t_size_t_Example_Hashtable_data_FStar_Pervasives_Native_option_size_t(res).contents;
@@ -339,7 +339,7 @@ insert__size_t_Example_Hashtable_data(
339339
ht1 = mk_ht__size_t_Example_Hashtable_data(ht.sz, hashf, vcontents);
340340
return
341341
(
342-
(__Pulse_Lib_HashTable_Type_ht_t_size_t_Example_Hashtable_data_bool){
342+
(__Pulse_Lib_HashTable_Type_ht_t__size_t_Example_Hashtable_data_bool){
343343
.fst = ht1,
344344
.snd = true
345345
}
@@ -352,7 +352,7 @@ insert__size_t_Example_Hashtable_data(
352352
ht1 = mk_ht__size_t_Example_Hashtable_data(ht.sz, hashf, vcontents);
353353
return
354354
(
355-
(__Pulse_Lib_HashTable_Type_ht_t_size_t_Example_Hashtable_data_bool){
355+
(__Pulse_Lib_HashTable_Type_ht_t__size_t_Example_Hashtable_data_bool){
356356
.fst = ht1,
357357
.snd = false
358358
}
@@ -361,14 +361,14 @@ insert__size_t_Example_Hashtable_data(
361361
}
362362

363363
typedef struct
364-
__Pulse_Lib_HashTable_Type_ht_t_size_t_Example_Hashtable_data_Example_Hashtable_data_s
364+
__Pulse_Lib_HashTable_Type_ht_t__size_t_Example_Hashtable_data_Example_Hashtable_data_s
365365
{
366366
ht_t__size_t_Example_Hashtable_data fst;
367367
Example_Hashtable_data snd;
368368
}
369-
__Pulse_Lib_HashTable_Type_ht_t_size_t_Example_Hashtable_data_Example_Hashtable_data;
369+
__Pulse_Lib_HashTable_Type_ht_t__size_t_Example_Hashtable_data_Example_Hashtable_data;
370370

371-
static __Pulse_Lib_HashTable_Type_ht_t_size_t_Example_Hashtable_data_Example_Hashtable_data
371+
static __Pulse_Lib_HashTable_Type_ht_t__size_t_Example_Hashtable_data_Example_Hashtable_data
372372
replace__size_t_Example_Hashtable_data(
373373
ht_t__size_t_Example_Hashtable_data ht,
374374
size_t idx,
@@ -391,7 +391,7 @@ replace__size_t_Example_Hashtable_data(
391391
Example_Hashtable_data v_1 = v_.v;
392392
return
393393
(
394-
(__Pulse_Lib_HashTable_Type_ht_t_size_t_Example_Hashtable_data_Example_Hashtable_data){
394+
(__Pulse_Lib_HashTable_Type_ht_t__size_t_Example_Hashtable_data_Example_Hashtable_data){
395395
.fst = ht1,
396396
.snd = v_1
397397
}
@@ -432,20 +432,20 @@ void Example_Hashtable_insert_lookup_and_replace(void)
432432
{
433433
ht_t__size_t_Example_Hashtable_data
434434
h = alloc__size_t_Example_Hashtable_data(Example_Hashtable_hash, (size_t)100U);
435-
__Pulse_Lib_HashTable_Type_ht_t_size_t_Example_Hashtable_data_bool
435+
__Pulse_Lib_HashTable_Type_ht_t__size_t_Example_Hashtable_data_bool
436436
_letpattern =
437437
insert__size_t_Example_Hashtable_data(h,
438438
(size_t)1U,
439439
((Example_Hashtable_data){ .left = true, .right = false }));
440440
ht_t__size_t_Example_Hashtable_data h1 = _letpattern.fst;
441-
__Pulse_Lib_HashTable_Type_ht_t_size_t_Example_Hashtable_data_FStar_Pervasives_Native_option_size_t
441+
__Pulse_Lib_HashTable_Type_ht_t__size_t_Example_Hashtable_data_FStar_Pervasives_Native_option__size_t
442442
_letpattern1 = lookup__size_t_Example_Hashtable_data(h1, (size_t)1U);
443443
ht_t__size_t_Example_Hashtable_data h2 = _letpattern1.fst;
444444
option__size_t found = _letpattern1.snd;
445445
if (found.tag == Some)
446446
{
447447
size_t i = found.v;
448-
__Pulse_Lib_HashTable_Type_ht_t_size_t_Example_Hashtable_data_Example_Hashtable_data
448+
__Pulse_Lib_HashTable_Type_ht_t__size_t_Example_Hashtable_data_Example_Hashtable_data
449449
_letpattern2 =
450450
replace__size_t_Example_Hashtable_data(h2,
451451
i,

‎test/Example_Slice.c.expected‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -16,21 +16,21 @@ static slice__uint8_t from_array__uint8_t(uint8_t *a, size_t alen)
1616
return ((slice__uint8_t){ .elt = ptr, .len = alen });
1717
}
1818

19-
typedef struct __Pulse_Lib_Slice_slice_uint8_t_Pulse_Lib_Slice_slice_uint8_t_s
19+
typedef struct __Pulse_Lib_Slice_slice__uint8_t_Pulse_Lib_Slice_slice__uint8_t_s
2020
{
2121
slice__uint8_t fst;
2222
slice__uint8_t snd;
2323
}
24-
__Pulse_Lib_Slice_slice_uint8_t_Pulse_Lib_Slice_slice_uint8_t;
24+
__Pulse_Lib_Slice_slice__uint8_t_Pulse_Lib_Slice_slice__uint8_t;
2525

26-
static __Pulse_Lib_Slice_slice_uint8_t_Pulse_Lib_Slice_slice_uint8_t
26+
static __Pulse_Lib_Slice_slice__uint8_t_Pulse_Lib_Slice_slice__uint8_t
2727
split__uint8_t(slice__uint8_t s, size_t i)
2828
{
2929
uint8_t *elt_ = s.elt + i;
3030
slice__uint8_t s1 = { .elt = s.elt, .len = i };
3131
slice__uint8_t s2 = { .elt = elt_, .len = s.len - i };
3232
return
33-
((__Pulse_Lib_Slice_slice_uint8_t_Pulse_Lib_Slice_slice_uint8_t){ .fst = s1, .snd = s2 });
33+
((__Pulse_Lib_Slice_slice__uint8_t_Pulse_Lib_Slice_slice__uint8_t){ .fst = s1, .snd = s2 });
3434
}
3535

3636
static slice__uint8_t subslice__uint8_t(slice__uint8_t s, size_t i, size_t j)
@@ -62,15 +62,15 @@ static void copy__uint8_t(slice__uint8_t dst, slice__uint8_t src)
6262
void Example_Slice_test(uint8_t *arr)
6363
{
6464
slice__uint8_t slice = from_array__uint8_t(arr, (size_t)6U);
65-
__Pulse_Lib_Slice_slice_uint8_t_Pulse_Lib_Slice_slice_uint8_t
65+
__Pulse_Lib_Slice_slice__uint8_t_Pulse_Lib_Slice_slice__uint8_t
6666
s_ = split__uint8_t(slice, (size_t)2U);
6767
slice__uint8_t s1 = s_.fst;
6868
slice__uint8_t s2 = s_.snd;
6969
slice__uint8_t res = subslice__uint8_t(s2, (size_t)1U, (size_t)4U);
7070
slice__uint8_t s2_ = res;
7171
uint8_t x = op_Array_Access__uint8_t(s2_, len__uint8_t(s1));
7272
op_Array_Assignment__uint8_t(s1, (size_t)1U, x);
73-
__Pulse_Lib_Slice_slice_uint8_t_Pulse_Lib_Slice_slice_uint8_t
73+
__Pulse_Lib_Slice_slice__uint8_t_Pulse_Lib_Slice_slice__uint8_t
7474
s_1 = split__uint8_t(s2, (size_t)2U);
7575
slice__uint8_t s3 = s_1.fst;
7676
slice__uint8_t s4 = s_1.snd;

0 commit comments

Comments
 (0)