--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on March 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Issue with non terminating function



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