RiSE4fun samples for SLAyerList of built-in samples for the SLAyer in RiSE4funen-USrise4fun &copy; 2017 Microsoft Corporationhttp://rise4fun.com//Images/Rise.gifRiSE4fun samples for SLAyerhttp://rise4fun.com/SLAyer/free_localfree_local/* Free a stack variable. Expected result: POSSIBLY UNSAFE. */ #include "slayer.h" int main() { int x; free(&x); } http://rise4fun.com/SLAyer/deref_NULL2deref_NULL2/* Read from the un-allocated address 0. Expected result: POSSIBLY UNSAFE. */ #include "slayer.h" int main() { int x; int *y = 0; x = *y; } http://rise4fun.com/SLAyer/free_freefree_free/* Double free x. Expected result: POSSIBLY UNSAFE. */ #include "slayer.h" int main() { int *x = (int*)malloc(sizeof(int)); free(x); free(x); x = (int*)malloc(sizeof(int)); } http://rise4fun.com/SLAyer/mallocmalloc/* malloc and then leak x and y. Expected result: SAFE, MAY LEAK. */ #include "slayer.h" int main() { int *x = (int*)malloc(sizeof(int)); int *y = (int*)malloc(sizeof(int)); *x = 42; *y = 13; } http://rise4fun.com/SLAyer/malloc_free_structmalloc_free_struct/* malloc and then free a cell. Expected result: SAFE. */ #include "slayer.h" typedef struct cell cell; struct cell { int car; cell* cdr; }; int main() { cell *x = (cell*)malloc(sizeof(cell)); x->car = 42; x->cdr = 0; free(x); } http://rise4fun.com/SLAyer/if_pointerif_pointer/* Update x->car if x. Expected result: POSSIBLY UNSAFE. */ #include "slayer.h" typedef struct cell cell; struct cell { int car; cell* cdr; }; int main() { cell *x ; if (x) { x->car = x->car * 2 ; x->cdr = 0; } else { x = (cell*)malloc(sizeof(cell)); x->car = 0; } return 0; } http://rise4fun.com/SLAyer/createcreate/* Create and then leak a singly-linked list. Expected result: SAFE, MAY LEAK. */ #include "slayer.h" // Singly-linked lists. typedef struct _SLL_ENTRY { int Data; struct _SLL_ENTRY *Flink; } SLL_ENTRY, *PSLL_ENTRY; PSLL_ENTRY SLL_create(int length) { int i; PSLL_ENTRY head, tmp; head = NULL; for(i = 0; i < length; i++) { tmp = (PSLL_ENTRY)malloc(sizeof(SLL_ENTRY)); tmp->Flink = head; head = tmp; } return head; } void main(void) { PSLL_ENTRY head; head = SLL_create(nondet()); } http://rise4fun.com/SLAyer/reversereverse/* Create, reverse, then destroy a singly-linked list. Expected result: SAFE. */ #include "slayer.h" // Singly-linked lists. typedef struct _SLL_ENTRY { int Data; struct _SLL_ENTRY *Flink; } SLL_ENTRY, *PSLL_ENTRY; PSLL_ENTRY SLL_create(int length) { int i; PSLL_ENTRY head, tmp; head = NULL; for(i = 0; i < length; i++) { tmp = (PSLL_ENTRY)malloc(sizeof(SLL_ENTRY)); tmp->Flink = head; head = tmp; } return head; } void SLL_destroy_seg(PSLL_ENTRY x, PSLL_ENTRY y) { PSLL_ENTRY t; while(x != y) { t = x; x = x->Flink; free(t); } } void SLL_destroy(PSLL_ENTRY x) { SLL_destroy_seg(x, NULL); } /* Reverse the list pointed to by l. Implemented by poping off each item of *l into r. */ void reverse(PSLL_ENTRY *l) { PSLL_ENTRY c = *l, r = NULL; while(c != NULL) { PSLL_ENTRY t; t = c; c = c->Flink; t->Flink = r; r = t; } *l = r; } void main() { PSLL_ENTRY head; head = SLL_create(nondet()); reverse(&head); SLL_destroy(head); } http://rise4fun.com/SLAyer/copycopy/* Create, copy, then free a singly-linked list. Expected result: SAFE. */ #include "slayer.h" // Singly-linked lists. typedef struct _SLL_ENTRY { int Data; struct _SLL_ENTRY *Flink; } SLL_ENTRY, *PSLL_ENTRY; PSLL_ENTRY SLL_create(int length) { int i; PSLL_ENTRY head, tmp; head = NULL; for(i = 0; i < length; i++) { tmp = (PSLL_ENTRY)malloc(sizeof(SLL_ENTRY)); tmp->Flink = head; head = tmp; } return head; } void SLL_destroy_seg(PSLL_ENTRY x, PSLL_ENTRY y) { PSLL_ENTRY t; while(x != y) { t = x; x = x->Flink; free(t); } } void SLL_destroy(PSLL_ENTRY x) { SLL_destroy_seg(x, NULL); } PSLL_ENTRY copy(PSLL_ENTRY a) { PSLL_ENTRY y, x = a; SLL_ENTRY* * z = &y; while(x != NULL) /* listseg(y,*z) * listseg(-,x) * list(x) */ { *z = (SLL_ENTRY*)malloc(sizeof(SLL_ENTRY)); (*z)->Data = x->Data; z = &(*z)->Flink; x = x->Flink; } *z = NULL; return y; } void main() { PSLL_ENTRY x = NULL, y = NULL; x = SLL_create(nondet()); y = copy(x); SLL_destroy(x); SLL_destroy(y); }