diff --git a/sefht.geany b/sefht.geany
index 39bd9158495e11cfb98f05ad454f391effabb24d..f5df0230f46418b43bbb7b664df37c95d743ea94 100644
--- a/sefht.geany
+++ b/sefht.geany
@@ -28,15 +28,15 @@ long_line_behaviour=1
long_line_column=72
[files]
-current_page=4
+current_page=6
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
FILE_NAME_3=640;Make;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2FMakefile.am;0;8
FILE_NAME_4=1593;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Fcms.c;0;8
FILE_NAME_5=1395;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Fcms.h;0;8
-FILE_NAME_6=4511;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Fdata.c;0;8
-FILE_NAME_7=1145;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Fdata.h;0;8
+FILE_NAME_6=2921;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Fdata.c;0;8
+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=1733;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=2164;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=1296;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Fnode_fragment.c;0;8
@@ -47,7 +47,7 @@ FILE_NAME_14=1212;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fp
FILE_NAME_15=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_16=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_17=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_18=1361;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Fstatus.h;0;8
+FILE_NAME_18=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_19=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_20=1077;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Fmacro.h;0;8
FILE_NAME_21=937;C;0;EUTF-8;1;1;0;%2Fhome%2Fjonathan%2FDokumente%2Fprojekte%2Fprgm%2Finternet%2Fweb%2FSeFHT%2Fsrc%2Flib%2Fsefht%2Fsefht.h;0;8
diff --git a/src/lib/sefht/data.c b/src/lib/sefht/data.c
index df206e0878b6148542351d975fc6a251b4779aba..4c3da9327d3c997bdd1f3944ec137c339728c605 100644
--- a/src/lib/sefht/data.c
+++ b/src/lib/sefht/data.c
@@ -37,8 +37,6 @@
#include "data.h"
-#define NEXT_PAGE(page) page++
-
struct SH_Page
{
page_t id;
@@ -47,19 +45,53 @@ struct SH_Page
struct SH_Data
{
- struct SH_Validator * validator;
+ SH_Validator * validator;
size_t page_n;
struct SH_Page * pages;
page_t last_page;
};
-static inline bool init_validator (struct SH_Data * data,
- struct SH_Status * status);
-static inline void init_pages (struct SH_Data * data);
+static inline
+page_t
+next_page (struct SH_Data * data)
+ /*@*/
+{
+ if (data->last_page == PAGE_MAX)
+ {
+ return PAGE_ERR;
+ }
+ return data->last_page + 1;
+}
+static inline
+bool
+init_validator (/*@special@*/ struct SH_Data * data,
+ /*@null@*/ /*@out@*/ struct SH_Status * status)
+ /*@allocates data->validator@*/
+ /*@defines *(data->validator)@*/
+ /*@globals fileSystem@*/
+ /*@modifies fileSystem@*/
+ /*@modifies status@*/;
+
+static inline
+void
+init_pages (/*@special@*/ struct SH_Data * data)
+ /*@allocates data->pages@*/
+ /*@defines data->page_n,
+ * data->last_page@*/
+ /*@modifies data->page_n@*/
+ /*@modifies data->pages@*/
+ /*@modifies data->last_page@*/;
+
+/*@null@*/
+/*@only@*/
struct SH_Data *
-SH_Data_new (struct SH_Status * status)
+SH_Data_new (/*@out@*/ /*@null@*/ struct SH_Status * status)
+ /*@globals fileSystem@*/
+ /*@modifies fileSystem@*/
+ /*@modifies status@*/
+
{
struct SH_Data * data;
data = malloc (sizeof (struct SH_Data));
@@ -74,6 +106,12 @@ SH_Data_new (struct SH_Status * status)
if (!init_validator (data, status))
{
+
+/* dangerous call to silence splint, should never be executed. */
+#ifdef S_SPLINT_S
+ free (data->validator);
+#endif
+
free (data);
return NULL;
@@ -82,15 +120,28 @@ SH_Data_new (struct SH_Status * status)
init_pages (data);
set_success (status);
-
return data;
}
-static inline void free_validator (struct SH_Data * data);
-static inline void free_pages (struct SH_Data * data);
+static inline
+void
+free_validator (/*@special@*/ struct SH_Data * data)
+ /*@modifies data->validator@*/
+ /*@releases data->validator@*/;
+static inline
void
-SH_Data_free (struct SH_Data * data)
+free_pages (/*@special@*/ struct SH_Data * data)
+ /*@modifies data->pages@*/
+ /*@releases data->pages@*/
+ /*@requires maxRead(data->pages) == (data->page_n - 1)@*/;
+
+void
+SH_Data_free (/*@only@*/ struct SH_Data * data)
+ /*@modifies data->validator@*/
+ /*@modifies data->pages@*/
+ /*@modifies data@*/
+ /*@releases data@*/
{
free_validator (data);
free_pages (data);
@@ -100,8 +151,15 @@ SH_Data_free (struct SH_Data * data)
return;
}
-static inline bool
-init_validator (struct SH_Data * data, struct SH_Status * status)
+static inline
+bool
+init_validator (struct SH_Data * data,
+ /*@out@*/ /*@null@*/ struct SH_Status * status)
+ /*@allocates data->validator@*/
+ /*@defines *(data->validator)@*/
+ /*@globals fileSystem@*/
+ /*@modifies fileSystem@*/
+ /*@modifies status@*/
{
data->validator = SH_Validator_new (status);
@@ -138,15 +196,25 @@ init_validator (struct SH_Data * data, struct SH_Status * status)
return TRUE;
}
-static inline void
-free_validator (struct SH_Data * data)
+static inline
+void
+free_validator (/*@special@*/ struct SH_Data * data)
+ /*@modifies data->validator@*/
+ /*@releases data->validator@*/
{
SH_Validator_free (data->validator);
return;
}
-static inline void
-init_pages (struct SH_Data * data)
+static inline
+void
+init_pages (/*@special@*/ struct SH_Data * data)
+ /*@allocates data->pages@*/
+ /*@defines data->page_n,
+ * data->last_page@*/
+ /*@modifies data->page_n@*/
+ /*@modifies data->pages@*/
+ /*@modifies data->last_page@*/
{
data->page_n = 0;
data->pages = malloc (0);
@@ -155,8 +223,12 @@ init_pages (struct SH_Data * data)
return;
}
-static inline void
-free_pages (struct SH_Data * data)
+static inline
+void
+free_pages (/*@special@*/ struct SH_Data * data)
+ /*@modifies data->pages@*/
+ /*@releases data->pages@*/
+ /*@requires maxRead(data->pages) == (data->page_n - 1)@*/
{
size_t index;
@@ -172,9 +244,21 @@ free_pages (struct SH_Data * data)
page_t
SH_Data_register_page (struct SH_Data * data, const char * name,
struct SH_Status * status)
+ /*@modifies data->page_n@*/
+ /*@modifies data->pages@*/
+ /*@modifies data->last_page@*/
+ /*@requires maxRead(data->pages) == (data->page_n - 1)@*/
+ /*@ensures maxRead(data->pages) == (data->page_n - 1)@*/
+ /*@globals fileSystem@*/
+ /*@modifies fileSystem@*/
+ /*@modifies status@*/
{
+ struct SH_Page * new_pages;
+ page_t page_id;
+
+ page_id = next_page (data);
/* abort on overflow */
- if ((data->last_page == PAGE_MAX) || (data->page_n == SIZE_MAX))
+ if ((page_id == PAGE_ERR) || (data->page_n == SIZE_MAX))
{
set_status (status, E_DOMAIN, 0,
"Maximum number of pages reached.\n");
@@ -182,31 +266,38 @@ SH_Data_register_page (struct SH_Data * data, const char * name,
return PAGE_ERR;
}
- data->pages = realloc (data->pages,
- sizeof (struct SH_Page)
- * (data->page_n + 1));
+ new_pages = realloc (data->pages,
+ sizeof (struct SH_Page)
+ * (data->page_n + 1));
- if (data->pages == NULL)
+ if (new_pages == NULL)
{
set_status (status, E_ALLOC, 5,
"Memory allocation for page data failed.\n");
+/* bad code to silence splint, should never be executed. */
+#ifdef S_SPLINT_S
+ data->pages = (void *) 0x12345;
+#endif
+
return PAGE_ERR;
}
- NEXT_PAGE(data->last_page);
-
- data->pages[data->page_n].id = data->last_page;
- data->pages[data->page_n].name = strdup (name);
+ new_pages[data->page_n].id = page_id;
+ new_pages[data->page_n].name = strdup (name);
- if (data->pages[data->page_n].name == NULL)
+ if (new_pages[data->page_n].name == NULL)
{
set_status (status, E_ALLOC, 4,
"Memory allocation for page data failed.\n");
+ data->pages = new_pages;
return PAGE_ERR;
}
+ /* commit changes */
+ data->pages = new_pages;
+ data->last_page = page_id;
data->page_n++;
set_success (status);
diff --git a/src/lib/sefht/data.h b/src/lib/sefht/data.h
index fd5d702d2b8b92b6da450f8acf9899680e139c0f..8cda0c5f2b1f97ac8e8ace78bc7d21e65b2dd838 100644
--- a/src/lib/sefht/data.h
+++ b/src/lib/sefht/data.h
@@ -36,22 +36,33 @@
#include "validator.h"
-typedef unsigned int page_t;
+typedef /*@abstract@*/ unsigned int page_t;
#define PAGE_ERR 0
#define PAGE_MIN 1
#define PAGE_MAX UINT_MAX
-typedef struct SH_Data SH_Data;
+typedef /*@abstract@*/ struct SH_Data SH_Data;
+/*@null@*/
+/*@only@*/
SH_Data *
-SH_Data_new (struct SH_Status * status);
+SH_Data_new (/*@out@*/ /*@null@*/ struct SH_Status * status)
+ /*@globals fileSystem@*/
+ /*@modifies fileSystem@*/
+ /*@modifies status@*/;
void
-SH_Data_free (SH_Data * data);
+SH_Data_free (/*@only@*/ struct SH_Data * data)
+ /*@modifies data@*/
+ /*@releases data@*/;
page_t
SH_Data_register_page (SH_Data * data, const char * name,
- struct SH_Status * status);
+ struct SH_Status * status)
+ /*@modifies data@*/
+ /*@globals fileSystem@*/
+ /*@modifies fileSystem@*/
+ /*@modifies status@*/;
#endif /* __DATA_H__ */
diff --git a/src/lib/sefht/status.h b/src/lib/sefht/status.h
index 3d7266dc59871bc8ca89a9bfd78c8fbfe0a643d2..0cc1dcb0575bfe8c1b59baeed5b75d193f43e602 100644
--- a/src/lib/sefht/status.h
+++ b/src/lib/sefht/status.h
@@ -28,6 +28,7 @@
#include <errno.h>
#include <string.h>
+#include "macro.h"
#if !defined (__SEFHT_H_INSIDE__) && !defined (LIB_SEFHT_COMPILATION)
#error "Only <sefht/sefht.h> can be included directly."
@@ -53,7 +54,7 @@ do \
STATUS->errno_ = (ERROR == SUCCESS) ? 0: errno; \
STATUS->file = __FILE__; \
STATUS->function = __FUNCTION__; \
- STATUS->line = __LINE__ - OFFSET; \
+ STATUS->line = (unsigned long) (__LINE__ - OFFSET); \
STATUS->message = MESSAGE; \
}; \
\
@@ -62,7 +63,7 @@ do \
ERROR1 (MESSAGE); \
} \
} \
-while (0)
+while (FALSE)
#define set_status_(STATUS, ERROR, OFFSET, LENGTH, MESSAGE, ...) \
do \
@@ -73,7 +74,7 @@ do \
STATUS->errno_ = (ERROR == SUCCESS) ? 0: errno; \
STATUS->file = __FILE__; \
STATUS->function = __FUNCTION__; \
- STATUS->line = __LINE__ - OFFSET; \
+ STATUS->line = (unsigned long) (__LINE__ - OFFSET); \
STATUS->message = malloc (strlen(MESSAGE)+1 + LENGTH); \
if (STATUS->message == NULL) \
{ \
@@ -86,7 +87,7 @@ do \
\
ERROR_ (MESSAGE, __VA_ARGS__); \
} \
-while (0)
+while (FALSE)
#define set_success(STATUS) set_status(STATUS, SUCCESS, 0, NULL)
@@ -107,13 +108,11 @@ struct SH_Status
int errno_;
- const char * file;
- const char * function;
+ /*@observer@*/ const char * file;
+ /*@observer@*/ const char * function;
unsigned long int line;
- char * message;
+ /*@observer@*/ /*@null@*/ char * message;
};
-typedef struct SH_Status SH_Status;
-
#endif /* __STATUS_H__ */