1 files changed, 1 insertions, 0 deletions
diff --git a/src/fatx.h b/src/fatx.h
index a6c46ac9..7c2718b7 100644
--- a/src/fatx.h
+++ b/src/fatx.h
@@ -39,6 +39,7 @@ struct disk_fatx
   @ requires valid_disk(disk_car);
   @ requires \valid(partition);
   @ requires \separated(disk_car, partition);
+  @ decreases 0;
   @*/
 int check_FATX(disk_t *disk_car, partition_t *partition);