Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Issue with non terminating function
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Mon, 2 Mar 2009 17:39:49 +0100
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