1 files changed, 2 insertions, 0 deletions
diff --git a/src/psearchn.h b/src/psearchn.h
index d60b0943..ac8c630a 100644
--- a/src/psearchn.h
+++ b/src/psearchn.h
@@ -31,6 +31,8 @@ extern "C" {
   @ requires \valid_read(options);
   @ requires \valid(list_search_space);
   @ requires \separated(params, options, list_search_space);
+  @ decreases 0;
+  @ ensures  valid_ph_param(params);
   @*/
 pstatus_t photorec_aux(struct ph_param *params, const struct ph_options *options, alloc_data_t *list_search_space);