--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on March 2009 ---
Hello, With following "check_lib.h": === source begin "check_lib.h" === /* copy/paste from /usr/include/* */ #define EINTR (-4) #define EXIT_FAILURE 1 #define EXIT_SUCCESS 0 #define O_RDONLY 00 int errno; /*@ assigns \nothing; */ void perror(char *); void exit(int err_code) { for(;;); } /*@ requires \valid(name); assigns \nothing; */ int open(char * name, int mode); /*@ requires fd >= 0; assigns \nothing; */ void close(int fd); === source end === I'm using following code: === source begin "exit_issue.c" === #include "check_lib.h" int main(void) { static int rand_fd = -1; rand_fd = open("/dev/random", O_RDONLY); if (rand_fd < 0) { perror("open"); exit(EXIT_FAILURE); } //@ assert rand_fd >= 0; close(rand_fd); return EXIT_SUCCESS; } === source end === In above code, using Alt-Ergo 0.8, alt-ergo is unable to prove property "assert rand_fd >= 0;". It seems obvious to me that the exit() function never terminates. So, the only case that goes past the "if (rand_fd < 0)" should be when "rand_fd >= 0", thus proving the assert clause. This is apparently not the case. What have I missed? I'm using following command line: frama-c -jessie-analysis -jessie-atp alt-ergo -jessie-gui exit_issue.c Sincerely yours, david