diff options
Diffstat (limited to 'src/sessionp.h')
| -rw-r--r-- | src/sessionp.h | 23 |
1 files changed, 22 insertions, 1 deletions
diff --git a/src/sessionp.h b/src/sessionp.h index 18ab7324..c5a1b57f 100644 --- a/src/sessionp.h +++ b/src/sessionp.h @@ -25,8 +25,29 @@ extern "C" { #endif +/*@ + @ requires \valid(cmd_device); + @ requires \valid(current_cmd); + @ requires valid_list_search_space(list_free_space); + @ requires \separated(cmd_device, current_cmd, list_free_space); + @*/ +// ensures *cmd_device==\null || valid_read_string(*cmd_device); +// ensures *current_cmd==\null || valid_read_string(*current_cmd); +// ensures valid_list_search_space(list_free_space); int session_load(char **cmd_device, char **current_cmd, alloc_data_t *list_free_space); -int session_save(alloc_data_t *list_free_space, struct ph_param *params, const struct ph_options *options); + +/*@ + @ requires list_free_space==\null || \valid_read(list_free_space); + @ requires params==\null || \valid_read(params); + @ requires options==\null || \valid_read(options); + @*/ +int session_save(const alloc_data_t *list_free_space, const struct ph_param *params, const struct ph_options *options); + +/*@ + @ requires \valid_read(list_free_space); + @ requires params==\null || \valid_read(params); + @ requires options==\null || \valid_read(options); + @*/ time_t regular_session_save(alloc_data_t *list_free_space, struct ph_param *params, const struct ph_options *options, time_t current_time); #ifdef __cplusplus |