2020-12-05 00:27 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002498Frama-CPlug-in > wppublic2020-02-24 12:17
Reporteradbq 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
Platformamd64OSLinux DebianOS VersionBuster (10)
Product VersionFrama-C 20-Calcium 
Target VersionFixed in Version 
Summary0002498: munmap() breaks WP analysis
DescriptionWhen using unmap() glib function, WP stops analysis with a fatal error "User Error: Invalid infinite range p_1+(0..)".
Steps To Reproducemake frama-c, with appended code snippet.
TagsNo tags attached.
Attached Files
  • ? file icon Makefile (665 bytes) 2020-02-10 09:32 -
    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
    
    ? file icon Makefile (665 bytes) 2020-02-10 09:32 +
  • c file icon test4.c (1,281 bytes) 2020-02-24 12:17 -
    #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();
    }
    c file icon test4.c (1,281 bytes) 2020-02-24 12:17 +

-Relationships
+Relationships

-Notes
There are no notes attached to this issue.
+Notes

-Issue History
Date Modified Username Field Change
2020-02-10 09:32 adbq New Issue
2020-02-10 09:32 adbq Status new => assigned
2020-02-10 09:32 adbq Assigned To => correnson
2020-02-10 09:32 adbq File Added: Makefile
2020-02-24 12:17 adbq File Added: test4.c
+Issue History