Skip to content

Commit

Permalink
assertions and fixes recommended by Frama-C
Browse files Browse the repository at this point in the history 
all tests pass on 64bit
  • Loading branch information
Reini Urban committed Sep 8, 2014
1 parent 5a81129 commit 74c0051
Show file tree
Hide file tree
Showing 7 changed files with 41 additions and 24 deletions.
2 changes: 1 addition & 1 deletion config.mak
View file
Expand Up @@ -115,7 +115,7 @@ endif
endif

ifeq (${DEBUG},0)
DEBUGFLAGS += -O3
DEBUGFLAGS += -O3 -DNDEBUG
CFLAGS += -D_FORTIFY_SOURCE=2
endif
ifneq (${SANDBOX},0)
Expand Down
18 changes: 9 additions & 9 deletions core/gc.c
View file
Expand Up @@ -310,7 +310,7 @@ PN_SIZE potion_type_size(Potion *P, const struct PNObject *ptr) {
case POTION_COPIED:
case POTION_FWD:
sz = ((struct PNFwd *)ptr)->siz;
goto done;
goto done_1;
}

if (ptr->vt < PN_TNIL) goto err;
Expand All @@ -331,7 +331,7 @@ PN_SIZE potion_type_size(Potion *P, const struct PNObject *ptr) {
(unsigned long)ptr, (unsigned long)ptr->vt);
return 0;
}
goto done;
goto done_1;
}

