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

added splint annotations (data)

parent 0a062a4a
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
sefht.geany
+ 4
− 4
View file @ 6f871cb6
......@@ -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
......
src/lib/sefht/data.c
+ 120
− 29
View file @ 6f871cb6
......@@ -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);
......
src/lib/sefht/data.h
+ 16
− 5
View file @ 6f871cb6
......@@ -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__ */
src/lib/sefht/status.h
+ 8
− 9
View file @ 6f871cb6
......@@ -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__ */
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment