From 38f3374173921c0fee7ecc8f84f9e72e50fbd7f1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jonathan=20Sch=C3=B6bel?= <jonathan@xn--schbel-yxa.info> Date: Fri, 6 Jan 2023 16:50:59 +0100 Subject: [PATCH] added splint annotations (validator) --- sefht.geany | 10 +-- src/lib/sefht/validator.c | 10 +++ src/lib/sefht/validator.h | 16 +++- src/lib/sefht/validator_tag.c | 149 +++++++++++++++++++++++++++++----- src/lib/sefht/validator_tag.h | 18 +++- 5 files changed, 171 insertions(+), 32 deletions(-) diff --git a/sefht.geany b/sefht.geany index 56ba616..ef3264e 100644 --- a/sefht.geany +++ b/sefht.geany @@ -28,7 +28,7 @@ long_line_behaviour=1 long_line_column=72 [files] -current_page=14 +current_page=19 FILE_NAME_0=923;Sh;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fconfigure.ac;0;8 FILE_NAME_1=73;Make;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2FMakefile.am;0;8 FILE_NAME_2=1143;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Fmain.c;0;8 @@ -45,10 +45,10 @@ FILE_NAME_12=8225;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fp FILE_NAME_13=1892;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Fnode_fragment.h;0;8 FILE_NAME_14=25820;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Ftext.c;0;8 FILE_NAME_15=3637;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Ftext.h;0;8 -FILE_NAME_16=1212;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Fvalidator.c;0;8 -FILE_NAME_17=1260;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Fvalidator.h;0;8 -FILE_NAME_18=1466;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Fvalidator_tag.c;0;8 -FILE_NAME_19=1135;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Fvalidator_tag.h;0;8 +FILE_NAME_16=1779;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Fvalidator.c;0;8 +FILE_NAME_17=1688;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Fvalidator.h;0;8 +FILE_NAME_18=14237;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Fvalidator_tag.c;0;8 +FILE_NAME_19=1156;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Fvalidator_tag.h;0;8 FILE_NAME_20=4304;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Fstatus.h;0;8 FILE_NAME_21=1017;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Flog.h;0;4 FILE_NAME_22=1077;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Fmacro.h;0;8 diff --git a/src/lib/sefht/validator.c b/src/lib/sefht/validator.c index f5d15af..9c6ad8c 100644 --- a/src/lib/sefht/validator.c +++ b/src/lib/sefht/validator.c @@ -49,8 +49,12 @@ struct SH_Validator /*@null@*/ +/*@only@*/ struct SH_Validator * SH_Validator_new (/*@null@*/ /*@out@*/ struct SH_Status * status) + /*@globals fileSystem@*/ + /*@modifies fileSystem@*/ + /*@modifies status@*/ { struct SH_Validator * validator; validator = malloc (sizeof (struct SH_Validator)); @@ -80,9 +84,13 @@ SH_Validator_new (/*@null@*/ /*@out@*/ struct SH_Status * status) } /*@null@*/ +/*@only@*/ struct SH_Validator * SH_Validator_copy (const struct SH_Validator * validator, /*@null@*/ /*@out@*/ struct SH_Status * status) + /*@globals fileSystem@*/ + /*@modifies fileSystem@*/ + /*@modifies status@*/ { struct SH_Validator * copy; copy = malloc (sizeof (struct SH_Validator)); @@ -113,6 +121,8 @@ SH_Validator_copy (const struct SH_Validator * validator, void SH_Validator_free (/*@only@*/ struct SH_Validator * validator) + /*@modifies validator@*/ + /*@releases validator@*/ { free_tags (validator); free (validator); diff --git a/src/lib/sefht/validator.h b/src/lib/sefht/validator.h index d06b721..9b4b44c 100644 --- a/src/lib/sefht/validator.h +++ b/src/lib/sefht/validator.h @@ -40,16 +40,26 @@ typedef struct SH_Validator SH_Validator; /*@null@*/ +/*@only@*/ SH_Validator * -SH_Validator_new (/*@null@*/ /*@out@*/ struct SH_Status * status); +SH_Validator_new (/*@null@*/ /*@out@*/ struct SH_Status * status) + /*@globals fileSystem@*/ + /*@modifies fileSystem@*/ + /*@modifies status@*/; /*@null@*/ +/*@only@*/ SH_Validator * SH_Validator_copy (const SH_Validator * validator, - /*@null@*/ /*@out@*/ struct SH_Status * status); + /*@null@*/ /*@out@*/ struct SH_Status * status) + /*@globals fileSystem@*/ + /*@modifies fileSystem@*/ + /*@modifies status@*/; void -SH_Validator_free (/*@only@*/ SH_Validator * validator); +SH_Validator_free (/*@only@*/ struct SH_Validator * validator) + /*@modifies validator@*/ + /*@releases validator@*/; #endif /* __VALIDATOR_H__ */ diff --git a/src/lib/sefht/validator_tag.c b/src/lib/sefht/validator_tag.c index a9f0ef2..887b996 100644 --- a/src/lib/sefht/validator_tag.c +++ b/src/lib/sefht/validator_tag.c @@ -60,51 +60,94 @@ struct tag_info static inline bool -init_tags (/*@out@*/ struct SH_Validator * validator, - /*@null@*/ /*@out@*/ struct SH_Status * status); +init_tags (/*@special@*/ struct SH_Validator * validator, + /*@null@*/ /*@out@*/ struct SH_Status * status) + /*@defines validator->tags, + validator->tag_n, + validator->last_tag@*/ + /*@modifies validator->tags@*/ + /*@modifies validator->tag_n@*/ + /*@modifies validator->last_tag@*/ + /*@globals fileSystem@*/ + /*@modifies fileSystem@*/ + /*@modifies status@*/; static inline bool -copy_tags (/*@out@*/ struct SH_Validator * copy, +copy_tags (/*@special@*/ struct SH_Validator * copy, const struct SH_Validator * validator, - /*@null@*/ /*@out@*/ struct SH_Status * status); + /*@null@*/ /*@out@*/ struct SH_Status * status) + /*@defines copy->tags, + copy->tag_n, + copy->last_tag@*/ + /*@modifies copy->tags@*/ + /*@modifies copy->tag_n@*/ + /*@modifies copy->last_tag@*/ + /*@globals fileSystem@*/ + /*@modifies fileSystem@*/ + /*@modifies status@*/; static inline void free_tags (/*@special@*/ struct SH_Validator * validator) + /*@modifies validator->tags@*/ /*@releases validator->tags@*/; static inline size_t -get_tag_number (const struct SH_Validator * validator); +get_tag_number (const struct SH_Validator * validator) + /*@*/; static inline Tag add_tag (struct SH_Validator * validator, const char * tag, - /*@null@*/ /*@out@*/ struct SH_Status * status); + /*@null@*/ /*@out@*/ struct SH_Status * status) + /*@modifies validator->tags@*/ + /*@modifies validator->tag_n@*/ + /*@modifies validator->last_tag@*/ + /*@globals fileSystem@*/ + /*@modifies fileSystem@*/ + /*@modifies status@*/; /*@unused@*/ static inline bool -is_tag_id (struct SH_Validator * validator, Tag id); +is_tag_id (const struct SH_Validator * validator, Tag id) + /*@*/; static inline bool -is_tag_name (struct SH_Validator * validator, const char * name); +is_tag_name (const struct SH_Validator * validator, const char * name) + /*@*/; /*@unused@*/ static inline /*@null@*/ +/*@only@*/ char * -get_tag_name_by_id (struct SH_Validator * validator, Tag id, - /*@null@*/ /*@out@*/ struct SH_Status * status); +get_tag_name_by_id (const struct SH_Validator * validator, Tag id, + /*@null@*/ /*@out@*/ struct SH_Status * status) + /*@globals fileSystem@*/ + /*@modifies fileSystem@*/ + /*@modifies status@*/; static inline Tag -get_tag_id_by_name (struct SH_Validator * validator, - const char * name); +get_tag_id_by_name (const struct SH_Validator * validator, + const char * name) + /*@*/; +static inline +bool +remove_tag (struct SH_Validator * validator, Tag id, + /*@null@*/ /*@out@*/ struct SH_Status * status) + /*@modifies validator->tag_n@*/ + /*@modifies validator->tags@*/ + /*@modifies validator->last_tag@*/ + /*@globals fileSystem@*/ + /*@modifies fileSystem@*/ + /*@modifies status@*/; #define EXECUTE_ON_ALL_TAGS_IF(ITER, CONDITION, BLOCK) \ @@ -125,6 +168,8 @@ do \ if (index == free_index) \ { \ is_free = TRUE; \ + \ + /*@innerbreak@*/ \ break; \ } \ } \ @@ -132,7 +177,7 @@ do \ if (!is_free && CONDITION) BLOCK \ } \ } \ -while (0) +while (FALSE) #define EXECUTE_ON_ALL_TAGS(BASE, BLOCK) \ EXECUTE_ON_ALL_TAGS_IF (BASE, TRUE, BLOCK) @@ -140,13 +185,25 @@ while (0) static inline bool -init_tags (/*@out@*/ struct SH_Validator * validator, +init_tags (/*@special@*/ struct SH_Validator * validator, /*@null@*/ /*@out@*/ struct SH_Status * status) + /*@defines validator->tags, + validator->tag_n, + validator->last_tag@*/ + /*@modifies validator->tags@*/ + /*@modifies validator->tag_n@*/ + /*@modifies validator->last_tag@*/ + /*@globals fileSystem@*/ + /*@modifies fileSystem@*/ + /*@modifies status@*/ { validator->tags = malloc (sizeof (struct tag_info)); if (validator->tags == NULL) { set_status (status, E_ALLOC, 3, "malloc failed"); + + validator->tag_n = 0; + validator->last_tag = TAG_ERR; return FALSE; } @@ -159,9 +216,18 @@ init_tags (/*@out@*/ struct SH_Validator * validator, static inline bool -copy_tags (/*@out@*/ struct SH_Validator * copy, +copy_tags (/*@special@*/ struct SH_Validator * copy, const struct SH_Validator * validator, /*@null@*/ /*@out@*/ struct SH_Status * status) + /*@defines copy->tags, + copy->tag_n, + copy->last_tag@*/ + /*@modifies copy->tags@*/ + /*@modifies copy->tag_n@*/ + /*@modifies copy->last_tag@*/ + /*@globals fileSystem@*/ + /*@modifies fileSystem@*/ + /*@modifies status@*/ { bool is_free; size_t index; @@ -178,6 +244,9 @@ copy_tags (/*@out@*/ struct SH_Validator * copy, if (copy->tags == NULL) { set_status (status, E_ALLOC, 5, "malloc failed"); + + copy->tag_n = 0; + copy->last_tag = TAG_ERR; return FALSE; } @@ -200,6 +269,8 @@ copy_tags (/*@out@*/ struct SH_Validator * copy, if (index == free_index) { is_free = TRUE; + + /*@innerbreak@*/ break; } } @@ -238,8 +309,10 @@ copy_tags (/*@out@*/ struct SH_Validator * copy, return TRUE; } -static inline void +static inline +void free_tags (/*@special@*/ struct SH_Validator * validator) + /*@modifies validator->tags@*/ /*@releases validator->tags@*/ { EXECUTE_ON_ALL_TAGS ( @@ -255,6 +328,7 @@ free_tags (/*@special@*/ struct SH_Validator * validator) static inline size_t get_tag_number (const struct SH_Validator * validator) + /*@*/ { size_t tag_n; @@ -277,6 +351,12 @@ Tag add_tag (struct SH_Validator * validator, const char * tag, /*@null@*/ /*@out@*/ struct SH_Status * status) + /*@modifies validator->tags@*/ + /*@modifies validator->tag_n@*/ + /*@modifies validator->last_tag@*/ + /*@globals fileSystem@*/ + /*@modifies fileSystem@*/ + /*@modifies status@*/ { Tag tag_id; size_t index; @@ -367,7 +447,8 @@ add_tag (struct SH_Validator * validator, /*@unused@*/ static inline bool -is_tag_id (struct SH_Validator * validator, Tag id) +is_tag_id (const struct SH_Validator * validator, Tag id) + /*@*/ { EXECUTE_ON_ALL_TAGS_IF ( validator->tag, @@ -381,7 +462,8 @@ is_tag_id (struct SH_Validator * validator, Tag id) static inline bool -is_tag_name (struct SH_Validator * validator, const char * name) +is_tag_name (const struct SH_Validator * validator, const char * name) + /*@*/ { EXECUTE_ON_ALL_TAGS_IF ( validator->tag, @@ -396,9 +478,13 @@ is_tag_name (struct SH_Validator * validator, const char * name) /*@unused@*/ static inline /*@null@*/ +/*@only@*/ char * -get_tag_name_by_id (struct SH_Validator * validator, Tag id, +get_tag_name_by_id (const struct SH_Validator * validator, Tag id, /*@null@*/ /*@out@*/ struct SH_Status * status) + /*@globals fileSystem@*/ + /*@modifies fileSystem@*/ + /*@modifies status@*/ { char * name; @@ -422,8 +508,9 @@ get_tag_name_by_id (struct SH_Validator * validator, Tag id, static inline Tag -get_tag_id_by_name (struct SH_Validator * validator, +get_tag_id_by_name (const struct SH_Validator * validator, const char * name) + /*@*/ { EXECUTE_ON_ALL_TAGS_IF ( validator->tag, @@ -439,6 +526,12 @@ static inline bool remove_tag (struct SH_Validator * validator, Tag id, /*@null@*/ /*@out@*/ struct SH_Status * status) + /*@modifies validator->tag_n@*/ + /*@modifies validator->tags@*/ + /*@modifies validator->last_tag@*/ + /*@globals fileSystem@*/ + /*@modifies fileSystem@*/ + /*@modifies status@*/ { #define tags validator->tags #define tag_n validator->tag_n @@ -469,6 +562,8 @@ remove_tag (struct SH_Validator * validator, Tag id, tags[free_index].next = tags[tags[free_index].next].next; + + /*@innerbreak@*/ break; } } @@ -520,15 +615,23 @@ remove_tag (struct SH_Validator * validator, Tag id, bool SH_Validator_check_tag (struct SH_Validator * validator, const char * tag) + /*@*/ { return is_tag_name (validator, tag); } Tag +/*@alt void@*/ SH_Validator_register_tag (struct SH_Validator * validator, const char * tag, /*@null@*/ /*@out@*/ struct SH_Status * status) + /*@modifies validator->tags@*/ + /*@modifies validator->tag_n@*/ + /*@modifies validator->last_tag@*/ + /*@globals fileSystem@*/ + /*@modifies fileSystem@*/ + /*@modifies status@*/ { Tag tag_id; @@ -547,6 +650,12 @@ SH_Validator_deregister_tag (struct SH_Validator * validator, Tag id, /*@null@*/ /*@out@*/ struct SH_Status * status) + /*@modifies validator->tag_n@*/ + /*@modifies validator->tags@*/ + /*@modifies validator->last_tag@*/ + /*@globals fileSystem@*/ + /*@modifies fileSystem@*/ + /*@modifies status@*/ { return remove_tag (validator, id, status); } diff --git a/src/lib/sefht/validator_tag.h b/src/lib/sefht/validator_tag.h index 8ccbe31..bc8305d 100644 --- a/src/lib/sefht/validator_tag.h +++ b/src/lib/sefht/validator_tag.h @@ -42,19 +42,29 @@ typedef unsigned int Tag; Tag +/*@alt void@*/ SH_Validator_register_tag (SH_Validator * validator, const char * tag, /*@null@*/ /*@out@*/ - struct SH_Status * status); + struct SH_Status * status) + /*@modifies validator@*/ + /*@globals fileSystem@*/ + /*@modifies fileSystem@*/ + /*@modifies status@*/; bool SH_Validator_deregister_tag (SH_Validator * validator, Tag id, /*@null@*/ /*@out@*/ - struct SH_Status * status); + struct SH_Status * status) + /*@modifies validator@*/ + /*@globals fileSystem@*/ + /*@modifies fileSystem@*/ + /*@modifies status@*/; bool -SH_Validator_check_tag (SH_Validator * validator, - const char * tag); +SH_Validator_check_tag (struct SH_Validator * validator, + const char * tag) + /*@*/; #endif /* __VALIDATOR_TAG_H__ */ -- GitLab