From c348b51275d56861001237df23d5a35b8b3e505a Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Wed, 13 Nov 2019 15:20:09 +0100
Subject: [PATCH] [Libc] add specs in termios.h
---
share/libc/termios.h | 48 +++++++++++++--
tests/libc/oracle/fc_libc.0.res.oracle | 85 +++++++++++++-------------
tests/libc/oracle/fc_libc.1.res.oracle | 42 +++++++++++++
tests/libc/termios.c | 8 +++
4 files changed, 136 insertions(+), 47 deletions(-)
diff --git a/share/libc/termios.h b/share/libc/termios.h
index d53d69c2c61..ccaba4b7898 100644
--- a/share/libc/termios.h
+++ b/share/libc/termios.h
@@ -170,13 +170,51 @@ struct termios {
cc_t c_cc[NCCS]; /* special characters */
};
-extern speed_t cfgetispeed(const struct termios *);
-extern speed_t cfgetospeed(const struct termios *);
-extern int cfsetispeed(struct termios *, speed_t);
-extern int cfsetospeed(struct termios *, speed_t);
+/*@
+ requires valid_termios_p: \valid_read(termios_p);
+ assigns \result \from indirect:termios_p, *termios_p;
+ // missing ensures result_is_valid_speed: speed \in {valid baud rates};
+*/
+extern speed_t cfgetispeed(const struct termios *termios_p);
+
+/*@
+ requires valid_termios_p: \valid_read(termios_p);
+ assigns \result \from indirect:termios_p, *termios_p;
+ // missing ensures result_is_valid_speed: speed \in {valid baud rates};
+*/
+extern speed_t cfgetospeed(const struct termios *termios_p);
+
+/*@
+ // missing requires valid_speed: speed \in {valid baud rates};
+ requires valid_termios_p: \valid(termios_p);
+ assigns \result, *termios_p \from indirect:termios_p, speed;
+ ensures result_ok_or_error: \result == 0 || \result == -1;
+ */
+extern int cfsetispeed(struct termios *termios_p, speed_t speed);
+
+/*@
+ // missing requires valid_speed: speed \in {valid baud rates};
+ requires valid_termios_p: \valid(termios_p);
+ assigns \result, *termios_p \from indirect:termios_p, speed;
+ ensures result_ok_or_error: \result == 0 || \result == -1;
+ */
+extern int cfsetospeed(struct termios *termios_p, speed_t speed);
+
extern int tcdrain(int);
extern int tcflow(int, int);
-extern int tcflush(int, int);
+
+/*@
+ // missing requires valid_fd: {fd is an open file descriptor
+ // associated with a terminal};
+ requires valid_queue_selector: queue_selector == TCIFLUSH
+ || queue_selector == TCOFLUSH
+ || queue_selector == TCIOFLUSH;
+ assigns \result \from indirect:fd, indirect:queue_selector,
+ indirect:Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ ensures result_ok_or_error: \result == 0 || \result == -1;
+ */
+extern int tcflush(int fd, int queue_selector);
/*@ requires valid_termios_p: \valid(termios_p);
assigns \result, *termios_p \from indirect:fd,
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index d64b91d8754..4576d6a15ca 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -40,7 +40,7 @@
unsetenv (0 call); wcscat (0 call); wcscpy (0 call); wcslen (2 calls);
wcsncat (0 call); wcsncpy (0 call); wmemcpy (0 call); wmemset (0 call);
- Undefined functions (385)
+ Undefined functions (390)
=========================
FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
Frama_C_int_interval (0 call); Frama_C_long_interval (0 call);
@@ -74,35 +74,36 @@
atanl (0 call); atexit (0 call); atof (0 call); atol (0 call);
atoll (0 call); basename (0 call); bind (0 call); bsearch (0 call);
bzero (0 call); ceil (0 call); ceilf (0 call); ceill (0 call);
- chdir (0 call); chown (0 call); chroot (0 call); clearerr (0 call);
- clearerr_unlocked (0 call); clock (0 call); clock_gettime (0 call);
- clock_nanosleep (0 call); close (0 call); closedir (0 call);
- closelog (0 call); connect (0 call); cos (0 call); cosf (0 call);
- cosl (0 call); creat (0 call); ctime (0 call); difftime (0 call);
- dirname (0 call); div (0 call); drand48 (0 call); dup (0 call);
- dup2 (0 call); erand48 (0 call); execl (0 call); execle (0 call);
- execlp (0 call); execv (0 call); execve (0 call); execvp (0 call);
- exit (0 call); exp (0 call); expf (0 call); fabsl (0 call); fclose (0 call);
- fcntl (0 call); fdopen (0 call); feof (2 calls); feof_unlocked (0 call);
- ferror (2 calls); ferror_unlocked (0 call); fflush (0 call); fgetc (1 call);
- fgetpos (0 call); fgets (0 call); fgetws (0 call); fileno (0 call);
- fileno_unlocked (0 call); flock (0 call); flockfile (0 call);
- floor (0 call); floorf (0 call); floorl (0 call); fmod (0 call);
- fmodf (0 call); fopen (0 call); fork (0 call); fputc (0 call);
- fputs (0 call); fread (0 call); free (1 call); freeaddrinfo (0 call);
- freopen (0 call); fseek (0 call); fsetpos (0 call); ftell (0 call);
- ftrylockfile (0 call); funlockfile (0 call); fwrite (0 call);
- gai_strerror (0 call); getc (0 call); getc_unlocked (0 call);
- getchar (0 call); getchar_unlocked (0 call); getcwd (0 call);
- getegid (0 call); geteuid (0 call); getgid (0 call); gethostname (0 call);
- getitimer (0 call); getopt (0 call); getopt_long (0 call);
- getopt_long_only (0 call); getpgid (0 call); getpgrp (0 call);
- getpid (0 call); getppid (0 call); getpriority (0 call); getpwnam (0 call);
- getpwuid (0 call); getresgid (0 call); getresuid (0 call);
- getrlimit (0 call); getrusage (0 call); gets (0 call); getsid (0 call);
- getsockname (0 call); getsockopt (0 call); gettimeofday (0 call);
- getuid (0 call); gmtime (0 call); htonl (0 call); htons (0 call);
- iconv (0 call); iconv_close (0 call); iconv_open (0 call);
+ cfgetispeed (0 call); cfgetospeed (0 call); cfsetispeed (0 call);
+ cfsetospeed (0 call); chdir (0 call); chown (0 call); chroot (0 call);
+ clearerr (0 call); clearerr_unlocked (0 call); clock (0 call);
+ clock_gettime (0 call); clock_nanosleep (0 call); close (0 call);
+ closedir (0 call); closelog (0 call); connect (0 call); cos (0 call);
+ cosf (0 call); cosl (0 call); creat (0 call); ctime (0 call);
+ difftime (0 call); dirname (0 call); div (0 call); drand48 (0 call);
+ dup (0 call); dup2 (0 call); erand48 (0 call); execl (0 call);
+ execle (0 call); execlp (0 call); execv (0 call); execve (0 call);
+ execvp (0 call); exit (0 call); exp (0 call); expf (0 call); fabsl (0 call);
+ fclose (0 call); fcntl (0 call); fdopen (0 call); feof (2 calls);
+ feof_unlocked (0 call); ferror (2 calls); ferror_unlocked (0 call);
+ fflush (0 call); fgetc (1 call); fgetpos (0 call); fgets (0 call);
+ fgetws (0 call); fileno (0 call); fileno_unlocked (0 call); flock (0 call);
+ flockfile (0 call); floor (0 call); floorf (0 call); floorl (0 call);
+ fmod (0 call); fmodf (0 call); fopen (0 call); fork (0 call);
+ fputc (0 call); fputs (0 call); fread (0 call); free (1 call);
+ freeaddrinfo (0 call); freopen (0 call); fseek (0 call); fsetpos (0 call);
+ ftell (0 call); ftrylockfile (0 call); funlockfile (0 call);
+ fwrite (0 call); gai_strerror (0 call); getc (0 call);
+ getc_unlocked (0 call); getchar (0 call); getchar_unlocked (0 call);
+ getcwd (0 call); getegid (0 call); geteuid (0 call); getgid (0 call);
+ gethostname (0 call); getitimer (0 call); getopt (0 call);
+ getopt_long (0 call); getopt_long_only (0 call); getpgid (0 call);
+ getpgrp (0 call); getpid (0 call); getppid (0 call); getpriority (0 call);
+ getpwnam (0 call); getpwuid (0 call); getresgid (0 call);
+ getresuid (0 call); getrlimit (0 call); getrusage (0 call); gets (0 call);
+ getsid (0 call); getsockname (0 call); getsockopt (0 call);
+ gettimeofday (0 call); getuid (0 call); gmtime (0 call); htonl (0 call);
+ htons (0 call); iconv (0 call); iconv_close (0 call); iconv_open (0 call);
inet_addr (2 calls); inet_ntoa (0 call); inet_ntop (0 call);
inet_pton (0 call); isascii (0 call); isatty (0 call); jrand48 (0 call);
kill (0 call); killpg (0 call); labs (0 call); lcong48 (0 call);
@@ -146,17 +147,17 @@
strtoimax (0 call); strtok (0 call); strtok_r (0 call); strtol (0 call);
strtold (0 call); strtoll (0 call); strtoul (0 call); strtoull (0 call);
strxfrm (0 call); sync (0 call); sysconf (0 call); syslog (0 call);
- system (0 call); tcgetattr (0 call); tcsetattr (0 call); time (0 call);
- times (0 call); tmpfile (0 call); tmpnam (0 call); trunc (0 call);
- truncf (0 call); truncl (0 call); ttyname (0 call); tzset (0 call);
- umask (0 call); ungetc (0 call); unlink (0 call); usleep (0 call);
- utimes (0 call); vfprintf (0 call); vfscanf (0 call); vprintf (0 call);
- vscanf (0 call); vsnprintf (0 call); vsprintf (0 call); vsyslog (0 call);
- wait (0 call); waitpid (0 call); wcschr (0 call); wcscmp (0 call);
- wcscspn (0 call); wcslcat (0 call); wcslcpy (0 call); wcsncmp (0 call);
- wcspbrk (0 call); wcsrchr (0 call); wcsspn (0 call); wcsstr (0 call);
- wcstombs (0 call); wctomb (0 call); wmemchr (0 call); wmemcmp (0 call);
- wmemmove (0 call); write (0 call);
+ system (0 call); tcflush (0 call); tcgetattr (0 call); tcsetattr (0 call);
+ time (0 call); times (0 call); tmpfile (0 call); tmpnam (0 call);
+ trunc (0 call); truncf (0 call); truncl (0 call); ttyname (0 call);
+ tzset (0 call); umask (0 call); ungetc (0 call); unlink (0 call);
+ usleep (0 call); utimes (0 call); vfprintf (0 call); vfscanf (0 call);
+ vprintf (0 call); vscanf (0 call); vsnprintf (0 call); vsprintf (0 call);
+ vsyslog (0 call); wait (0 call); waitpid (0 call); wcschr (0 call);
+ wcscmp (0 call); wcscspn (0 call); wcslcat (0 call); wcslcpy (0 call);
+ wcsncmp (0 call); wcspbrk (0 call); wcsrchr (0 call); wcsspn (0 call);
+ wcsstr (0 call); wcstombs (0 call); wctomb (0 call); wmemchr (0 call);
+ wmemcmp (0 call); wmemmove (0 call); write (0 call);
'Extern' global variables (16)
==============================
@@ -179,7 +180,7 @@
Goto = 89
Assignment = 438
Exit point = 82
- Function = 467
+ Function = 472
Function call = 89
Pointer dereferencing = 158
Cyclomatic complexity = 286
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 82cff401f47..26025f53b3f 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -365,6 +365,7 @@ struct tms {
};
typedef unsigned int tcflag_t;
typedef unsigned char cc_t;
+typedef unsigned int speed_t;
struct termios {
tcflag_t c_iflag ;
tcflag_t c_oflag ;
@@ -7935,6 +7936,47 @@ extern pid_t wait(int *stat_loc);
*/
extern pid_t waitpid(pid_t pid, int *stat_loc, int options);
+/*@ requires valid_termios_p: \valid_read(termios_p);
+ assigns \result;
+ assigns \result \from (indirect: termios_p), *termios_p;
+ */
+extern speed_t cfgetispeed(struct termios const *termios_p);
+
+/*@ requires valid_termios_p: \valid_read(termios_p);
+ assigns \result;
+ assigns \result \from (indirect: termios_p), *termios_p;
+ */
+extern speed_t cfgetospeed(struct termios const *termios_p);
+
+/*@ requires valid_termios_p: \valid(termios_p);
+ ensures result_ok_or_error: \result â‰، 0 ∨ \result â‰، -1;
+ assigns \result, *termios_p;
+ assigns \result \from (indirect: termios_p), speed;
+ assigns *termios_p \from (indirect: termios_p), speed;
+ */
+extern int cfsetispeed(struct termios *termios_p, speed_t speed);
+
+/*@ requires valid_termios_p: \valid(termios_p);
+ ensures result_ok_or_error: \result â‰، 0 ∨ \result â‰، -1;
+ assigns \result, *termios_p;
+ assigns \result \from (indirect: termios_p), speed;
+ assigns *termios_p \from (indirect: termios_p), speed;
+ */
+extern int cfsetospeed(struct termios *termios_p, speed_t speed);
+
+/*@ requires
+ valid_queue_selector:
+ queue_selector â‰، 0 ∨ queue_selector â‰، 1 ∨
+ queue_selector â‰، 2;
+ ensures result_ok_or_error: \result â‰، 0 ∨ \result â‰، -1;
+ assigns \result, Frama_C_entropy_source;
+ assigns \result
+ \from (indirect: fd), (indirect: queue_selector),
+ (indirect: Frama_C_entropy_source);
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+extern int tcflush(int fd, int queue_selector);
+
/*@ requires valid_termios_p: \valid(termios_p);
assigns \result, *termios_p, Frama_C_entropy_source;
assigns \result \from (indirect: fd), (indirect: Frama_C_entropy_source);
diff --git a/tests/libc/termios.c b/tests/libc/termios.c
index 9f3928b7f8f..6ba105607a2 100644
--- a/tests/libc/termios.c
+++ b/tests/libc/termios.c
@@ -15,5 +15,13 @@ int main() {
}
tio.c_lflag = (ECHO|ICANON|ISIG|ECHOE|ECHOK|ECHONL);
tio.c_oflag = OPOST;
+
+ res = cfsetispeed(&tio, B9600);
+ if (res) return 1;
+ res = cfsetospeed(&tio, B50);
+ if (res) return 1;
+ speed_t sp1 = cfgetispeed(&tio);
+ speed_t sp2 = cfgetospeed(&tio);
+ res = tcflush(fd, TCIOFLUSH);
return tcsetattr(fd, TCSADRAIN, &tio);
}
--
GitLab