Skip to content
Snippets Groups Projects
Commit 64205cb6 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

Merge branch 'master' into feature/rte/extern-api

parents 861f1bf8 89bd69af
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 164 additions and 321 deletions
.Makefile.lint
+ 0
− 6
View file @ 64205cb6
......@@ -101,8 +101,6 @@ ML_LINT_KO+=src/kernel_services/ast_printing/cil_types_debug.ml
ML_LINT_KO+=src/kernel_services/ast_printing/cil_types_debug.mli
ML_LINT_KO+=src/kernel_services/ast_printing/cprint.ml
ML_LINT_KO+=src/kernel_services/ast_printing/cprint.mli
ML_LINT_KO+=src/kernel_services/ast_printing/description.ml
ML_LINT_KO+=src/kernel_services/ast_printing/description.mli
ML_LINT_KO+=src/kernel_services/ast_printing/logic_print.ml
ML_LINT_KO+=src/kernel_services/ast_printing/printer.ml
ML_LINT_KO+=src/kernel_services/ast_printing/printer_api.mli
......@@ -194,8 +192,6 @@ ML_LINT_KO+=src/libraries/stdlib/FCSet.ml
ML_LINT_KO+=src/libraries/stdlib/FCSet.mli
ML_LINT_KO+=src/libraries/stdlib/extlib.ml
ML_LINT_KO+=src/libraries/stdlib/extlib.mli
ML_LINT_KO+=src/libraries/stdlib/integer.ml
ML_LINT_KO+=src/libraries/stdlib/integer.mli
ML_LINT_KO+=src/libraries/utils/bag.ml
ML_LINT_KO+=src/libraries/utils/binary_cache.ml
ML_LINT_KO+=src/libraries/utils/bitvector.ml
......@@ -222,8 +218,6 @@ ML_LINT_KO+=src/libraries/utils/qstack.ml
ML_LINT_KO+=src/libraries/utils/qstack.mli
ML_LINT_KO+=src/libraries/utils/rangemap.ml
ML_LINT_KO+=src/libraries/utils/rangemap.mli
ML_LINT_KO+=src/libraries/utils/rich_text.ml
ML_LINT_KO+=src/libraries/utils/rich_text.mli
ML_LINT_KO+=src/libraries/utils/task.ml
ML_LINT_KO+=src/libraries/utils/task.mli
ML_LINT_KO+=src/libraries/utils/vector.ml
......
Makefile
+ 6
− 6
View file @ 64205cb6
......@@ -188,7 +188,7 @@ THEME_ICONS_FLAT:= \
$(addprefix share/theme/flat/,$(THEME_ICON_NAMES))
ROOT_LIBC_DIR:= share/libc
LIBC_SUBDIRS:= sys netinet linux net arpa
LIBC_SUBDIRS:= sys netinet net arpa
LIBC_DIR:= $(ROOT_LIBC_DIR) $(addprefix $(ROOT_LIBC_DIR)/,$(LIBC_SUBDIRS))
LIBC_FILES:= \
$(wildcard share/*.h share/*.c) \
......@@ -576,6 +576,7 @@ KERNEL_CMO=\
src/kernel_services/abstract_interp/lmap_bitwise.cmo \
src/kernel_services/visitors/visitor.cmo \
src/kernel_services/ast_data/statuses_by_call.cmo \
src/kernel_services/ast_printing/printer_tag.cmo \
$(PLUGIN_TYPES_CMO_LIST) \
src/kernel_services/plugin_entry_points/db.cmo \
src/libraries/utils/command.cmo \
......@@ -732,6 +733,7 @@ endif
GENERATED+=src/plugins/gui/gtk_compat.ml
SINGLE_GUI_CMO:= \
wutil_once \
gtk_compat \
$(WTOOLKIT) \
$(SOURCEVIEWCOMPAT) \
......@@ -1421,9 +1423,9 @@ $(foreach file,$(LONELY_TESTS_ML_FILES),\
$(foreach file,$(LONELY_TESTS_ML_FILES),\
$(eval $(file:%.ml=%.cmxs): OFLAGS+=-I $(dir $(file))))
.PRECIOUS: $(LONELY_TESTS_ML_FILES:%.ml=%.cmx) \
$(LONELY_TESTS_DYN_FILES:%.ml=%.cmxs) \
$(LONELY_TESTS_BYTE_FILES:%.ml=%.cmo) \
$(LONELY_TESTS_BYTE_FILES:%.ml=%.cmi)
$(LONELY_TESTS_ML_FILES:%.ml=%.cmxs) \
$(LONELY_TESTS_ML_FILES:%.ml=%.cmo) \
$(LONELY_TESTS_ML_FILES:%.ml=%.cmi)
bin/ocamldep_transitive_closure: devel_tools/ocamldep_transitive_closure.ml
$(OCAMLOPT) -package ocamlgraph -package str -linkpkg -o $@ $<
......@@ -1874,7 +1876,6 @@ install:: install-lib
$(MKDIR) $(FRAMAC_DATADIR)/theme/flat
$(MKDIR) $(FRAMAC_DATADIR)/libc/sys
$(MKDIR) $(FRAMAC_DATADIR)/libc/netinet
$(MKDIR) $(FRAMAC_DATADIR)/libc/linux
$(MKDIR) $(FRAMAC_DATADIR)/libc/net
$(MKDIR) $(FRAMAC_DATADIR)/libc/arpa
$(PRINT_INSTALL) shared files
......@@ -1917,7 +1918,6 @@ install:: install-lib
$(CP) share/libc/arpa/*.[ch] $(FRAMAC_DATADIR)/libc/arpa
$(CP) share/libc/net/*.[ch] $(FRAMAC_DATADIR)/libc/net
$(CP) share/libc/netinet/*.[ch] $(FRAMAC_DATADIR)/libc/netinet
$(CP) share/libc/linux/*.[ch] $(FRAMAC_DATADIR)/libc/linux
$(PRINT_INSTALL) binaries
$(CP) bin/toplevel.$(OCAMLBEST) $(BINDIR)/frama-c$(EXE)
$(CP) bin/toplevel.byte$(EXE) $(BINDIR)/frama-c.byte$(EXE)
......
headers/header_spec.txt
+ 5
− 13
View file @ 64205cb6
......@@ -224,13 +224,7 @@ share/libc/inttypes.c: CEA_LGPL
share/libc/inttypes.h: CEA_LGPL
share/libc/iso646.h: CEA_LGPL
share/libc/libgen.h: CEA_LGPL
share/libc/libintl.h: CEA_LGPL
share/libc/limits.h: CEA_LGPL
share/libc/linux/fs.h: CEA_LGPL
share/libc/linux/if_addr.h: CEA_LGPL
share/libc/linux/if_netlink.h: CEA_LGPL
share/libc/linux/netlink.h: CEA_LGPL
share/libc/linux/rtnetlink.h: CEA_LGPL
share/libc/locale.c: CEA_LGPL
share/libc/locale.h: CEA_LGPL
share/libc/malloc.h: CEA_LGPL
......@@ -243,9 +237,6 @@ share/libc/net/if.h: CEA_LGPL
share/libc/netdb.c: CEA_LGPL
share/libc/netdb.h: CEA_LGPL
share/libc/netinet/in.h: CEA_LGPL
share/libc/netinet/in_systm.h: CEA_LGPL
share/libc/netinet/ip.h: CEA_LGPL
share/libc/netinet/ip_icmp.h: CEA_LGPL
share/libc/netinet/tcp.h: CEA_LGPL
share/libc/nl_types.h: CEA_LGPL
share/libc/poll.h: CEA_LGPL
......@@ -273,7 +264,6 @@ share/libc/sys/file.h: CEA_LGPL
share/libc/sys/ioctl.h: CEA_LGPL
share/libc/sys/ipc.h: CEA_LGPL
share/libc/sys/mman.h: CEA_LGPL
share/libc/sys/param.h: CEA_LGPL
share/libc/sys/random.h: CEA_LGPL
share/libc/sys/resource.h: CEA_LGPL
share/libc/sys/select.h: CEA_LGPL
......@@ -281,7 +271,6 @@ share/libc/sys/shm.h: CEA_LGPL
share/libc/sys/signal.h: CEA_LGPL
share/libc/sys/socket.h: CEA_LGPL
share/libc/sys/stat.h: CEA_LGPL
share/libc/sys/sysctl.h: CEA_LGPL
share/libc/sys/time.h: CEA_LGPL
share/libc/sys/times.h: CEA_LGPL
share/libc/sys/timex.h: CEA_LGPL
......@@ -293,9 +282,8 @@ share/libc/sys/wait.h: CEA_LGPL
share/libc/syslog.h: CEA_LGPL
share/libc/termios.h: CEA_LGPL
share/libc/tgmath.h: CEA_LGPL
share/libc/time.h: CEA_LGPL
share/libc/time.c: CEA_LGPL
share/libc/uchar.h: CEA_LGPL
share/libc/time.h: CEA_LGPL
share/libc/unistd.h: CEA_LGPL
share/libc/utime.h: CEA_LGPL
share/libc/utmpx.h: CEA_LGPL
......@@ -514,6 +502,8 @@ src/kernel_services/ast_printing/printer.mli: CEA_LGPL
src/kernel_services/ast_printing/printer_api.mli: CEA_LGPL
src/kernel_services/ast_printing/printer_builder.ml: CEA_LGPL
src/kernel_services/ast_printing/printer_builder.mli: CEA_LGPL
src/kernel_services/ast_printing/printer_tag.ml: CEA_LGPL
src/kernel_services/ast_printing/printer_tag.mli: CEA_LGPL
src/kernel_services/ast_queries/README.md: .ignore
src/kernel_services/ast_queries/ast_info.ml: CEA_LGPL
src/kernel_services/ast_queries/ast_info.mli: CEA_LGPL
......@@ -824,6 +814,8 @@ src/plugins/gui/wtext.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/wtext.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/wutil.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/wutil.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/wutil_once.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/wutil_once.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/impact/Impact.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/impact/compute_impact.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/impact/compute_impact.mli: CEA_LGPL_OR_PROPRIETARY
......
share/libc/__fc_define_fd_set_t.h
+ 3
− 2
View file @ 64205cb6
......@@ -24,8 +24,10 @@
#define __FC_DEFINE_FD_SET_T
#include "features.h"
__PUSH_FC_STDLIB
#define FD_SETSIZE 1024
#define NFDBITS (8 * sizeof(long))
__BEGIN_DECLS
typedef struct {char __fc_fd_set;} fd_set;
typedef struct { long __fc_fd_set[FD_SETSIZE / NFDBITS]; } fd_set;
/*@
requires valid_fdset: \valid(fdset);
......@@ -62,6 +64,5 @@ extern void FD_ZERO(fd_set *fdset);
#define FD_ZERO FD_ZERO
__END_DECLS
#define FD_SETSIZE 1024
__POP_FC_STDLIB
#endif
share/libc/libgen.h
+ 25
− 2
View file @ 64205cb6
......@@ -20,13 +20,36 @@
/* */
/**************************************************************************/
#ifndef __FC_LIBGEN
#define __FC_LIBGEN
#ifndef __FC_LIBGEN_H
#define __FC_LIBGEN_H
#include "features.h"
#include "__fc_machdep.h"
#include "__fc_string_axiomatic.h"
__PUSH_FC_STDLIB
__BEGIN_DECLS
extern char __fc_basename[__FC_PATH_MAX];
char *__fc_p_basename = __fc_basename;
/*@ // missing: assigns path[0 ..], __fc_p_basename[0 ..] \from 'filesystem';
requires null_or_valid_string_path: path == \null || valid_read_string(path);
assigns path[0 ..], __fc_basename[0 ..] \from path[0 ..], __fc_basename[0 ..];
assigns \result \from __fc_p_basename, path;
ensures result_points_to_internal_storage_or_path:
\subset(\result, {__fc_p_basename, path});
*/
extern char *basename(char *path);
extern char __fc_dirname[__FC_PATH_MAX];
char *__fc_p_dirname = __fc_dirname;
/*@ // missing: assigns path[0 ..], __fc_p_dirname[0 ..] \from 'filesystem';
requires null_or_valid_string_path: path == \null || valid_read_string(path);
assigns path[0 ..], __fc_dirname[0 ..] \from path[0 ..], __fc_dirname[0 ..];
assigns \result \from __fc_p_dirname, path;
ensures result_points_to_internal_storage_or_path:
\subset(\result, {__fc_p_dirname, path});
*/
extern char *dirname(char *path);
__END_DECLS
......
share/libc/libintl.h deleted 100644 → 0
+ 0
− 26
View file @ 861f1bf8
/**************************************************************************/
/* */
/* This file is part of Frama-C. */
/* */
/* Copyright (C) 2007-2019 */
/* 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_LIBINTL_H
#define __FC_LIBINTL_H
#endif
share/libc/linux/fs.h deleted 100644 → 0
+ 0
− 28
View file @ 861f1bf8
/**************************************************************************/
/* */
/* This file is part of Frama-C. */
/* */
/* Copyright (C) 2007-2019 */
/* 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_LINUX_FS_H
#define __FC_LINUX_FS_H
/* TODO */
#endif
share/libc/linux/if_addr.h deleted 100644 → 0
+ 0
− 26
View file @ 861f1bf8
/**************************************************************************/
/* */
/* This file is part of Frama-C. */
/* */
/* Copyright (C) 2007-2019 */
/* 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_LINUX_IF_ADDR_H
#define __FC_LINUX_IF_ADDR_H
#endif
share/libc/linux/if_netlink.h deleted 100644 → 0
+ 0
− 27
View file @ 861f1bf8
/**************************************************************************/
/* */
/* This file is part of Frama-C. */
/* */
/* Copyright (C) 2007-2019 */
/* 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_IF_NETLINK_H
#define __FC_IF_NETLINK_H
#endif
share/libc/linux/netlink.h deleted 100644 → 0
+ 0
− 28
View file @ 861f1bf8
/**************************************************************************/
/* */
/* This file is part of Frama-C. */
/* */
/* Copyright (C) 2007-2019 */
/* 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_LINUX_NETLINK_H
#define __FC_LINUX_NETLINK_H
#endif
share/libc/linux/rtnetlink.h deleted 100644 → 0
+ 0
− 28
View file @ 861f1bf8
/**************************************************************************/
/* */
/* This file is part of Frama-C. */
/* */
/* Copyright (C) 2007-2019 */
/* 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_LINUX_RTNETLINK_H
#define __FC_LINUX_RTNETLINK_H
#endif
share/libc/netdb.c
+ 81
− 0
View file @ 64205cb6
......@@ -25,6 +25,7 @@
#include "netinet/in.h"
#include "stdlib.h"
#include "stddef.h"
#include "string.h"
#include "errno.h"
#include "__fc_builtin.h"
__PUSH_FC_STDLIB
......@@ -76,4 +77,84 @@ int getaddrinfo(
}
}
#define __FC_MAX_HOST_ADDRS 2
#define __FC_MAX_HOST_ALIASES 2
#define __FC_HOSTBUF_SIZE 128
#define __FC_QUERYBUF_SIZE 128
struct __fc_gethostbyname {
struct hostent host;
unsigned char host_addr[sizeof(struct in_addr)];
char *h_addr_ptrs[__FC_MAX_HOST_ADDRS + 1];
char *host_aliases[__FC_MAX_HOST_ALIASES];
char hostbuf[__FC_HOSTBUF_SIZE];
};
struct __fc_gethostbyname __fc_ghbn;
int res_search(const char *dname, int class, int type,
char *answer, int anslen) {
for (int i = 0; i < anslen-1; i++) {
answer[i] = Frama_C_char_interval(CHAR_MIN, CHAR_MAX);
}
answer[anslen-1] = 0;
return Frama_C_interval(-1, anslen);
}
struct hostent *gethostbyname(const char *name) {
char buf[__FC_QUERYBUF_SIZE];
const char *cp;
int n;
__fc_ghbn.host.h_addrtype = AF_INET;
__fc_ghbn.host.h_length = sizeof(struct in_addr);
// Disallow names consisting only of digits/dots, unless they end in a dot
if (*name >= '0' && *name <= '9') {
for (cp = name;; ++cp) {
if (!*cp) {
struct in_addr addr;
if (*--cp == '.') break;
// All-numeric, no dot at the end. Fake up a hostent as if we'd actually done a lookup.
addr.s_addr = inet_addr(name);
if (addr.s_addr == INADDR_NONE) return NULL;
memcpy(__fc_ghbn.host_addr, &addr, __fc_ghbn.host.h_length);
strncpy(__fc_ghbn.hostbuf, name, __FC_HOSTBUF_SIZE - 1);
__fc_ghbn.hostbuf[__FC_HOSTBUF_SIZE - 1] = '\0';
__fc_ghbn.host.h_name = __fc_ghbn.hostbuf;
__fc_ghbn.host.h_aliases = __fc_ghbn.host_aliases;
__fc_ghbn.host_aliases[0] = NULL;
__fc_ghbn.h_addr_ptrs[0] = (char *) __fc_ghbn.host_addr;
__fc_ghbn.h_addr_ptrs[1] = NULL;
__fc_ghbn.host.h_addr_list = __fc_ghbn.h_addr_ptrs;
return &__fc_ghbn.host;
}
if (*cp < '0' && *cp > '9' && *cp != '.') break;
}
}
n = res_search(name, 1, 1, buf, sizeof(buf));
if (n < 0) return NULL;
if (Frama_C_nondet(0, 1)) return NULL;
else {
struct in_addr addr;
addr.s_addr = inet_addr(name);
memcpy(__fc_ghbn.host_addr, &addr, __fc_ghbn.host.h_length);
strncpy(__fc_ghbn.hostbuf, name, __FC_HOSTBUF_SIZE - 1);
__fc_ghbn.hostbuf[__FC_HOSTBUF_SIZE - 1] = '\0';
__fc_ghbn.host.h_name = __fc_ghbn.hostbuf;
__fc_ghbn.host.h_aliases = __fc_ghbn.host_aliases;
__fc_ghbn.host_aliases[0] = NULL;
__fc_ghbn.h_addr_ptrs[0] = (char *) __fc_ghbn.host_addr;
__fc_ghbn.h_addr_ptrs[1] = NULL;
__fc_ghbn.host.h_addr_list = __fc_ghbn.h_addr_ptrs;
return &__fc_ghbn.host;
}
}
__POP_FC_STDLIB
share/libc/netinet/in_systm.h deleted 100644 → 0
+ 0
− 26
View file @ 861f1bf8
/**************************************************************************/
/* */
/* This file is part of Frama-C. */
/* */
/* Copyright (C) 2007-2019 */
/* 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_NETINET_SYSTM_H
#define __FC_NETINET_SYSTM_H
#endif
share/libc/netinet/ip.h deleted 100644 → 0
+ 0
− 26
View file @ 861f1bf8
/**************************************************************************/
/* */
/* This file is part of Frama-C. */
/* */
/* Copyright (C) 2007-2019 */
/* 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_NETINET_IP_H
#define __FC_NETINET_IP_H
#endif
share/libc/netinet/ip_icmp.h deleted 100644 → 0
+ 0
− 27
View file @ 861f1bf8
/**************************************************************************/
/* */
/* This file is part of Frama-C. */
/* */
/* Copyright (C) 2007-2019 */
/* 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_NETINET_IP_ICMP_H
#define __FC_NETINET_IP_ICMP_H
#endif
share/libc/stdlib.c
+ 15
− 0
View file @ 64205cb6
......@@ -187,4 +187,19 @@ int unsetenv(const char *name)
char __fc_strerror[64];
#endif
// Note: this implementation does not check the alignment, since it cannot
// currently be specified in the memory model of most plug-ins
int posix_memalign(void **memptr, size_t alignment, size_t size) {
// By default, specifications in the libc are ignored for defined functions,
// and since we do not actually use alignment, we need to check its validity.
// The assertion below is the requires in the specification.
/*@ assert alignment_is_a_suitable_power_of_two:
alignment >= sizeof(void*) &&
((size_t)alignment & ((size_t)alignment - 1)) == 0;
*/
*memptr = malloc(size);
if (!*memptr) return ENOMEM;
return 0;
}
__POP_FC_STDLIB
share/libc/stdlib.h
+ 28
− 0
View file @ 64205cb6
......@@ -594,6 +594,34 @@ extern size_t wcstombs(char * restrict s,
size_t n);
// Note: this specification should ideally use a more specific predicate,
// such as 'is_allocable_aligned(alignment, size)'.
/*@
requires valid_memptr: \valid(memptr);
requires alignment_is_a_suitable_power_of_two:
alignment >= sizeof(void*) &&
((size_t)alignment & ((size_t)alignment - 1)) == 0;
allocates *memptr;
assigns __fc_heap_status \from indirect:alignment, size, __fc_heap_status;
assigns \result \from indirect:alignment, indirect:size,
indirect:__fc_heap_status;
behavior allocation:
assumes can_allocate: is_allocable(size);
assigns __fc_heap_status \from indirect:alignment, size, __fc_heap_status;
assigns \result \from indirect:alignment, indirect:size,
indirect:__fc_heap_status;
ensures allocation: \fresh(*memptr,size);
ensures result_zero: \result == 0;
behavior no_allocation:
assumes cannot_allocate: !is_allocable(size);
assigns \result \from indirect:alignment;
allocates \nothing;
ensures result_non_zero: \result < 0 || \result > 0;
complete behaviors;
disjoint behaviors;
*/
extern int posix_memalign(void **memptr, size_t alignment, size_t size);
__END_DECLS
__POP_FC_STDLIB
......
share/libc/strings.h
+ 1
− 0
View file @ 64205cb6
......@@ -35,6 +35,7 @@ extern void bcopy(const void *, void *, size_t);
/*@ requires valid_memory_area: \valid (((char*) s)+(0 .. n-1));
assigns ((char*) s)[0 .. n-1] \from \nothing;
ensures s_initialized:initialization:\initialized(((char*) s)+(0 .. n-1));
ensures zero_initialized: \subset(((char*) s)[0 .. n-1], {0}); */
extern void bzero(void *s, size_t n);
extern int ffs(int);
......
share/libc/sys/param.h deleted 100644 → 0
+ 0
− 28
View file @ 861f1bf8
/**************************************************************************/
/* */
/* This file is part of Frama-C. */
/* */
/* Copyright (C) 2007-2019 */
/* 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_SYS_PARAM_H__
#define __FC_SYS_PARAM_H__
/* Only deprecated programs use this header. Add whatever is needed
for this program to compile. */
#endif
share/libc/sys/sysctl.h deleted 100644 → 0
+ 0
− 22
View file @ 861f1bf8
/**************************************************************************/
/* */
/* This file is part of Frama-C. */
/* */
/* Copyright (C) 2007-2019 */
/* 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). */
/* */
/**************************************************************************/
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment