-
Notifications
You must be signed in to change notification settings - Fork 16
Open
Labels
enhancementNew feature or requestNew feature or request
Description
7d4d0fd removed the definition of array_to_subslice3 and slice_subslice3
The goal of this phase was to replace occurrences of array_to_subslice (and slice_subslice3) where the range start and end are constant values, with a more optimized macro that does not take so many arguments.
Concretely, the removal of array_to_subslice3 generates a diff like this:
- Eurydice_slice_copy(Eurydice_array_to_subslice3(uu____0,
- (size_t)0U,
- Eurydice_slice_len(slice, uint8_t),
- uint8_t *),
+ Eurydice_slice_copy(array_to_subslice_3621(uu____0,
+ (
+ KRML_CLITERAL(core_ops_range_Range_08){
+ .start = (size_t)0U,
+ .end = Eurydice_slice_len(slice, uint8_t)
+ }
+ )),The new code is quite a bit more verbose.
Can we restore this code quality optimization? @Lin23299 thanks!
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
enhancementNew feature or requestNew feature or request