diff --git a/cgc-challenges/old_stubs/README.md b/cgc-challenges/old_stubs/README.md
new file mode 100644
index 0000000000000000000000000000000000000000..1ce64866eae42b83400089374af5759e1a0476c1
--- /dev/null
+++ b/cgc-challenges/old_stubs/README.md
@@ -0,0 +1,2 @@
+# These stubs are only for reference; copy and fix them when adding new case
+# studies.
diff --git a/cgc-challenges/old_stubs/fc_stubs.c b/cgc-challenges/old_stubs/fc_stubs.c
new file mode 100644
index 0000000000000000000000000000000000000000..3b525737eddace642c55c5c84c8255459827f091
--- /dev/null
+++ b/cgc-challenges/old_stubs/fc_stubs.c
@@ -0,0 +1,79 @@
+#include "__fc_define_size_t.h"
+#include "__fc_define_off_t.h"
+#include "__fc_define_file.h"
+#include "__fc_builtin.h"
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <unistd.h>
+
+static volatile int v;
+
+int cgc_putenv(const char *name, const unsigned char *val, size_t val_len) {
+ return setenv(name, (char*)val, 1);
+}
+
+unsigned char *cgc_getenv(const char *name, size_t *len) {
+ char *p = (unsigned char*) getenv(name);
+ if (p) {
+ size_t n = strlen(p)+1;
+ unsigned char *newstr = malloc(n);
+ strcpy((char*)newstr, p);
+ *len = n;
+ return newstr;
+ }
+ return 0;
+}
+
+void *cgc_calloc(size_t size) {
+ void *p = malloc(size);
+ bzero(p, size);
+ return p;
+}
+
+#include "libcgc.h"
+
+int cgc_write3( int fd, void *buffer, size_t count ) {
+ size_t written;
+ int total_written;
+ int retval;
+
+ written = 0;
+ total_written = 0;
+
+ while (total_written < count) {
+ retval = cgc_transmit(fd, ((char*)buffer)+total_written,
+ count-total_written, &written);
+ if (retval != 0)
+ return(-1);
+
+ total_written+=written;
+ }
+ return(count);
+
+}
+
+ssize_t cgc_fread3(void *ptr, size_t size, FILE *stream) {
+ size_t r = fread(ptr, size, 1, stream);
+ if (v) return -1;
+ else return Frama_C_interval(0, size * 8);
+}
+
+ssize_t cgc_fwrite3(const void *ptr, size_t size, FILE *stream) {
+ size_t r = fwrite(ptr, size, 1, stream);
+ if (v) return -1;
+ else return r;
+}
+
+void cgc_bzero_Pv_i(void *s, int n) {
+ bzero(s, n);
+}
+
+// Frama-C/Eva does not yet have a way to model mmap() or page permissions,
+// so for now we model allocate() via malloc()
+/*@ requires valid_addr: \valid((char*)*addr); */
+int cgc_allocate(size_t length, int is_X, void **addr) {
+ *addr = malloc(length);
+ if (!*addr) return 1;
+ else return 0;
+}
diff --git a/cgc-challenges/old_stubs/fc_stubs.h b/cgc-challenges/old_stubs/fc_stubs.h
new file mode 100644
index 0000000000000000000000000000000000000000..cb85d74a4e760749ad2f3e1a983c3909f7784ca8
--- /dev/null
+++ b/cgc-challenges/old_stubs/fc_stubs.h
@@ -0,0 +1,401 @@
+#define cgc_abs abs
+#define cgc_atoi atoi
+#define cgc_calloc2 calloc
+#define cgc_exit exit
+#define cgc_fdprintf(...)
+#define cgc_fabs fabs
+#define cgc_pow pow
+#define cgc_sin sin
+#define cgc_sqrt sqrt
+#define cgc_tan tan
+#define cgc_free free
+#define cgc_isalnum isalnum
+#define cgc_isalpha isalpha
+#define cgc_isdigit isdigit
+#define cgc_islower islower
+#define cgc_isspace isspace
+#define cgc_isupper isupper
+#define cgc_isxdigit isxdigit
+#define cgc_tolower tolower
+#define cgc_toupper toupper
+#ifndef MALLOC_IS_CALLOC
+#define cgc_malloc malloc
+#endif
+#define cgc_memchr memchr
+#define cgc_memcmp memcmp
+#define cgc_memcpy memcpy
+#define cgc_memmove memmove
+#define cgc_memset memset
+#define cgc_printf printf
+#define cgc_realloc realloc
+#define cgc_snprintf snprintf
+#define cgc_sprintf sprintf
+#define cgc_strcasecmp strcasecmp
+#define cgc_strcat strcat
+#define cgc_strchr strchr
+#define cgc_strcmp strcmp
+#define cgc_strcpy strcpy
+#define cgc_strdup strdup
+#define cgc_strlen strlen
+#define cgc_strncat strncat
+#define cgc_strncmp strncmp
+#define cgc_strncpy strncpy
+#define cgc_strnlen strnlen
+#define cgc_strrchr strrchr
+#define cgc_getchar getchar
+
+#define cgc_stdin stdin
+#define cgc_stdout stdout
+#define cgc_stderr stderr
+
+/*@ assigns \result \from indirect:pStr, indirect:pStr[0..]; */
+double cgc_atof( char *pStr );
+
+#define SUCCESS 0
+#define FAILURE 1
+#define TRUE 1
+#define FALSE 0
+
+#include <stdlib.h>
+#include <string.h>
+#include <stdint.h>
+#include <stdio.h>
+#include <ctype.h>
+
+#include <sys/types.h>
+/*@
+ requires \valid(result);
+ assigns \result \from indirect:str, indirect:str[0..], indirect:base;
+ assigns *result \from indirect:str, indirect:str[0..], indirect:base;
+*/
+ssize_t cgc_strtoi(char *str, unsigned int base, int *result);
+
+/*@
+ requires \valid_read(str);
+ assigns \result \from indirect:str, indirect:str[0..], indirect:endptr,
+ indirect:*endptr, indirect:base;
+*/
+long cgc_strtol(const char *str, char **endptr, int base);
+
+/*@
+ requires \valid_read(str);
+ assigns \result \from indirect:str, indirect:str[0..], indirect:endptr,
+ indirect:*endptr, indirect:base;
+*/
+unsigned long cgc_strtoul(const char *str, char **endptr, int base);
+
+/*@
+ requires \valid(s);
+ assigns s[0..] \from indirect:val;
+ assigns \result \from s;
+ ensures \result == \null || \result == s;
+ */
+char *cgc_itoa(int val, char *s);
+
+/*@
+ requires \valid(buf);
+ assigns buf[0..] \from indirect:val;
+ */
+void cgc_int_to_str( int val, char *buf );
+
+
+#include "__fc_string_axiomatic.h"
+
+/*@
+ requires *stringp == \null || \valid(*stringp);
+ requires valid_read_string(delim);
+ assigns *stringp[0..] \from indirect:*stringp[0..], indirect:delim[0..];
+ assigns \result \from *stringp;
+ ensures \result == \null || \subset(\result, *stringp+(0..));
+ */
+char *cgc_strsep(char **stringp, const char *delim);
+
+#include "__fc_define_file.h"
+
+/*@
+ assigns *stream \from indirect:enabled;
+ */
+void cgc_fbuffered(FILE *stream, int enabled);
+
+/*@
+ assigns \result, *stream \from indirect:stream;
+ */
+int cgc_fflush(FILE *stream);
+
+/*@
+ requires \valid_read(((char*)ptr)+(0..size-1));
+ assigns \result \from indirect:fd, indirect:ptr, indirect:size;
+ ensures \result == size || \result == EXIT_FAILURE;
+ */
+ssize_t cgc_write_all(int fd, const void *ptr, size_t size);
+
+/*@
+ requires \valid_read(((char*)ptr)+(0..size-1));
+ assigns \result \from indirect:ptr, indirect:size;
+ ensures \result == size || \result == EXIT_FAILURE;
+ */
+ssize_t cgc_write_Pcv_sz(const void *ptr, size_t size);
+
+/*@
+ requires \valid_read(((char*)ptr)+(0..size-1));
+ assigns \result \from indirect:stream, indirect:size;
+ */
+ssize_t cgc_fwrite3(const void *ptr, size_t size, FILE *stream);
+
+/*@
+ requires \valid(((char*)ptr)+(0..size-1));
+ assigns \result, ((char*)ptr)[0..size-1] \from indirect:fd, indirect:delim,
+ indirect:size;
+ */
+ssize_t cgc_read_until4(int fd, void *ptr, unsigned char delim, size_t size);
+
+/*@
+ requires \valid(buf+(0..max-1));
+ assigns buf[0..max-1] \from indirect:delim, indirect:max;
+ assigns \result \from indirect:delim, indirect:max;
+*/
+ssize_t cgc_read_until3(char *buf, char *delim, size_t max);
+
+/*@
+ requires \valid(((char*)ptr)+(0..size-1));
+ assigns \result, ((char*)ptr)[0..size-1] \from indirect:delim, indirect:size,
+ indirect:stream;
+ */
+ssize_t cgc_fread_until(void *ptr, unsigned char delim, size_t size,
+ FILE *stream);
+
+/*@
+ requires \valid(str+(0..size-1));
+ assigns \result, str[0..size-1] \from indirect: size, indirect: term,
+ indirect:stream;
+ */
+ssize_t cgc_freaduntil(char *str, size_t size, char term, FILE *stream);
+
+/*@
+ requires \valid(((char*)ptr)+(0..size-1));
+ assigns \result, ((char*)ptr)[0..size-1] \from indirect:size, indirect:stream;
+ */
+ssize_t cgc_fread3(void *ptr, size_t size, FILE *stream);
+
+/*@
+ requires \valid(((char*)ptr)+(0..(size*nmemb)-1));
+ assigns \result, ((char*)ptr)[0..(size*nmemb)-1]
+ \from indirect:size, indirect:nmemb, indirect:stream;
+ */
+int cgc_fread4(void *ptr, size_t size, size_t nmemb, FILE *stream);
+
+/*@
+ requires \valid(s+(0..size-1));
+ assigns s[0..size-1] \from indirect:stream;
+ assigns \result \from s;
+ ensures \result == \null || \result == s;
+*/
+char *cgc_fgets3(char *s, int size, FILE *stream);
+
+/*@
+ requires \valid(str_buf+(0..buf_size-1));
+ assigns str_buf[0..buf_size-1] \from indirect:buf_size, indirect:i;
+ assigns \result \from indirect:buf_size, indirect:i;
+*/
+int cgc_int2str(char* str_buf, int buf_size, int i);
+
+/*@
+ requires \valid(str_buf+(0..buf_size-1));
+ assigns str_buf[0..buf_size-1] \from indirect:i;
+ assigns \result \from indirect:buf_size, indirect:i;
+ */
+int cgc_uint2str(char* str_buf, int buf_size, uint32_t i);
+
+/*@
+ requires valid_read_string(str_buf);
+ assigns \result \from indirect:str_buf[0..];
+ */
+uint32_t cgc_str2uint(const char* str_buf);
+
+/*@
+ requires \valid(buf+(0..size-1));
+ assigns buf[0..size-1] \from indirect:fd, indirect:size;
+ assigns \result \from indirect: fd, size;
+*/
+int cgc_recvline(int fd, char *buf, size_t size);
+
+/*@
+ requires \valid(buf+(0..size-1));
+ assigns buf[0..size-1] \from indirect:fd, indirect:size;
+ assigns \result \from indirect: fd, size;
+*/
+int cgc_recv(int fd, char *buf, size_t size);
+
+/*@
+ requires \valid(res_buf+(0..res_buf_size-1));
+ assigns res_buf[0..res_buf_size-1] \from indirect:res_buf_size;
+ */
+unsigned int cgc_recv_all2(char *res_buf, size_t res_buf_size);
+
+/*@
+ requires \valid_read(buf+(0..size-1));
+ assigns \result \from indirect:fd, indirect:size;
+*/
+int cgc_transmit_all3(int fd, const char *buf, const size_t size);
+
+/*@
+ requires valid_read_string(s);
+ assigns \result \from indirect:fd, indirect:s[0..];
+*/
+int cgc_transmit_str(int fd, char *s);
+
+/*@
+ requires \valid(dst+(0..max-1));
+ assigns dst[0..max-1] \from indirect:delim, indirect:max;
+ assigns \result \from indirect:delim, indirect:max;
+*/
+size_t cgc_receive_until( char *dst, char delim, size_t max );
+
+/*@
+ requires \valid(buf+(0..size-1));
+ assigns buf[0..size-1] \from indirect:fd, indirect:delim, indirect:size;
+ assigns \result \from indirect:fd, indirect:delim, indirect:size;
+ */
+int cgc_receive_delim(int fd, char *buf, const size_t size, char delim);
+
+/*@
+ requires \valid(buffer+(0..count-1));
+ assigns buffer[0..count-1] \from indirect:count;
+ assigns \result \from indirect:count;
+*/
+int cgc_receive_bytes2(char *buffer, size_t count);
+
+/*@
+ requires \valid(buf+(0..size-1));
+ assigns buf[0..size-1] \from indirect:fd, indirect:delim, indirect:size;
+ assigns \result \from indirect:fd, indirect:delim, indirect:size;
+ */
+ssize_t cgc_recv_until_delim_n(int fd, char delim, char *buf,
+ unsigned int size);
+
+/*@
+ requires \valid(buf+(0..size-1));
+ assigns buf[0..size-1] \from indirect:fd, indirect:delim, indirect:size;
+ assigns \result \from indirect:fd, indirect:delim, indirect:size;
+ */
+int cgc_recv_until_delim(int fd, char *buf, size_t size, char delim);
+
+/*@
+ requires \valid(buf+(0..len-1));
+ assigns buf[0..len-1] \from indirect:fd, indirect:len;
+ assigns \result \from indirect:fd, indirect:len;
+*/
+ssize_t cgc_readLine(int fd, char* buf, size_t len);
+
+/*@
+ requires \valid(((char*)buf)+(0..size-1));
+ assigns ((char*)buf)[0..size-1] \from indirect:fd, indirect:size;
+ assigns \result \from indirect:size, indirect:fd;
+*/
+unsigned int cgc_read_all(int fd, void *buf, unsigned int size);
+
+/*@
+ requires \valid(buffer+(0..size-1));
+ requires cgc_read == \null || \valid(cgc_read);
+ assigns \result \from indirect:socket, indirect:delim, indirect:size;
+ assigns buffer[0..size-1] \from indirect:socket, indirect:delim,
+ indirect:size;
+ assigns cgc_read == \null ? \empty : *cgc_read \from indirect:socket,
+ indirect:delim,
+ indirect:size;
+*/
+int cgc_read_until_delim_or_n(unsigned int socket, char* buffer, char delim,
+ size_t size, size_t* cgc_read);
+
+/*@
+ assigns \result \from base, exponent;
+ */
+int cgc_expi( int base, int exponent);
+
+/*@
+ assigns \result \from x;
+ */
+float cgc_exp2f(float x);
+
+/*@
+ assigns \result \from x;
+ */
+float cgc_sqrtf(float x);
+
+/*@
+ requires \valid_read(buf+(0..size-1));
+ assigns \result \from indirect:fd, indirect:buf[0..size-1], indirect:size;
+ */
+int cgc_sendline(int fd, const char *buf, size_t size);
+
+/*@
+ requires \valid_read(buf+(0..size-1));
+ assigns \result \from indirect:buf[0..size-1], indirect:size;
+*/
+int cgc_send2(const char *buf, const size_t size);
+
+/*@
+ requires valid_read_string(t);
+ assigns \nothing;
+ */
+void cgc_puts( char *t );
+
+/*@
+ assigns \result \from indirect:str[0..];
+ */
+double cgc_cgcatof(const char* str);
+
+/*@
+ requires str == \null || valid_string(str);
+ requires valid_read_string(delim);
+ assigns \result \from str;
+ assigns str == \null ? \empty : str[0..] \from indirect:delim[0..];
+ */
+char *cgc_strtok_const(char *str, const char *delim);
+
+/*@
+ requires s == \null || valid_string(s);
+ assigns \result \from s;
+ assigns s == \null ? \empty : s[0..] \from indirect:d;
+ */
+char *cgc_strtok_int(char *s, int d);
+
+/*@
+ assigns \result \from min, max;
+ ensures min <= \result <= max;
+ */
+uint32_t cgc_random_in_range(uint32_t min, uint32_t max);
+
+/*@
+ assigns \result \from v;
+ */
+char cgc_to_hex(unsigned char v);
+
+/*@
+ assigns \result \from c;
+ */
+unsigned char cgc_to_bin(char c);
+
+#include "ansi_x931_aes128.h"
+/*@
+ requires \valid(prng);
+ assigns *prng \from *seed;
+ */
+void cgc_init_prng(cgc_prng* prng, const cgc_aes_state* seed);
+
+/*@
+ requires \valid(prng);
+ requires \valid(buf+(0..len-1));
+ assigns buf[0..len-1] \from indirect:*prng, indirect:len;
+ assigns *prng \from *prng;
+ */
+void cgc_aes_get_bytes(cgc_prng *prng, uint32_t len, uint8_t *buf);
+
+// used for calls to printf with non-static format strings
+/*@
+ requires valid_read_string(s);
+ assigns \result \from indirect:s;
+ */
+int cgc_printf_s(const char *s);
+
+void cgc_bzero_Pv_i(void *s, int n);