diff options
Diffstat (limited to 'src/pdisksel.c')
| -rw-r--r-- | src/pdisksel.c | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/pdisksel.c b/src/pdisksel.c index 69546944..aa86ab25 100644 --- a/src/pdisksel.c +++ b/src/pdisksel.c @@ -40,6 +40,10 @@ disk_t *photorec_disk_selection_cli(const char *cmd_device, const list_disk_t *l { const list_disk_t *element_disk; disk_t *disk=NULL; + /*@ + @ loop invariant valid_disk(disk); + @ loop assigns element_disk, disk; + @*/ for(element_disk=list_disk;element_disk!=NULL;element_disk=element_disk->next) { if(strcmp(element_disk->disk->device, cmd_device)==0) |