1 files changed, 6 insertions, 0 deletions
diff --git a/src/phbs.h b/src/phbs.h
index 031992f9..ee3406a3 100644
--- a/src/phbs.h
+++ b/src/phbs.h
@@ -25,6 +25,12 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires \valid(params);
+  @ requires \valid_read(options);
+  @ requires valid_list_search_space(list_search_space);
+  @ requires \separated(params, options, list_search_space);
+  @*/
 pstatus_t photorec_find_blocksize(struct ph_param *params, const struct ph_options *options, alloc_data_t *list_search_space);
 
 #ifdef __cplusplus