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

added splint annotations (node fragment)

parent c408639b
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=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
......
......@@ -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;
}
......
......@@ -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 */
......
......@@ -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,
......
......@@ -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__ */
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