switch (ptr->vt) {
Expand Down Expand Up @@ -385,7 +385,7 @@ PN_SIZE potion_type_size(Potion *P, const struct PNObject *ptr) {
break;
}

done:
done_1:
if (sz < sizeof(struct PNFwd))
sz = sizeof(struct PNFwd);
return PN_ALIGN(sz, 8); // force 64-bit alignment
Expand Down Expand Up @@ -415,15 +415,15 @@ void *potion_mark_minor(Potion *P, const struct PNObject *ptr) {
case POTION_COPIED:
case POTION_FWD:
GC_MINOR_UPDATE(((struct PNFwd *)ptr)->ptr);
goto done;
goto done_2;
}

if (ptr->vt > PN_TUSER) {
GC_MINOR_UPDATE(PN_VTABLE(ptr->vt));
int ivars = ((struct PNVtable *)PN_VTABLE(ptr->vt))->ivlen;
for (i = 0; i < ivars; i++)
GC_MINOR_UPDATE(((struct PNObject *)ptr)->ivars[i]);
goto done;
goto done_2;
}

switch (ptr->vt) {
Expand Down Expand Up @@ -505,7 +505,7 @@ void *potion_mark_minor(Potion *P, const struct PNObject *ptr) {
break;
}

done:
done_2:
sz = potion_type_size(P, ptr);
return (void *)((char *)ptr + sz);
}
Expand All @@ -519,15 +519,15 @@ void *potion_mark_major(Potion *P, const struct PNObject *ptr) {
case POTION_COPIED:
case POTION_FWD:
GC_MAJOR_UPDATE(((struct PNFwd *)ptr)->ptr);
goto done;
goto done_3;
}

if (ptr->vt > PN_TUSER) {
GC_MAJOR_UPDATE(PN_VTABLE(ptr->vt));
int ivars = ((struct PNVtable *)PN_VTABLE(ptr->vt))->ivlen;
for (i = 0; i < ivars; i++)
GC_MAJOR_UPDATE(((struct PNObject *)ptr)->ivars[i]);
goto done;
goto done_3;
}

switch (ptr->vt) {
Expand Down Expand Up @@ -609,7 +609,7 @@ void *potion_mark_major(Potion *P, const struct PNObject *ptr) {
break;
}

done:
done_3:
sz = potion_type_size(P, ptr);
return (void *)((char *)ptr + sz);
}
Expand Down
2 changes: 1 addition & 1 deletion core/internal.h
View file
Expand Up @@ -72,7 +72,7 @@ struct PNBHeader {
u8 minor;
u8 vmid;
u8 pn;
u8 proto[0];
u8 proto[];
};

size_t potion_cp_strlen_utf8(const char *);
Expand Down
12 changes: 10 additions & 2 deletions core/mt19937ar.c
View file
Expand Up @@ -117,12 +117,20 @@ static void next_state(void) {
left = N;
next = state;

for (j=N-M+1; --j; p++)
for (j=N-M+1; --j; p++) {
/*@ assert Value: mem_access: \valid_read(p+1); */
/*@ assert Value: mem_access: \valid_read(p+397); */
*p = p[M] ^ TWIST(p[0], p[1]);
}

for (j=M; --j; p++)
for (j=M; --j; p++) {
/*@ assert Value: mem_access: \valid_read(p+1); */
/*@ assert Value: mem_access: \valid_read(p+(int)(397-624)); */
*p = p[M-N] ^ TWIST(p[0], p[1]);
}

/*@ assert Value: mem_access: \valid(p); */
/*@ assert Value: mem_access: \valid_read(p+(int)(397-624)); */
*p = p[M-N] ^ TWIST(p[0], state[0]);
}

Expand Down
2 changes: 1 addition & 1 deletion core/objmodel.c
View file
Expand Up @@ -585,9 +585,9 @@ PN potion_lobby_say(Potion *P, PN cl, PN self) {
}

static void potion_init_class_reference(Potion *P, PN name, PN vt) {
char meta_str[strlen("<metaclass: >") + PN_STR_LEN(name) + 1];
potion_send(P->lobby, PN_def, name, vt);
((struct PNVtable *)vt)->name = name;
char meta_str[strlen("<metaclass: >") + PN_STR_LEN(name) + 1];
sprintf(meta_str, "<metaclass: %s>", PN_STR_PTR(name));
((struct PNVtable *)vt)->meta->name = potion_str(P, meta_str);
}
Expand Down
27 changes: 18 additions & 9 deletions core/potion.h
View file
Expand Up @@ -53,6 +53,7 @@ and optionally args, statically typed via signature strings.
#include <limits.h>
#include <string.h>
#include <fcntl.h>
#include <assert.h>
#include "config.h"
#if POTION_WIN32
# include <sys/stat.h>
Expand Down Expand Up @@ -229,7 +230,7 @@ struct PNVtable;
PNType vt; \
PNUniq uniq

#define PN_FLEX(N, T) typedef struct { PN_OBJECT_HEADER; PN_SIZE len; PN_SIZE siz; T ptr[0]; } N
#define PN_FLEX(N, T) typedef struct { PN_OBJECT_HEADER; PN_SIZE len; PN_SIZE siz; T ptr[]; } N
#define PN_FLEX_AT(N, I) ((PNFlex *)(N))->ptr[I]
#define PN_FLEX_SIZE(N) ((PNFlex *)(N))->len

Expand Down Expand Up @@ -297,7 +298,7 @@ struct PNVtable;
///
struct PNObject {
PN_OBJECT_HEADER; ///< PNType vt; PNUniq uniq
PN ivars[0];
PN ivars[];
};

///
Expand All @@ -320,7 +321,7 @@ struct PNFwd {
struct PNData {
PN_OBJECT_HEADER; ///< PNType vt; PNUniq uniq
PN_SIZE siz;
char data[0];
char data[];
};

///
Expand All @@ -331,7 +332,7 @@ struct PNData {
struct PNString {
PN_OBJECT_HEADER; ///< PNType vt; PNUniq uniq
PN_SIZE len;
char chars[0];
char chars[];
};

///
Expand All @@ -342,7 +343,7 @@ struct PNBytes {
PN_OBJECT_HEADER; ///< PNType vt; PNUniq uniq
PN_SIZE len;
PN_SIZE siz;
char chars[0];
char chars[];
};

/// PN_MANTISSA the last part of ->real
Expand Down Expand Up @@ -382,7 +383,7 @@ struct PNClosure {
int minargs; ///< cached number of mandatory args, without optional
PN_SIZE extra; ///< 0 or 1 if has code attached at data
PN name; /// PNString
PN data[0]; ///< code
PN data[]; ///< code
};

///
Expand Down Expand Up @@ -473,7 +474,7 @@ struct PNTuple {
PN_OBJECT_HEADER; ///< PNType vt; PNUniq uniq
PN_SIZE len;
PN_SIZE alloc; ///< overallocate a bit
PN set[0];
PN set[];
};

///
Expand Down Expand Up @@ -514,7 +515,7 @@ struct PNLick {
struct PNCont {
PN_OBJECT_HEADER; ///< PNType vt; PNUniq uniq
PN_SIZE len;
PN stack[0]; // [0] = head of potion stack
PN stack[]; // [0] = head of potion stack
// [1] = current %rsp
// [2] = current %rbp
// [3+] = full stack dump, ascending
Expand Down Expand Up @@ -562,7 +563,7 @@ static inline char *potion_str_ptr(PN s) {

PN_FLEX(PNFlex, PN);
//PN_FLEX(PNAsm, unsigned char);
typedef struct { PN_OBJECT_HEADER; PN_SIZE len; PN_SIZE siz; unsigned char ptr[0]; } PNAsm;
typedef struct { PN_OBJECT_HEADER; PN_SIZE len; PN_SIZE siz; unsigned char ptr[]; } PNAsm;

///
/// the jit
Expand Down Expand Up @@ -682,6 +683,14 @@ static inline void *potion_gc_alloc(Potion *P, PNType vt, int siz) {
if (siz < sizeof(struct PNFwd))
siz = sizeof(struct PNFwd);
siz = PN_ALIGN(siz, 8); // force 64-bit alignment
/*@ assert Value: mem_access: \valid_read(&M->dirty); */
/*@ assert
Value: ptr_comparison:
\pointer_comparable((char *)M->birth_cur+siz,
(char *)M->birth_storeptr-2); */
assert(M);
assert(M->birth_cur);
assert(M->birth_storeptr);
if (M->dirty || (char *)M->birth_cur + siz >= (char *)M->birth_storeptr - 2)
potion_garbagecollect(P, siz + 4 * sizeof(double), 0);
res = (struct PNObject *)M->birth_cur;
Expand Down
2 changes: 1 addition & 1 deletion core/table.h
View file
Expand Up @@ -40,7 +40,7 @@ struct PNVtable {
struct PNTable {
PN_OBJECT_HEADER; ///< PNType vt; PNUniq uniq
PN_TABLE_HEADER; ///< PN_SIZE n_buckets, size, n_occupied, upper_bound
char table[0];
char table[];
};

KHASH_MAP_INIT_PN(PN, struct PNTable)
Expand Down

0 comments on commit 74c0051

Please sign in to comment.