diff options
Diffstat (limited to 'src/phcfg.h')
| -rw-r--r-- | src/phcfg.h | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/phcfg.h b/src/phcfg.h index 66a382d6..619bbdc3 100644 --- a/src/phcfg.h +++ b/src/phcfg.h @@ -25,8 +25,19 @@ extern "C" { #endif +/*@ + @ requires \valid(files_enable); + @*/ void reset_array_file_enable(file_enable_t *files_enable); + +/*@ + @ requires \valid_read(files_enable); + @*/ int file_options_save(const file_enable_t *files_enable); + +/*@ + @ requires \valid(files_enable); + @*/ int file_options_load(file_enable_t *files_enable); #ifdef __cplusplus |