2021-02-24 19:15 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001939Frama-CKernel > libcpublic2016-01-26 13:33
Reportermansour 
Assigned Tomaroneze 
PrioritynormalSeverityfeatureReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Neon-20140301 
Target VersionFixed in VersionFrama-C Magnesium 
Summary0001939: Specification of the read function
DescriptionHi,

I think it would be useful to have a specification of common libc functions included with Frama-C (instead of repeating them in many projects), so I started with one for the read function.

I think it's complete, but I am still new to ACSL, so correct me if I'm wrong.

Please find attached the diff to the Neon version.

Yours,
Mansour
TagsNo tags attached.
Attached Files
  • patch file icon frama-c-Neon-20140301-read-spec.patch (4,633 bytes) 2014-10-19 21:09 -
    diff -Ndurp frama-c-Neon-20140301.orig/share/libc/__fc_define_ssize_max.h frama-c-Neon-20140301/share/libc/__fc_define_ssize_max.h
    --- frama-c-Neon-20140301.orig/share/libc/__fc_define_ssize_max.h	1969-12-31 19:00:00.000000000 -0500
    +++ frama-c-Neon-20140301/share/libc/__fc_define_ssize_max.h	2014-10-08 22:44:30.679246685 -0400
    @@ -0,0 +1,27 @@
    +/**************************************************************************/
    +/*                                                                        */
    +/*  This file is part of Frama-C.                                         */
    +/*                                                                        */
    +/*  Copyright (C) 2007-2014                                               */
    +/*    CEA (Commissariat à l'énergie atomique et aux énergies              */
    +/*         alternatives)                                                  */
    +/*                                                                        */
    +/*  you can redistribute it and/or modify it under the terms of the GNU   */
    +/*  Lesser General Public License as published by the Free Software       */
    +/*  Foundation, version 2.1.                                              */
    +/*                                                                        */
    +/*  It is distributed in the hope that it will be useful,                 */
    +/*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
    +/*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         */
    +/*  GNU Lesser General Public License for more details.                   */
    +/*                                                                        */
    +/*  See the GNU Lesser General Public License version 2.1                 */
    +/*  for more details (enclosed in the file licenses/LGPLv2.1).            */
    +/*                                                                        */
    +/**************************************************************************/
    +
    +#ifndef __FC_DEFINE_SSIZE_MAX
    +#define __FC_DEFINE_SSIZE_MAX
    +#include "__fc_machdep.h"
    +#define __SSIZE_MAX __FC_SSIZE_MAX
    +#endif
    diff -Ndurp frama-c-Neon-20140301.orig/share/libc/__fc_machdep.h frama-c-Neon-20140301/share/libc/__fc_machdep.h
    --- frama-c-Neon-20140301.orig/share/libc/__fc_machdep.h	2014-03-12 11:07:51.000000000 -0400
    +++ frama-c-Neon-20140301/share/libc/__fc_machdep.h	2014-10-08 22:44:30.683246685 -0400
    @@ -66,6 +66,8 @@
     /* stdint.h */
     #define __FC_PTRDIFF_MIN __FC_INT_MIN
     #define __FC_PTRDIFF_MAX __FC_INT_MAX
    +/* limits.h */
    +#define __FC_SSIZE_MAX __FC_INT_MAX
     
     #else
     #ifdef __FC_MACHDEP_X86_64
    @@ -144,6 +146,8 @@
     #define __FC_PTRDIFF_MIN __FC_LONG_MIN
     #define __FC_PTRDIFF_MAX __FC_LONG_MAX
     #else
    +/* limits.h */
    +#define __FC_SSIZE_MAX __FC_LONG_MAX
     
     #error Must define __FC_MACHDEP_X86_32 or __FC_MACHDEP_X86_64 or \
            __FC_MACHDEP_X86_16.
    diff -Ndurp frama-c-Neon-20140301.orig/share/libc/limits.h frama-c-Neon-20140301/share/libc/limits.h
    --- frama-c-Neon-20140301.orig/share/libc/limits.h	2014-03-12 11:07:51.000000000 -0400
    +++ frama-c-Neon-20140301/share/libc/limits.h	2014-10-08 22:44:30.707246686 -0400
    @@ -76,5 +76,8 @@
     /* Maximum value an `unsigned long long int' can hold.  (Minimum is 0.)  */
     #   define ULLONG_MAX	__FC_ULLONG_MAX
     
    +/* Maximum value an `ssize_t` can hold.  */
    +#   define SSIZE_MAX     __FC_SSIZE_MAX
    +
     #endif
     
    diff -Ndurp frama-c-Neon-20140301.orig/share/libc/unistd.h frama-c-Neon-20140301/share/libc/unistd.h
    --- frama-c-Neon-20140301.orig/share/libc/unistd.h	2014-03-12 11:07:51.000000000 -0400
    +++ frama-c-Neon-20140301/share/libc/unistd.h	2014-10-08 22:44:30.791246691 -0400
    @@ -32,6 +32,7 @@
     #include "__fc_define_useconds_t.h"
     #include "__fc_define_intptr_t.h"
     #include "__fc_select.h"
    +#include "__fc_define_ssize_max.h"
     
     #include <getopt.h>
     
    @@ -767,7 +768,19 @@ ssize_t      pread(int, void *, size_t,
     int          pthread_atfork(void (*)(void), void (*)(void),
                      void(*)(void));
     ssize_t      pwrite(int, const void *, size_t, off_t);
    -ssize_t      read(int, void *, size_t);
    +/*@ 
    +    requires \valid((char *) buf);
    +    requires nbyte <= __SSIZE_MAX;
    +    behavior success:
    +        assigns *((char *)buf + (0 .. nbyte - 1)) \from fd, nbyte;
    +        ensures 0 <= \result <= nbyte;
    +    behavior failure:
    +        ensures \result < 0;
    +        assigns \nothing;
    +    complete behaviors success, failure;
    +    disjoint behaviors success, failure;
    + */
    +ssize_t      read(int fd, void *buf, size_t nbyte);
     int          readlink(const char *, char *, size_t);
     int          rmdir(const char *);
     void        *sbrk(intptr_t);
    
    patch file icon frama-c-Neon-20140301-read-spec.patch (4,633 bytes) 2014-10-19 21:09 +

-Relationships
+Relationships

-Notes

~0005901

maroneze (administrator)

Thank you for the suggestions.

One of the issues in specifying (at least part of) the libc is that there's no consensus about the level of detail that would be useful/necessary for some people, and that would not be excessive for others.

For instance, several functions in the libc are stateful and would benefit from the introduction of model/ghost variables, but introducing too many of these imposes a burden on users who do not require such precision.

Still, it is likely that a few functions, such as read, will have a default specification in the next release of Frama-C. In the meanwhile, there is a question related to read on Stack Overflow (http://stackoverflow.com/questions/28439055/) which you may find useful.

~0005902

maroneze (administrator)

A few specifications will be present in the next release.
+Notes

-Issue History
Date Modified Username Field Change
2014-10-19 21:09 mansour New Issue
2014-10-19 21:09 mansour Status new => assigned
2014-10-19 21:09 mansour Assigned To => virgile
2014-10-19 21:09 mansour File Added: frama-c-Neon-20140301-read-spec.patch
2015-04-29 14:15 maroneze Assigned To virgile => maroneze
2015-04-29 15:07 maroneze Note Added: 0005901
2015-04-29 16:39 maroneze Note Added: 0005902
2015-04-29 16:39 maroneze Status assigned => resolved
2015-04-29 16:39 maroneze Resolution open => fixed
2015-07-17 08:35 signoles Category Kernel > ACSL implementation => Kernel > libc
2016-01-26 08:51 signoles Fixed in Version => Frama-C Magnesium
2016-01-26 08:52 signoles Status resolved => closed
+Issue History