diff --git a/sefht.geany b/sefht.geany
index 730c3d965a2512ebb32f0977932932e3daa05278..3bca782fb8c545d99c0e5b6c020e09f84b540473 100644
--- a/sefht.geany
+++ b/sefht.geany
@@ -28,7 +28,7 @@ long_line_behaviour=1
long_line_column=72
[files]
-current_page=10
+current_page=12
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
@@ -39,10 +39,10 @@ FILE_NAME_6=2921;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fpr
FILE_NAME_7=1583;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Fdata.h;0;8
FILE_NAME_8=1185;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Ffragment.c;0;8
FILE_NAME_9=1835;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Ffragment.h;0;8
-FILE_NAME_10=1156;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Ffragment_data.c;0;8
-FILE_NAME_11=1164;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Ffragment_class.c;0;8
-FILE_NAME_12=1099;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Fnode_fragment.c;0;8
-FILE_NAME_13=2259;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_10=1923;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Ffragment_data.c;0;8
+FILE_NAME_11=1701;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Ffragment_class.c;0;8
+FILE_NAME_12=8225;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Fnode_fragment.c;0;8
+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=1384;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=2692;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
diff --git a/src/lib/sefht/fragment_class.c b/src/lib/sefht/fragment_class.c
index ea72c2be230101a0d0f9b25e2f08ef32024df1e0..c33cfdb3bbd44a69040feaad5e2da8749ff25da6 100644
--- a/src/lib/sefht/fragment_class.c
+++ b/src/lib/sefht/fragment_class.c
@@ -40,12 +40,14 @@
static inline
void
-init_fragment (struct SH_Fragment * fragment,
- SH_Data * data,
+init_fragment (/*@out@*/ struct SH_Fragment * fragment,
+ /*@dependent@*/ SH_Data * data,
const enum SH_FRAGMENT_TYPE type,
+ /*@shared@*/
const struct fragment_methods * const methods)
- /*@sets fragment->data,
- fragment->type@*/
+ /*@modifies fragment->data@*/
+ /*@modifies fragment->type@*/
+ /*@modifies fragment->methods@*/
{
fragment->data = data;
fragment->type = type;
@@ -57,6 +59,8 @@ init_fragment (struct SH_Fragment * fragment,
static inline
void
free_fragment (struct SH_Fragment * fragment)
+ /*@modifies fragment@*/
+ /*@releases fragment@*/
{
(void) fragment;
return;
@@ -64,8 +68,11 @@ free_fragment (struct SH_Fragment * fragment)
static inline
void
-copy_fragment (struct SH_Fragment * copy,
- struct SH_Fragment * fragment)
+copy_fragment (/*@out@*/ struct SH_Fragment * copy,
+ const struct SH_Fragment * fragment)
+ /*@modifies copy->data@*/
+ /*@modifies copy->type@*/
+ /*@modifies copy->methods@*/
{
copy->data = fragment->data;
copy->type = fragment->type;
@@ -76,7 +83,8 @@ copy_fragment (struct SH_Fragment * copy,
static inline
enum SH_FRAGMENT_TYPE
-get_type (struct SH_Fragment * fragment)
+get_type (const struct SH_Fragment * fragment)
+ /*@*/
{
return fragment->type;
}
diff --git a/src/lib/sefht/fragment_data.c b/src/lib/sefht/fragment_data.c
index 4bfac5aa78db0962acc2048f91653cbe8d865f40..334a3badaf638288b89bec97d80397c7950dc42f 100644
--- a/src/lib/sefht/fragment_data.c
+++ b/src/lib/sefht/fragment_data.c
@@ -76,10 +76,10 @@ struct fragment_methods
struct SH_Fragment
{
- SH_Data * data;
+ /*@dependent@*/ SH_Data * data;
enum SH_FRAGMENT_TYPE type;
- const struct fragment_methods * methods;
+ /*@shared@*/ const struct fragment_methods * methods;
};
#endif /* LIB_SEFHT_COMPILATION */
diff --git a/src/lib/sefht/node_fragment.c b/src/lib/sefht/node_fragment.c
index e470ca325a50f5be90941addbb75e02eb3228717..b1294cdf3288ffa92432734f8b314531a4aaf956 100644
--- a/src/lib/sefht/node_fragment.c
+++ b/src/lib/sefht/node_fragment.c
@@ -62,22 +62,31 @@ struct SH_NodeFragment
static const struct fragment_methods methods = {
(struct SH_Fragment * (*)(const struct SH_Fragment *,
+ /*@out@*/ /*@null@*/
struct SH_Status *))
SH_NodeFragment_deepcopy,
- (void (*)(struct SH_Fragment *))
+ (void (*)(/*@only@*/ struct SH_Fragment *))
SH_NodeFragment_free,
- (struct SH_Text * (*)(struct SH_Fragment *, enum HTML_MODE,
+ (struct SH_Text * (*)(const struct SH_Fragment *,
+ enum HTML_MODE,
unsigned int, unsigned int, const char *,
- struct SH_Status *))
+ /*@out@*/ /*@null@*/ struct SH_Status *))
SH_NodeFragment_to_html
};
-struct SH_Fragment *
-SH_NodeFragment_new (const char * tag, struct SH_Data * data,
- struct SH_Status * status)
+/*@null@*/
+/*@only@*/
+struct SH_Fragment /*@alt struct SH_NodeFragment@*/ *
+SH_NodeFragment_new (const char * tag,
+ /*@dependent@*/ SH_Data * data,
+ /*@out@*/ /*@null@*/ struct SH_Status * status)
+ /*@globals NODE,
+ fileSystem@*/
+ /*@modifies fileSystem@*/
+ /*@modifies status@*/
{
struct SH_NodeFragment * fragment;
@@ -115,7 +124,9 @@ SH_NodeFragment_new (const char * tag, struct SH_Data * data,
}
void
-SH_NodeFragment_free (struct SH_NodeFragment * fragment)
+SH_NodeFragment_free (/*@only@*/ struct SH_NodeFragment * fragment)
+ /*@modifies fragment@*/
+ /*@releases fragment@*/
{
size_t index;
@@ -134,9 +145,14 @@ SH_NodeFragment_free (struct SH_NodeFragment * fragment)
return;
}
-struct SH_Fragment *
-SH_NodeFragment_copy (struct SH_NodeFragment * fragment,
- struct SH_Status * status)
+/*@null@*/
+/*@only@*/
+struct SH_Fragment /*@alt struct SH_NodeFragment@*/ *
+SH_NodeFragment_copy (const struct SH_NodeFragment * fragment,
+ /*@out@*/ /*@null@*/ struct SH_Status * status)
+ /*@globals fileSystem@*/
+ /*@modifies fileSystem@*/
+ /*@modifies status@*/
{
struct SH_NodeFragment * copy;
@@ -173,9 +189,15 @@ SH_NodeFragment_copy (struct SH_NodeFragment * fragment,
return (struct SH_Fragment *) copy;
}
-struct SH_Fragment *
-SH_NodeFragment_deepcopy (struct SH_NodeFragment * fragment,
+/*@null@*/
+/*@only@*/
+struct SH_Fragment /*@alt struct SH_NodeFragment@*/ *
+SH_NodeFragment_deepcopy (const struct SH_NodeFragment * fragment,
+ /*@out@*/ /*@null@*/
struct SH_Status * status)
+ /*@globals fileSystem@*/
+ /*@modifies fileSystem@*/
+ /*@modifies status@*/
{
struct SH_NodeFragment * copy;
struct SH_Fragment * child;
@@ -217,6 +239,10 @@ SH_NodeFragment_deepcopy (struct SH_NodeFragment * fragment,
"fragment child failed.\n");
free (copy->tag);
+/* dangerous call to silence splint, should never be executed. */
+#ifdef S_SPLINT_S
+ free (copy->childs);
+#endif
free (copy);
return NULL;
@@ -244,14 +270,20 @@ SH_NodeFragment_deepcopy (struct SH_NodeFragment * fragment,
}
bool
-SH_Fragment_is_NodeFragment (struct SH_Fragment * fragment)
+SH_Fragment_is_NodeFragment (const struct SH_Fragment * fragment)
+ /*@*/
{
return get_type (fragment) == NODE;
}
+/*@null@*/
+/*@only@*/
char *
-SH_NodeFragment_get_tag (struct SH_NodeFragment * fragment,
- struct SH_Status * status)
+SH_NodeFragment_get_tag (const struct SH_NodeFragment * fragment,
+ /*@out@*/ /*@null@*/ struct SH_Status * status)
+ /*@globals fileSystem@*/
+ /*@modifies fileSystem@*/
+ /*@modifies status@*/
{
char * tag;
@@ -271,10 +303,16 @@ SH_NodeFragment_get_tag (struct SH_NodeFragment * fragment,
return tag;
}
+/*@null@*/
+/*@observer@*/
struct SH_Fragment *
-SH_NodeFragment_get_child (struct SH_NodeFragment * fragment,
+SH_NodeFragment_get_child (const struct SH_NodeFragment * fragment,
size_t index,
+ /*@out@*/ /*@null@*/
struct SH_Status * status)
+ /*@globals fileSystem@*/
+ /*@modifies fileSystem@*/
+ /*@modifies status@*/
{
if (index >= fragment->child_n)
{
@@ -290,8 +328,9 @@ SH_NodeFragment_get_child (struct SH_NodeFragment * fragment,
}
bool
-SH_NodeFragment_is_child (struct SH_NodeFragment * fragment,
- struct SH_Fragment * child)
+SH_NodeFragment_is_child (const struct SH_NodeFragment * fragment,
+ const struct SH_Fragment * child)
+ /*@*/
{
size_t index;
@@ -306,8 +345,9 @@ SH_NodeFragment_is_child (struct SH_NodeFragment * fragment,
}
bool
-SH_NodeFragment_is_descendant (struct SH_NodeFragment * fragment,
- struct SH_Fragment * child)
+SH_NodeFragment_is_descendant (const struct SH_NodeFragment * fragment,
+ const struct SH_Fragment * child)
+ /*@*/
{
size_t index;
@@ -328,23 +368,37 @@ SH_NodeFragment_is_descendant (struct SH_NodeFragment * fragment,
bool
SH_NodeFragment_append_child (struct SH_NodeFragment * fragment,
- struct SH_Fragment * child,
+ /*@only@*/ struct SH_Fragment * child,
+ /*@out@*/ /*@null@*/
struct SH_Status * status)
+ /*@modifies fragment->childs@*/
+ /*@modifies fragment->child_n@*/
+ /*@globals fileSystem@*/
+ /*@modifies fileSystem@*/
+ /*@modifies status@*/
{
- fragment->childs = realloc (fragment->childs,
- sizeof (struct SH_Fragment *)
- * (fragment->child_n + 1));
+ struct SH_Fragment ** new_childs;
- if (fragment->childs == NULL)
+ new_childs = realloc (fragment->childs,
+ sizeof (struct SH_Fragment *)
+ * (fragment->child_n + 1));
+
+ if (new_childs == NULL)
{
set_status (status, E_ALLOC, 6,
"Memory allocation for "
"fragment child failed.\n");
+/* bad code to silence splint, should never be executed. */
+#ifdef S_SPLINT_S
+ fragment->childs = (void *) 0x12345;
+#endif
return FALSE;
}
- fragment->childs[fragment->child_n] = child;
+ new_childs[fragment->child_n] = child;
+
+ fragment->childs = new_childs;
fragment->child_n++;
set_success (status);
@@ -352,13 +406,18 @@ SH_NodeFragment_append_child (struct SH_NodeFragment * fragment,
return TRUE;
}
+/*@null@*/
+/*@only@*/
struct SH_Text *
-SH_NodeFragment_to_html (struct SH_NodeFragment * fragment,
+SH_NodeFragment_to_html (const struct SH_NodeFragment * fragment,
enum HTML_MODE mode,
unsigned int indent_base,
unsigned int indent_step,
- char * indent_char,
- struct SH_Status * status)
+ const char * indent_char,
+ /*@out@*/ /*@null@*/ struct SH_Status * status)
+ /*@globals fileSystem@*/
+ /*@modifies fileSystem@*/
+ /*@modifies status@*/
{
struct SH_Text * html;
struct SH_Text * child;
@@ -366,7 +425,7 @@ SH_NodeFragment_to_html (struct SH_NodeFragment * fragment,
size_t index;
html = SH_Text_new (status);
- if (failed (status))
+ if (html == NULL)
{
return NULL;
}
@@ -380,7 +439,8 @@ SH_NodeFragment_to_html (struct SH_NodeFragment * fragment,
return NULL;
}
- for (index = 0; index < indent_base; index++)
+ for (index = 0; ((unsigned int) index) < indent_base;
+ index++)
{
if (!SH_Text_append_string (indent_text,
indent_char,
diff --git a/src/lib/sefht/node_fragment.h b/src/lib/sefht/node_fragment.h
index a0d8d4f701d2b503311260ca67c9d8bf74c6840e..518c52d25d68b98b602aee4c214afa2a170541c3 100644
--- a/src/lib/sefht/node_fragment.h
+++ b/src/lib/sefht/node_fragment.h
@@ -39,56 +39,98 @@
#define INDENT_TEXT "\t"
-typedef struct SH_NodeFragment SH_NodeFragment;
+typedef /*@abstract@*/ struct SH_NodeFragment SH_NodeFragment;
-SH_Fragment *
+/*@null@*/
+/*@only@*/
+SH_Fragment /*@alt SH_NodeFragment@*/ *
SH_NodeFragment_new (const char * tag,
- SH_Data * data,
- struct SH_Status * status);
+ /*@dependent@*/ SH_Data * data,
+ /*@out@*/ /*@null@*/ struct SH_Status * status)
+ /*@globals fileSystem@*/
+ /*@modifies fileSystem@*/
+ /*@modifies status@*/;
void
-SH_NodeFragment_free (SH_NodeFragment * fragment);
-
-SH_Fragment *
-SH_NodeFragment_copy (SH_NodeFragment * fragment,
- struct SH_Status * status);
-
-SH_Fragment *
-SH_NodeFragment_deepcopy (SH_NodeFragment * fragment,
- struct SH_Status * status);
+SH_NodeFragment_free (/*@only@*/ SH_NodeFragment * fragment)
+ /*@modifies fragment@*/
+ /*@releases fragment@*/;
+
+/*@null@*/
+/*@only@*/
+SH_Fragment /*@alt SH_NodeFragment@*/ *
+SH_NodeFragment_copy (const SH_NodeFragment * fragment,
+ /*@out@*/ /*@null@*/ struct SH_Status * status)
+ /*@globals fileSystem@*/
+ /*@modifies fileSystem@*/
+ /*@modifies status@*/;
+
+/*@null@*/
+/*@only@*/
+SH_Fragment /*@alt SH_NodeFragment@*/ *
+SH_NodeFragment_deepcopy (const SH_NodeFragment * fragment,
+ /*@out@*/ /*@null@*/
+ struct SH_Status * status)
+ /*@globals fileSystem@*/
+ /*@modifies fileSystem@*/
+ /*@modifies status@*/;
bool
-SH_Fragment_is_NodeFragment (SH_Fragment * fragment);
+SH_Fragment_is_NodeFragment (const SH_Fragment * fragment)
+ /*@*/;
+/*@null@*/
+/*@only@*/
char *
-SH_NodeFragment_get_tag (SH_NodeFragment * fragment,
- struct SH_Status * status);
-
+SH_NodeFragment_get_tag (const SH_NodeFragment * fragment,
+ /*@out@*/ /*@null@*/ struct SH_Status * status)
+ /*@globals fileSystem@*/
+ /*@modifies fileSystem@*/
+ /*@modifies status@*/;
+
+/*@null@*/
+/*@observer@*/
SH_Fragment *
-SH_NodeFragment_get_child (SH_NodeFragment * fragment,
+SH_NodeFragment_get_child (const SH_NodeFragment * fragment,
size_t index,
- struct SH_Status * status);
+ /*@out@*/ /*@null@*/
+ struct SH_Status * status)
+ /*@globals fileSystem@*/
+ /*@modifies fileSystem@*/
+ /*@modifies status@*/;
bool
-SH_NodeFragment_is_child (SH_NodeFragment * fragment,
- SH_Fragment * child);
+SH_NodeFragment_is_child (const SH_NodeFragment * fragment,
+ const SH_Fragment * child)
+ /*@*/;
bool
-SH_NodeFragment_is_descendant (SH_NodeFragment * fragment,
- SH_Fragment * child);
+SH_NodeFragment_is_descendant (const struct SH_NodeFragment * fragment,
+ const struct SH_Fragment * child)
+ /*@*/;
bool
-SH_NodeFragment_append_child (SH_NodeFragment * fragment,
- SH_Fragment * child,
- struct SH_Status * status);
-
+SH_NodeFragment_append_child (struct SH_NodeFragment * fragment,
+ /*@only@*/ struct SH_Fragment * child,
+ /*@out@*/ /*@null@*/
+ struct SH_Status * status)
+ /*@modifies fragment@*/
+ /*@globals fileSystem@*/
+ /*@modifies fileSystem@*/
+ /*@modifies status@*/;
+
+/*@null@*/
+/*@only@*/
SH_Text *
-SH_NodeFragment_to_html (SH_NodeFragment * fragment,
+SH_NodeFragment_to_html (const SH_NodeFragment * fragment,
enum HTML_MODE mode,
unsigned int indent_base,
unsigned int indent_step,
- char * indent_char,
- struct SH_Status * status);
+ const char * indent_char,
+ /*@out@*/ /*@null@*/ struct SH_Status * status)
+ /*@globals fileSystem@*/
+ /*@modifies fileSystem@*/
+ /*@modifies status@*/;
#endif /* __NODE_FRAGMENT_H__ */