Skip to content
Snippets Groups Projects
Commit 38f33741 authored by Jonathan Schöbel's avatar Jonathan Schöbel
Browse files

added splint annotations (validator)

parent 65b9c179
No related branches found
No related tags found
No related merge requests found
......@@ -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
......
......@@ -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);
......
......@@ -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__ */
......@@ -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);
}
......
......@@ -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__ */
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment