| 2056 | } |
| 2057 | |
| 2058 | void hd_update_all_geometry(const list_disk_t * list_disk, const int verbose) |
| 2059 | { |
| 2060 | const list_disk_t *element_disk; |
| 2061 | if(verbose>1) |
| 2062 | { |
| 2063 | log_trace("hd_update_all_geometry\n"); |
| 2064 | } |
| 2065 | /*@ |
| 2066 | @ loop invariant valid_list_disk(element_disk); |
| 2067 | @*/ |
| 2068 | for(element_disk=list_disk;element_disk!=NULL;element_disk=element_disk->next) |
| 2069 | { |
| 2070 | /*@ assert \valid(element_disk); */ |
| 2071 | /*@ assert valid_disk(element_disk->disk); */ |
| 2072 | hd_update_geometry(element_disk->disk, verbose); |
| 2073 | /*@ assert \valid(element_disk); */ |
| 2074 | } |
| 2075 | } |
| 2076 | |
| 2077 | void init_disk(disk_t *disk) |
| 2078 | { |