@ @ requires \valid(list_search_space); @ requires \valid(new_current_search_space); @ requires \valid(offset); @ requires \separated(list_search_space, new_current_search_space, offset); @*/
| 1114 | @ requires \separated(list_search_space, new_current_search_space, offset); |
| 1115 | @*/ |
| 1116 | static inline void file_block_remove_from_sp(alloc_data_t *list_search_space, alloc_data_t **new_current_search_space, uint64_t *offset, const unsigned int blocksize) |
| 1117 | { |
| 1118 | #ifndef DISABLED_FOR_FRAMAC |
| 1119 | struct td_list_head *search_walker = &(*new_current_search_space)->list; |
| 1120 | if(search_walker!=NULL) |
| 1121 | { |
| 1122 | alloc_data_t *tmp; |
| 1123 | tmp=td_list_entry(search_walker, alloc_data_t, list); |
| 1124 | if(tmp->start <= *offset && *offset + blocksize <= tmp->end + 1) |
| 1125 | { |
| 1126 | file_block_remove_from_sp_aux(tmp, new_current_search_space, offset, blocksize); |
| 1127 | return; |
| 1128 | } |
| 1129 | } |
| 1130 | td_list_for_each(search_walker, &list_search_space->list) |
| 1131 | { |
| 1132 | alloc_data_t *tmp; |
| 1133 | tmp=td_list_entry(search_walker, alloc_data_t, list); |
| 1134 | if(tmp->start <= *offset && *offset + blocksize <= tmp->end + 1) |
| 1135 | { |
| 1136 | file_block_remove_from_sp_aux(tmp, new_current_search_space, offset, blocksize); |
| 1137 | return ; |
| 1138 | } |
| 1139 | } |
| 1140 | log_critical("file_block_remove_from_sp(list_search_space, alloc_data_t **new_current_search_space, uint64_t *offset, const unsigned int blocksize) failed\n"); |
| 1141 | log_flush(); |
| 1142 | exit(1); |
| 1143 | #endif |
| 1144 | } |
| 1145 | |
| 1146 | /*@ |
| 1147 | @ requires \valid(list); |
no test coverage detected