SRC=test4.c

all:
	gcc $(SRC) -o test4

ADDONS= ~/.opam/default/share/frama-c/libc/string.c \
        ~/.opam/default/share/frama-c/libc/netdb.c 

JOBS:=$(shell nproc)
TIMEOUT:=10

frama-c:
	frama-c-gui $(SRC) $(ADDONS) -machdep x86_64 \
			-warn-left-shift-negative \
			-warn-right-shift-negative \
			-warn-signed-downcast \
			-warn-signed-overflow \
			-warn-unsigned-downcast \
			-warn-unsigned-overflow \
			-rte \
			-then \
			-eva \
			-eva-slevel 10000 \
			-eva-symbolic-locations-domain \
			-then \
			-wp \
			-wp-dynamic \
			-wp-no-init-const\
			-wp-par $(JOBS) \
			-wp-steps 100  -pp-annot \
			-wp-timeout $(TIMEOUT)


# eva-equility-domain 1

#include <stdio.h>
#include <unistd.h>
#include <stdlib.h>
#include <sys/types.h>
#include <sys/stat.h>
#include <fcntl.h>

#include <stdio.h>
#include <stdlib.h>
#include <errno.h>
#include <sys/types.h> 
#include <sys/socket.h>
#include <unistd.h>
#include <string.h>
#include <sys/mman.h>

//
// FRAMA-C bug: when assign something to this function, we get a WP user error at munmap
//

/*@ ensures \result >= 0;
  @ assigns __fc_errno;
*/
int bug()
{
    int fd;
    unsigned int i;
    int status = 0;
    struct stat statbuf = { 0 };
    char *p;
    char *entry;
    size_t memsize;

    /* open file */
    if ((fd = open("/etc/passwd", O_RDONLY)) < 1) { // errno
        printf("open()\n");
        return 1;
    }

	if (fstat(fd, &statbuf)) { // errno
		return 2;
	}

    memsize = (size_t)statbuf.st_size + 1000;

    /* maps the file*/
    if (!(p = (char *)mmap(NULL, memsize, PROT_READ|PROT_WRITE, MAP_PRIVATE, fd, 0))) {
        close(fd);
        return 4;
    }

    /* null bytes at the end */
    memset((unsigned char *)&p[statbuf.st_size], 0, 1000);

    /* wipe data containing sensitive info */
    memset(p, 0, memsize);
	munmap(p, memsize); // ************************************************ HERE
	close(fd);

    return status;
}



int main()
{
	bug();
}