diff --git a/sefht.geany b/sefht.geany
index 56ba616bad5db69ad4bb4e2dd89a475aac7e0209..ef3264e9eda3517e94bf0971af9be1a822c4ba27 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 f5d15af33eac9415bab7fabb8a8906a30de90e8f..9c6ad8ce01b8e40816f7518757dcff4067447b93 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 d06b721d1642cd99fe002e8f9d41c6a460d43078..9b4b44cfcdd538973bc447255c9b4168f124fb8d 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 a9f0ef2fab1d5e6d9ce64407009dcd2e11ed24bd..887b996c54ce188f6acc159ab5f08ab76552b447 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 8ccbe31cedd1a957399f7483f970ee74bcdbb4f2..bc8305d0584aa82202b0aed375351f91d7257564 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__ */