From e47585b560e0ec54252365e8761e37f0ae5853d8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 6 Apr 2018 14:34:47 +0000 Subject: [PATCH 1/2] Re-use known declarations when parsing the built-in library When doing cross-platform verification we should not rely on 1) system headers being present and 2) system headers matching the declarations that were used while compiling the program to be verified. Thus re-use the symbol table that has been generated from the input program when compiling functions of the built-in library. This will address a number of SV-COMP benchmarks that CBMC currently fails on for they use augmented standard-library types. --- regression/cbmc/library1/main.c | 16 ++++++++++++ regression/cbmc/library1/test.desc | 10 ++++++++ src/ansi-c/ansi_c_language.cpp | 41 ++++++++++++++++++++++++++---- src/ansi-c/ansi_c_language.h | 5 ++++ src/ansi-c/ansi_c_parser.cpp | 24 ++++++++++++++++- src/ansi-c/ansi_c_parser.h | 13 +++++++++- src/ansi-c/ansi_c_scope.h | 4 ++- src/ansi-c/cprover_library.cpp | 7 +++-- src/ansi-c/cprover_library.h | 5 ---- 9 files changed, 110 insertions(+), 15 deletions(-) create mode 100644 regression/cbmc/library1/main.c create mode 100644 regression/cbmc/library1/test.desc diff --git a/regression/cbmc/library1/main.c b/regression/cbmc/library1/main.c new file mode 100644 index 00000000000..a719833c455 --- /dev/null +++ b/regression/cbmc/library1/main.c @@ -0,0 +1,16 @@ +struct _IO_FILE; +typedef struct _IO_FILE FILE; +struct _IO_FILE +{ + char dummy; +}; + +extern FILE *fopen(char const *fname, char const *mode); + +int main() +{ + FILE *f; + f = fopen("some_file", "r"); + __CPROVER_assert(f == 0, ""); + return 0; +} diff --git a/regression/cbmc/library1/test.desc b/regression/cbmc/library1/test.desc new file mode 100644 index 00000000000..e41d42cf59f --- /dev/null +++ b/regression/cbmc/library1/test.desc @@ -0,0 +1,10 @@ +CORE +main.c + +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring +implicit function declaration +syntax error diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp index bbb1236e9e7..f3e61b8e161 100644 --- a/src/ansi-c/ansi_c_language.cpp +++ b/src/ansi-c/ansi_c_language.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -52,6 +53,15 @@ bool ansi_c_languaget::preprocess( bool ansi_c_languaget::parse( std::istream &instream, const std::string &path) +{ + symbol_tablet st; + return parse(instream, path, st); +} + +bool ansi_c_languaget::parse( + std::istream &instream, + const std::string &path, + const symbol_tablet &symbol_table) { // store the path parse_path=path; @@ -78,6 +88,7 @@ bool ansi_c_languaget::parse( ansi_c_parser.cpp98=false; // it's not C++ ansi_c_parser.cpp11=false; // it's not C++ ansi_c_parser.mode=config.ansi_c.mode; + ansi_c_parser.set_symbol_table(symbol_table); ansi_c_scanner_init(); @@ -95,6 +106,27 @@ bool ansi_c_languaget::parse( // save result parse_tree.swap(ansi_c_parser.parse_tree); + // copy depended-on symbols from the existing symbol table + std::list needed_syms; + for(const auto &scope_syms : ansi_c_parser.root_scope().name_map) + { + if(scope_syms.second.from_symbol_table) + needed_syms.push_back(scope_syms.second.prefixed_name); + } + while(!needed_syms.empty()) + { + const irep_idt id = needed_syms.front(); + needed_syms.pop_front(); + const symbolt &symbol = symbol_table.lookup_ref(id); + + if(symbol.is_type && !new_symbol_table.add(symbol)) + { + find_symbols_sett deps; + find_type_symbols(symbol.type, deps); + needed_syms.insert(needed_syms.end(), deps.begin(), deps.end()); + } + } + // save some memory ansi_c_parser.clear(); @@ -105,8 +137,6 @@ bool ansi_c_languaget::typecheck( symbol_tablet &symbol_table, const std::string &module) { - symbol_tablet new_symbol_table; - if(ansi_c_typecheck( parse_tree, new_symbol_table, @@ -118,10 +148,10 @@ bool ansi_c_languaget::typecheck( remove_internal_symbols(new_symbol_table); - if(linking(symbol_table, new_symbol_table, get_message_handler())) - return true; + bool retval = linking(symbol_table, new_symbol_table, get_message_handler()); + new_symbol_table.clear(); - return false; + return retval; } bool ansi_c_languaget::generate_support_functions( @@ -196,6 +226,7 @@ bool ansi_c_languaget::to_expr( ansi_c_parser.in=&i_preprocessed; ansi_c_parser.set_message_handler(get_message_handler()); ansi_c_parser.mode=config.ansi_c.mode; + ansi_c_parser.set_symbol_table(ns.get_symbol_table()); ansi_c_scanner_init(); bool result=ansi_c_parser.parse(); diff --git a/src/ansi-c/ansi_c_language.h b/src/ansi-c/ansi_c_language.h index b23bdad6469..d9a420a95cb 100644 --- a/src/ansi-c/ansi_c_language.h +++ b/src/ansi-c/ansi_c_language.h @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include @@ -30,6 +31,9 @@ class ansi_c_languaget:public languaget std::istream &instream, const std::string &path) override; + bool + parse(std::istream &instream, const std::string &path, const symbol_tablet &); + bool generate_support_functions( symbol_tablet &symbol_table) override; @@ -75,6 +79,7 @@ class ansi_c_languaget:public languaget protected: ansi_c_parse_treet parse_tree; std::string parse_path; + symbol_tablet new_symbol_table; }; std::unique_ptr new_ansi_c_language(); diff --git a/src/ansi-c/ansi_c_parser.cpp b/src/ansi-c/ansi_c_parser.cpp index 46d9f51d1b4..80b0f96c6f8 100644 --- a/src/ansi-c/ansi_c_parser.cpp +++ b/src/ansi-c/ansi_c_parser.cpp @@ -8,7 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "ansi_c_parser.h" -#include +#include #include "c_storage_spec.h" @@ -42,6 +42,24 @@ ansi_c_id_classt ansi_c_parsert::lookup( } } + // if a symbol table has been provided, try to resolve global-scoped symbols + if(!tag && !label && symbol_table) + { + const symbolt *symbol = symbol_table->lookup(scope_name); + if(symbol) + { + ansi_c_identifiert &i = root_scope().name_map[scope_name]; + i.from_symbol_table = true; + i.id_class = symbol->is_type && symbol->is_macro + ? ansi_c_id_classt::ANSI_C_TYPEDEF + : ansi_c_id_classt::ANSI_C_SYMBOL; + i.prefixed_name = symbol->name; + i.base_name = symbol->base_name; + identifier = i.prefixed_name; + return i.id_class; + } + } + // Not found. // If it's a tag, we will add to current scope. if(tag) @@ -150,6 +168,10 @@ void ansi_c_parsert::add_declarator( ansi_c_identifiert &identifier=scope.name_map[base_name]; identifier.id_class=id_class; identifier.prefixed_name=prefixed_name; + // it may already have been put in the scope from an existing symbol table + // via lookup; now that we know it's being declared here we don't need or + // want the entry from the symbol table + identifier.from_symbol_table = false; } ansi_c_declaration.declarators().push_back(new_declarator); diff --git a/src/ansi-c/ansi_c_parser.h b/src/ansi-c/ansi_c_parser.h index b5dad0a515f..78931277d3a 100644 --- a/src/ansi-c/ansi_c_parser.h +++ b/src/ansi-c/ansi_c_parser.h @@ -35,7 +35,8 @@ class ansi_c_parsert:public parsert mode(modet::NONE), cpp98(false), cpp11(false), - for_has_scope(false) + for_has_scope(false), + symbol_table(nullptr) { } @@ -59,6 +60,8 @@ class ansi_c_parsert:public parsert // set up global scope scopes.clear(); scopes.push_back(scopet()); + + symbol_table = nullptr; } // internal state of the scanner @@ -139,6 +142,14 @@ class ansi_c_parsert:public parsert lookup(base_name, identifier, false, true); return identifier; } + + void set_symbol_table(const symbol_tablet &st) + { + symbol_table = &st; + } + +private: + const symbol_tablet *symbol_table; }; extern ansi_c_parsert ansi_c_parser; diff --git a/src/ansi-c/ansi_c_scope.h b/src/ansi-c/ansi_c_scope.h index 4095c58ec63..a5ef0afe13e 100644 --- a/src/ansi-c/ansi_c_scope.h +++ b/src/ansi-c/ansi_c_scope.h @@ -29,9 +29,11 @@ class ansi_c_identifiert { public: ansi_c_id_classt id_class; + bool from_symbol_table; irep_idt base_name, prefixed_name; - ansi_c_identifiert():id_class(ansi_c_id_classt::ANSI_C_UNKNOWN) + ansi_c_identifiert() + : id_class(ansi_c_id_classt::ANSI_C_UNKNOWN), from_symbol_table(false) { } }; diff --git a/src/ansi-c/cprover_library.cpp b/src/ansi-c/cprover_library.cpp index f13e321d752..efecfcb123e 100644 --- a/src/ansi-c/cprover_library.cpp +++ b/src/ansi-c/cprover_library.cpp @@ -14,6 +14,9 @@ Author: Daniel Kroening, kroening@kroening.com #include "ansi_c_language.h" +static void +add_library(const std::string &src, symbol_tablet &, message_handlert &); + struct cprover_library_entryt { const char *function; @@ -78,7 +81,7 @@ void add_cprover_library( add_library(library_text, symbol_table, message_handler); } -void add_library( +static void add_library( const std::string &src, symbol_tablet &symbol_table, message_handlert &message_handler) @@ -90,7 +93,7 @@ void add_library( ansi_c_languaget ansi_c_language; ansi_c_language.set_message_handler(message_handler); - ansi_c_language.parse(in, ""); + ansi_c_language.parse(in, "", symbol_table); ansi_c_language.typecheck(symbol_table, ""); } diff --git a/src/ansi-c/cprover_library.h b/src/ansi-c/cprover_library.h index 6f36eb5abca..babcfea7778 100644 --- a/src/ansi-c/cprover_library.h +++ b/src/ansi-c/cprover_library.h @@ -19,11 +19,6 @@ std::string get_cprover_library_text( const std::set &functions, const symbol_tablet &); -void add_library( - const std::string &src, - symbol_tablet &, - message_handlert &); - void add_cprover_library( const std::set &functions, symbol_tablet &, From ad308bb0fe077d4c364924e95582ace50943be5b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 6 Apr 2018 14:45:45 +0000 Subject: [PATCH 2/2] Built-in C library: only include headers that provide macro- or enum values --- src/ansi-c/library/cprover.h | 1 + src/ansi-c/library/err.c | 30 +-- src/ansi-c/library/fcntl.c | 5 - src/ansi-c/library/getopt.c | 20 +- src/ansi-c/library/inet.c | 69 ++--- src/ansi-c/library/locale.c | 13 +- src/ansi-c/library/math.c | 423 ++++--------------------------- src/ansi-c/library/netdb.c | 6 +- src/ansi-c/library/pthread_lib.c | 142 +---------- src/ansi-c/library/semaphore.c | 20 +- src/ansi-c/library/setjmp.c | 23 +- src/ansi-c/library/signal.c | 10 +- src/ansi-c/library/stdio.c | 279 +++----------------- src/ansi-c/library/string.c | 180 ++----------- src/ansi-c/library/syslog.c | 15 -- src/ansi-c/library/threads.c | 89 +------ src/ansi-c/library/time.c | 59 +---- src/ansi-c/library/unistd.c | 32 +-- src/ansi-c/library/windows.c | 9 +- 19 files changed, 176 insertions(+), 1249 deletions(-) diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h index 7fce070860a..a16feef74c7 100644 --- a/src/ansi-c/library/cprover.h +++ b/src/ansi-c/library/cprover.h @@ -38,6 +38,7 @@ void __CPROVER_cover(__CPROVER_bool condition); void __CPROVER_input(const char *id, ...); void __CPROVER_output(const char *id, ...); +int __CPROVER_printf(const char *fmt, ...); // concurrency-related void __CPROVER_atomic_begin(); diff --git a/src/ansi-c/library/err.c b/src/ansi-c/library/err.c index bbf9f133427..d21f1260fa8 100644 --- a/src/ansi-c/library/err.c +++ b/src/ansi-c/library/err.c @@ -1,14 +1,6 @@ /* FUNCTION: err */ -#ifndef __CPROVER_ERR_H_INCLUDED -#include -#define __CPROVER_ERR_H_INCLUDED -#endif - -#ifndef __CPROVER_STDLIB_H_INCLUDED -#include -#define __CPROVER_STDLIB_H_INCLUDED -#endif +void abort(void); void err(int eval, const char *fmt, ...) { @@ -19,15 +11,7 @@ void err(int eval, const char *fmt, ...) /* FUNCTION: err */ -#ifndef __CPROVER_ERR_H_INCLUDED -#include -#define __CPROVER_ERR_H_INCLUDED -#endif - -#ifndef __CPROVER_STDLIB_H_INCLUDED -#include -#define __CPROVER_STDLIB_H_INCLUDED -#endif +void abort(void); void errx(int eval, const char *fmt, ...) { @@ -38,11 +22,6 @@ void errx(int eval, const char *fmt, ...) /* FUNCTION: warn */ -#ifndef __CPROVER_ERR_H_INCLUDED -#include -#define __CPROVER_ERR_H_INCLUDED -#endif - void warn(const char *fmt, ...) { (void)*fmt; @@ -50,11 +29,6 @@ void warn(const char *fmt, ...) /* FUNCTION: warnx */ -#ifndef __CPROVER_ERR_H_INCLUDED -#include -#define __CPROVER_ERR_H_INCLUDED -#endif - void warnx(const char *fmt, ...) { (void)*fmt; diff --git a/src/ansi-c/library/fcntl.c b/src/ansi-c/library/fcntl.c index 7001724c9bf..9153a37ed8e 100644 --- a/src/ansi-c/library/fcntl.c +++ b/src/ansi-c/library/fcntl.c @@ -1,10 +1,5 @@ /* FUNCTION: fcntl */ -#ifndef __CPROVER_FCNTL_H_INCLUDED -#include -#define __CPROVER_FCNTL_H_INCLUDED -#endif - int __VERIFIER_nondet_int(); int fcntl(int fd, int cmd, ...) diff --git a/src/ansi-c/library/getopt.c b/src/ansi-c/library/getopt.c index 0045cbd105d..7f261ad5b7f 100644 --- a/src/ansi-c/library/getopt.c +++ b/src/ansi-c/library/getopt.c @@ -1,15 +1,16 @@ +#ifdef LIBRARY_CHECK +#include +#endif + /* FUNCTION: getopt */ extern char *optarg; extern int optind; -#ifndef __CPROVER_STRING_H_INCLUDED -#include -#define __CPROVER_STRING_H_INCLUDED -#endif +__CPROVER_size_t strlen(const char *s); __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); -size_t __VERIFIER_nondet_size_t(); +__CPROVER_size_t __VERIFIER_nondet_size_t(); inline int getopt( int argc, char * const argv[], const char *optstring) @@ -23,7 +24,7 @@ inline int getopt( if(optind>=argc || argv[optind][0]!='-') return -1; - size_t result_index=__VERIFIER_nondet_size_t(); + __CPROVER_size_t result_index = __VERIFIER_nondet_size_t(); __CPROVER_assume( result_index -#define __CPROVER_GETOPT_H_INCLUDED -#endif +int getopt(int argc, char *const argv[], const char *optstring); inline int getopt_long( int argc, diff --git a/src/ansi-c/library/inet.c b/src/ansi-c/library/inet.c index 54623bffb5a..f8db5ab47c1 100644 --- a/src/ansi-c/library/inet.c +++ b/src/ansi-c/library/inet.c @@ -1,12 +1,17 @@ -/* FUNCTION: inet_addr */ - #ifndef _WIN32 - -#ifndef __CPROVER_INET_H_INCLUDED +#ifdef LIBRARY_CHECK #include -#define __CPROVER_INET_H_INCLUDED +#undef htonl +#undef htons +#undef ntohl +#undef ntohs +#endif #endif +/* FUNCTION: inet_addr */ + +#ifndef _WIN32 + in_addr_t __VERIFIER_nondet_in_addr_t(); in_addr_t inet_addr(const char *cp) @@ -28,11 +33,6 @@ in_addr_t inet_addr(const char *cp) #ifndef _WIN32 -#ifndef __CPROVER_INET_H_INCLUDED -#include -#define __CPROVER_INET_H_INCLUDED -#endif - int __VERIFIER_nondet_int(); int inet_aton(const char *cp, struct in_addr *pin) @@ -55,11 +55,6 @@ int inet_aton(const char *cp, struct in_addr *pin) #ifndef _WIN32 -#ifndef __CPROVER_INET_H_INCLUDED -#include -#define __CPROVER_INET_H_INCLUDED -#endif - in_addr_t __VERIFIER_nondet_in_addr_t(); in_addr_t inet_network(const char *cp) @@ -79,16 +74,9 @@ in_addr_t inet_network(const char *cp) /* FUNCTION: htonl */ -#ifndef __CPROVER_STDINT_H_INCLUDED -#include -#define __CPROVER_STDINT_H_INCLUDED -#endif - -#undef htonl - -uint32_t __builtin_bswap32(uint32_t); +unsigned int __builtin_bswap32(unsigned int); -uint32_t htonl(uint32_t hostlong) +unsigned int htonl(unsigned int hostlong) { #if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__ return __builtin_bswap32(hostlong); @@ -99,16 +87,9 @@ uint32_t htonl(uint32_t hostlong) /* FUNCTION: htons */ -#ifndef __CPROVER_STDINT_H_INCLUDED -#include -#define __CPROVER_STDINT_H_INCLUDED -#endif - -#undef htons - -uint16_t __builtin_bswap16(uint16_t); +unsigned short __builtin_bswap16(unsigned short); -uint16_t htons(uint16_t hostshort) +unsigned short htons(unsigned short hostshort) { #if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__ return __builtin_bswap16(hostshort); @@ -120,16 +101,9 @@ uint16_t htons(uint16_t hostshort) /* FUNCTION: ntohl */ -#ifndef __CPROVER_STDINT_H_INCLUDED -#include -#define __CPROVER_STDINT_H_INCLUDED -#endif - -#undef ntohl - -uint32_t __builtin_bswap32(uint32_t); +unsigned int __builtin_bswap32(unsigned int); -uint32_t ntohl(uint32_t netlong) +unsigned int ntohl(unsigned int netlong) { #if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__ return __builtin_bswap32(netlong); @@ -141,16 +115,9 @@ uint32_t ntohl(uint32_t netlong) /* FUNCTION: ntohs */ -#ifndef __CPROVER_STDINT_H_INCLUDED -#include -#define __CPROVER_STDINT_H_INCLUDED -#endif - -#undef ntohs - -uint16_t __builtin_bswap16(uint16_t); +unsigned short __builtin_bswap16(unsigned short); -uint16_t ntohs(uint16_t netshort) +unsigned short ntohs(unsigned short netshort) { #if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__ return __builtin_bswap16(netshort); diff --git a/src/ansi-c/library/locale.c b/src/ansi-c/library/locale.c index 61d5353457e..8a60844bb02 100644 --- a/src/ansi-c/library/locale.c +++ b/src/ansi-c/library/locale.c @@ -1,11 +1,9 @@ - -/* FUNCTION: setlocale */ - -#ifndef __CPROVER_LOCALE_H_INCLUDED +#ifdef LIBRARY_CHECK #include -#define __CPROVER_LOCALE_H_INCLUDED #endif +/* FUNCTION: setlocale */ + inline char *setlocale(int category, const char *locale) { __CPROVER_HIDE:; @@ -24,11 +22,6 @@ inline char *setlocale(int category, const char *locale) /* FUNCTION: localeconv */ -#ifndef __CPROVER_LOCALE_H_INCLUDED -#include -#define __CPROVER_LOCALE_H_INCLUDED -#endif - inline struct lconv *localeconv(void) { __CPROVER_HIDE:; diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c index c9f52dc8f76..573758089c3 100644 --- a/src/ansi-c/library/math.c +++ b/src/ansi-c/library/math.c @@ -714,11 +714,6 @@ __CPROVER_hide:; * square root (i.e. the real value of the square root rounded). */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - #ifndef __CPROVER_FENV_H_INCLUDED #include #define __CPROVER_FENV_H_INCLUDED @@ -801,11 +796,6 @@ float sqrtf(float f) /* The same caveats as sqrtf apply */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - #ifndef __CPROVER_FENV_H_INCLUDED #include #define __CPROVER_FENV_H_INCLUDED @@ -872,11 +862,6 @@ double sqrt(double d) /* The same caveats as sqrtf apply */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - #ifndef __CPROVER_FENV_H_INCLUDED #include #define __CPROVER_FENV_H_INCLUDED @@ -962,34 +947,28 @@ long double sqrtl(long double d) /* FUNCTION: fmax */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - // TODO : Should call a __CPROVER_function so that it can be converted to SMT-LIB -double fmax(double f, double g) { return ((f >= g) || isnan(g)) ? f : g; } +double fmax(double f, double g) +{ + return ((f >= g) || __CPROVER_isnand(g)) ? f : g; +} /* FUNCTION : fmaxf */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - // TODO : Should call a __CPROVER_function so that it can be converted to SMT-LIB -float fmaxf(float f, float g) { return ((f >= g) || isnan(g)) ? f : g; } +float fmaxf(float f, float g) +{ + return ((f >= g) || __CPROVER_isnanf(g)) ? f : g; +} /* FUNCTION : fmaxl */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - // TODO : Should call a __CPROVER_function so that it can be converted to SMT-LIB -long double fmaxl(long double f, long double g) { return ((f >= g) || isnan(g)) ? f : g; } +long double fmaxl(long double f, long double g) +{ + return ((f >= g) || __CPROVER_isnanld(g)) ? f : g; +} /* ISO 9899:2011 @@ -1006,33 +985,27 @@ long double fmaxl(long double f, long double g) { return ((f >= g) || isnan(g)) /* FUNCTION: fmin */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - // TODO : Should call a __CPROVER_function so that it can be converted to SMT-LIB -double fmin(double f, double g) { return ((f <= g) || isnan(g)) ? f : g; } +double fmin(double f, double g) +{ + return ((f <= g) || __CPROVER_isnand(g)) ? f : g; +} /* FUNCTION: fminf */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - // TODO : Should call a __CPROVER_function so that it can be converted to SMT-LIB -float fminf(float f, float g) { return ((f <= g) || isnan(g)) ? f : g; } +float fminf(float f, float g) +{ + return ((f <= g) || __CPROVER_isnanf(g)) ? f : g; +} /* FUNCTION: fminl */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - // TODO : Should call a __CPROVER_function so that it can be converted to SMT-LIB -long double fminl(long double f, long double g) { return ((f <= g) || isnan(g)) ? f : g; } +long double fminl(long double f, long double g) +{ + return ((f <= g) || __CPROVER_isnanld(g)) ? f : g; +} /* ISO 9899:2011 @@ -1045,31 +1018,16 @@ long double fminl(long double f, long double g) { return ((f <= g) || isnan(g)) /* FUNCTION: fdim */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - double fdim(double f, double g) { return ((f > g) ? f - g : +0.0); } /* FUNCTION: fdimf */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - float fdimf(float f, float g) { return ((f > g) ? f - g : +0.0f); } /* FUNCTION: fdiml */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - long double fdiml(long double f, long double g) { return ((f > g) ? f - g : +0.0); } @@ -1077,15 +1035,8 @@ long double fdiml(long double f, long double g) { return ((f > g) ? f - g : +0.0 /* FUNCTION: __sort_of_CPROVER_round_to_integral */ // TODO : Should be a real __CPROVER function to convert to SMT-LIB -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - -#ifndef __CPROVER_FENV_H_INCLUDED -#include -#define __CPROVER_FENV_H_INCLUDED -#endif +int fegetround(); +int fesetround(int); double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d) { @@ -1116,15 +1067,8 @@ double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d) /* FUNCTION: __sort_of_CPROVER_round_to_integralf */ // TODO : Should be a real __CPROVER function to convert to SMT-LIB -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - -#ifndef __CPROVER_FENV_H_INCLUDED -#include -#define __CPROVER_FENV_H_INCLUDED -#endif +int fegetround(); +int fesetround(int); float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d) { @@ -1156,15 +1100,8 @@ float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d) /* FUNCTION: __sort_of_CPROVER_round_to_integrall */ // TODO : Should be a real __CPROVER function to convert to SMT-LIB -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - -#ifndef __CPROVER_FENV_H_INCLUDED -#include -#define __CPROVER_FENV_H_INCLUDED -#endif +int fegetround(); +int fesetround(int); long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d) { @@ -1200,11 +1137,6 @@ long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double /* FUNCTION: ceil */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - #ifndef __CPROVER_FENV_H_INCLUDED #include #define __CPROVER_FENV_H_INCLUDED @@ -1219,11 +1151,6 @@ double ceil(double x) /* FUNCTION: ceilf */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - #ifndef __CPROVER_FENV_H_INCLUDED #include #define __CPROVER_FENV_H_INCLUDED @@ -1239,11 +1166,6 @@ float ceilf(float x) /* FUNCTION: ceill */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - #ifndef __CPROVER_FENV_H_INCLUDED #include #define __CPROVER_FENV_H_INCLUDED @@ -1264,11 +1186,6 @@ long double ceill(long double x) /* FUNCTION: floor */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - #ifndef __CPROVER_FENV_H_INCLUDED #include #define __CPROVER_FENV_H_INCLUDED @@ -1283,11 +1200,6 @@ double floor(double x) /* FUNCTION: floorf */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - #ifndef __CPROVER_FENV_H_INCLUDED #include #define __CPROVER_FENV_H_INCLUDED @@ -1303,11 +1215,6 @@ float floorf(float x) /* FUNCTION: floorl */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - #ifndef __CPROVER_FENV_H_INCLUDED #include #define __CPROVER_FENV_H_INCLUDED @@ -1329,11 +1236,6 @@ long double floorl(long double x) /* FUNCTION: trunc */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - #ifndef __CPROVER_FENV_H_INCLUDED #include #define __CPROVER_FENV_H_INCLUDED @@ -1348,11 +1250,6 @@ double trunc(double x) /* FUNCTION: truncf */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - #ifndef __CPROVER_FENV_H_INCLUDED #include #define __CPROVER_FENV_H_INCLUDED @@ -1368,11 +1265,6 @@ float truncf(float x) /* FUNCTION: truncl */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - #ifndef __CPROVER_FENV_H_INCLUDED #include #define __CPROVER_FENV_H_INCLUDED @@ -1394,11 +1286,6 @@ long double truncl(long double x) /* FUNCTION: round */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - #ifndef __CPROVER_FENV_H_INCLUDED #include #define __CPROVER_FENV_H_INCLUDED @@ -1430,11 +1317,6 @@ double round(double x) /* FUNCTION: roundf */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - #ifndef __CPROVER_FENV_H_INCLUDED #include #define __CPROVER_FENV_H_INCLUDED @@ -1467,11 +1349,6 @@ float roundf(float x) /* FUNCTION: roundl */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - #ifndef __CPROVER_FENV_H_INCLUDED #include #define __CPROVER_FENV_H_INCLUDED @@ -1512,17 +1389,8 @@ long double roundl(long double x) /* FUNCTION: nearbyint */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - -#ifndef __CPROVER_FENV_H_INCLUDED -#include -#define __CPROVER_FENV_H_INCLUDED -#endif - double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d); +int fegetround(); double nearbyint(double x) { @@ -1531,17 +1399,8 @@ double nearbyint(double x) /* FUNCTION: nearbyintf */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - -#ifndef __CPROVER_FENV_H_INCLUDED -#include -#define __CPROVER_FENV_H_INCLUDED -#endif - float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d); +int fegetround(); float nearbyintf(float x) { @@ -1551,17 +1410,8 @@ float nearbyintf(float x) /* FUNCTION: nearbyintl */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - -#ifndef __CPROVER_FENV_H_INCLUDED -#include -#define __CPROVER_FENV_H_INCLUDED -#endif - long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d); +int fegetround(); long double nearbyintl(long double x) { @@ -1579,17 +1429,8 @@ long double nearbyintl(long double x) /* FUNCTION: rint */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - -#ifndef __CPROVER_FENV_H_INCLUDED -#include -#define __CPROVER_FENV_H_INCLUDED -#endif - double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d); +int fegetround(); double rint(double x) { @@ -1598,17 +1439,8 @@ double rint(double x) /* FUNCTION: rintf */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - -#ifndef __CPROVER_FENV_H_INCLUDED -#include -#define __CPROVER_FENV_H_INCLUDED -#endif - float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d); +int fegetround(); float rintf(float x) { @@ -1617,17 +1449,8 @@ float rintf(float x) /* FUNCTION: rintl */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - -#ifndef __CPROVER_FENV_H_INCLUDED -#include -#define __CPROVER_FENV_H_INCLUDED -#endif - long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d); +int fegetround(); long double rintl(long double x) { @@ -1647,17 +1470,8 @@ long double rintl(long double x) /* FUNCTION: lrint */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - -#ifndef __CPROVER_FENV_H_INCLUDED -#include -#define __CPROVER_FENV_H_INCLUDED -#endif - double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d); +int fegetround(); long int lrint(double x) { @@ -1669,17 +1483,8 @@ long int lrint(double x) /* FUNCTION: lrintf */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - -#ifndef __CPROVER_FENV_H_INCLUDED -#include -#define __CPROVER_FENV_H_INCLUDED -#endif - float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d); +int fegetround(); long int lrintf(float x) { @@ -1692,17 +1497,8 @@ long int lrintf(float x) /* FUNCTION: lrintl */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - -#ifndef __CPROVER_FENV_H_INCLUDED -#include -#define __CPROVER_FENV_H_INCLUDED -#endif - long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d); +int fegetround(); long int lrintl(long double x) { @@ -1715,17 +1511,8 @@ long int lrintl(long double x) /* FUNCTION: llrint */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - -#ifndef __CPROVER_FENV_H_INCLUDED -#include -#define __CPROVER_FENV_H_INCLUDED -#endif - double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d); +int fegetround(); long long int llrint(double x) { @@ -1737,17 +1524,8 @@ long long int llrint(double x) /* FUNCTION: llrintf */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - -#ifndef __CPROVER_FENV_H_INCLUDED -#include -#define __CPROVER_FENV_H_INCLUDED -#endif - float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d); +int fegetround(); long long int llrintf(float x) { @@ -1760,17 +1538,8 @@ long long int llrintf(float x) /* FUNCTION: llrintl */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - -#ifndef __CPROVER_FENV_H_INCLUDED -#include -#define __CPROVER_FENV_H_INCLUDED -#endif - long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d); +int fegetround(); long long int llrintl(long double x) { @@ -1792,11 +1561,6 @@ long long int llrintl(long double x) /* FUNCTION: lround */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - #ifndef __CPROVER_FENV_H_INCLUDED #include #define __CPROVER_FENV_H_INCLUDED @@ -1829,11 +1593,6 @@ long int lround(double x) /* FUNCTION: lroundf */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - #ifndef __CPROVER_FENV_H_INCLUDED #include #define __CPROVER_FENV_H_INCLUDED @@ -1866,11 +1625,6 @@ long int lroundf(float x) /* FUNCTION: lroundl */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - #ifndef __CPROVER_FENV_H_INCLUDED #include #define __CPROVER_FENV_H_INCLUDED @@ -1903,11 +1657,6 @@ long int lroundl(long double x) /* FUNCTION: llround */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - #ifndef __CPROVER_FENV_H_INCLUDED #include #define __CPROVER_FENV_H_INCLUDED @@ -1939,11 +1688,6 @@ long long int llround(double x) /* FUNCTION: llroundf */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - #ifndef __CPROVER_FENV_H_INCLUDED #include #define __CPROVER_FENV_H_INCLUDED @@ -1976,11 +1720,6 @@ long long int llroundf(float x) /* FUNCTION: llroundl */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - #ifndef __CPROVER_FENV_H_INCLUDED #include #define __CPROVER_FENV_H_INCLUDED @@ -2021,11 +1760,6 @@ long long int llroundl(long double x) /* FUNCTION: modf */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - #ifndef __CPROVER_FENV_H_INCLUDED #include #define __CPROVER_FENV_H_INCLUDED @@ -2041,11 +1775,6 @@ double modf(double x, double *iptr) /* FUNCTION: modff */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - #ifndef __CPROVER_FENV_H_INCLUDED #include #define __CPROVER_FENV_H_INCLUDED @@ -2062,11 +1791,6 @@ float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d); /* FUNCTION: modfl */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - #ifndef __CPROVER_FENV_H_INCLUDED #include #define __CPROVER_FENV_H_INCLUDED @@ -2145,11 +1869,6 @@ long double __sort_of_CPROVER_remainderl (int rounding_mode, long double x, long /* FUNCTION: fmod */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - #ifndef __CPROVER_FENV_H_INCLUDED #include #define __CPROVER_FENV_H_INCLUDED @@ -2162,11 +1881,6 @@ double fmod(double x, double y) { return __sort_of_CPROVER_remainder(FE_TOWARDZE /* FUNCTION: fmodf */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - #ifndef __CPROVER_FENV_H_INCLUDED #include #define __CPROVER_FENV_H_INCLUDED @@ -2179,11 +1893,6 @@ float fmodf(float x, float y) { return __sort_of_CPROVER_remainderf(FE_TOWARDZER /* FUNCTION: fmodl */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - #ifndef __CPROVER_FENV_H_INCLUDED #include #define __CPROVER_FENV_H_INCLUDED @@ -2210,11 +1919,6 @@ long double fmodl(long double x, long double y) { return __sort_of_CPROVER_remai /* FUNCTION: remainder */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - #ifndef __CPROVER_FENV_H_INCLUDED #include #define __CPROVER_FENV_H_INCLUDED @@ -2227,11 +1931,6 @@ double remainder(double x, double y) { return __sort_of_CPROVER_remainder(FE_TON /* FUNCTION: remainderf */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - #ifndef __CPROVER_FENV_H_INCLUDED #include #define __CPROVER_FENV_H_INCLUDED @@ -2244,11 +1943,6 @@ float remainderf(float x, float y) { return __sort_of_CPROVER_remainderf(FE_TONE /* FUNCTION: remainderl */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - #ifndef __CPROVER_FENV_H_INCLUDED #include #define __CPROVER_FENV_H_INCLUDED @@ -2271,47 +1965,26 @@ long double remainderl(long double x, long double y) { return __sort_of_CPROVER_ /* FUNCTION: copysign */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - -double fabs (double d); - double copysign(double x, double y) { - double abs = fabs(x); - return (signbit(y)) ? -abs : abs; + double abs = __CPROVER_fabs(x); + return (__CPROVER_signd(y)) ? -abs : abs; } /* FUNCTION: copysignf */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - -float fabsf (float d); - float copysignf(float x, float y) { - float abs = fabs(x); - return (signbit(y)) ? -abs : abs; + float abs = __CPROVER_fabs(x); + return (__CPROVER_signf(y)) ? -abs : abs; } /* FUNCTION: copysignl */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - -long double fabsl (long double d); - long double copysignl(long double x, long double y) { - long double abs = fabsl(x); - return (signbit(y)) ? -abs : abs; + long double abs = __CPROVER_fabsl(x); + return (__CPROVER_signld(y)) ? -abs : abs; } diff --git a/src/ansi-c/library/netdb.c b/src/ansi-c/library/netdb.c index 289e7945202..1869f350c52 100644 --- a/src/ansi-c/library/netdb.c +++ b/src/ansi-c/library/netdb.c @@ -1,6 +1,8 @@ -/* FUNCTION: gethostbyname */ - +#ifdef LIBRARY_CHECK #include +#endif + +/* FUNCTION: gethostbyname */ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); diff --git a/src/ansi-c/library/pthread_lib.c b/src/ansi-c/library/pthread_lib.c index 97194052a54..dc556485f23 100644 --- a/src/ansi-c/library/pthread_lib.c +++ b/src/ansi-c/library/pthread_lib.c @@ -1,10 +1,9 @@ -/* FUNCTION: pthread_mutexattr_settype */ - -#ifndef __CPROVER_PTHREAD_H_INCLUDED +#ifdef LIBRARY_CHECK #include -#define __CPROVER_PTHREAD_H_INCLUDED #endif +/* FUNCTION: pthread_mutexattr_settype */ + int __VERIFIER_nondet_int(); inline int pthread_mutexattr_settype(pthread_mutexattr_t *attr, int type) @@ -25,11 +24,6 @@ inline int pthread_mutexattr_settype(pthread_mutexattr_t *attr, int type) /* FUNCTION: pthread_cancel */ -#ifndef __CPROVER_PTHREAD_H_INCLUDED -#include -#define __CPROVER_PTHREAD_H_INCLUDED -#endif - int __VERIFIER_nondet_int(); inline int pthread_cancel(pthread_t thread) @@ -48,11 +42,6 @@ inline int pthread_cancel(pthread_t thread) /* FUNCTION: pthread_mutex_init */ -#ifndef __CPROVER_PTHREAD_H_INCLUDED -#include -#define __CPROVER_PTHREAD_H_INCLUDED -#endif - #ifndef __CPROVER_mutex_t_defined #define __CPROVER_mutex_t_defined #if defined __CYGWIN__ || defined __MINGW32__ || defined _WIN32 @@ -93,11 +82,6 @@ inline int pthread_mutex_init( /* FUNCTION: pthread_mutex_lock */ -#ifndef __CPROVER_PTHREAD_H_INCLUDED -#include -#define __CPROVER_PTHREAD_H_INCLUDED -#endif - #ifndef __CPROVER_mutex_t_defined #define __CPROVER_mutex_t_defined #if defined __CYGWIN__ || defined __MINGW32__ || defined _WIN32 @@ -142,11 +126,6 @@ inline int pthread_mutex_lock(pthread_mutex_t *mutex) /* FUNCTION: pthread_mutex_trylock */ -#ifndef __CPROVER_PTHREAD_H_INCLUDED -#include -#define __CPROVER_PTHREAD_H_INCLUDED -#endif - #ifndef __CPROVER_mutex_t_defined #define __CPROVER_mutex_t_defined #if defined __CYGWIN__ || defined __MINGW32__ || defined _WIN32 @@ -193,11 +172,6 @@ inline int pthread_mutex_trylock(pthread_mutex_t *mutex) /* FUNCTION: pthread_mutex_unlock */ -#ifndef __CPROVER_PTHREAD_H_INCLUDED -#include -#define __CPROVER_PTHREAD_H_INCLUDED -#endif - #ifndef __CPROVER_mutex_t_defined #define __CPROVER_mutex_t_defined #if defined __CYGWIN__ || defined __MINGW32__ || defined _WIN32 @@ -241,11 +215,6 @@ inline int pthread_mutex_unlock(pthread_mutex_t *mutex) /* FUNCTION: pthread_mutex_destroy */ -#ifndef __CPROVER_PTHREAD_H_INCLUDED -#include -#define __CPROVER_PTHREAD_H_INCLUDED -#endif - #ifndef __CPROVER_mutex_t_defined #define __CPROVER_mutex_t_defined #if defined __CYGWIN__ || defined __MINGW32__ || defined _WIN32 @@ -285,11 +254,6 @@ inline int pthread_mutex_destroy(pthread_mutex_t *mutex) /* FUNCTION: pthread_exit */ -#ifndef __CPROVER_PTHREAD_H_INCLUDED -#include -#define __CPROVER_PTHREAD_H_INCLUDED -#endif - extern __CPROVER_bool __CPROVER_threads_exited[]; extern __CPROVER_thread_local unsigned long __CPROVER_thread_id; @@ -303,11 +267,6 @@ inline void pthread_exit(void *value_ptr) /* FUNCTION: pthread_join */ -#ifndef __CPROVER_PTHREAD_H_INCLUDED -#include -#define __CPROVER_PTHREAD_H_INCLUDED -#endif - #ifndef __CPROVER_ERRNO_H_INCLUDED #include #define __CPROVER_ERRNO_H_INCLUDED @@ -338,11 +297,6 @@ inline int pthread_join(pthread_t thread, void **value_ptr) // This is for Apple -#ifndef __CPROVER_PTHREAD_H_INCLUDED -#include -#define __CPROVER_PTHREAD_H_INCLUDED -#endif - #ifndef __CPROVER_ERRNO_H_INCLUDED #include #define __CPROVER_ERRNO_H_INCLUDED @@ -373,11 +327,6 @@ inline int _pthread_join(pthread_t thread, void **value_ptr) /* FUNCTION: pthread_rwlock_destroy */ -#ifndef __CPROVER_PTHREAD_H_INCLUDED -#include -#define __CPROVER_PTHREAD_H_INCLUDED -#endif - inline int pthread_rwlock_destroy(pthread_rwlock_t *lock) { __CPROVER_HIDE:; @@ -394,11 +343,6 @@ inline int pthread_rwlock_destroy(pthread_rwlock_t *lock) /* FUNCTION: pthread_rwlock_init */ -#ifndef __CPROVER_PTHREAD_H_INCLUDED -#include -#define __CPROVER_PTHREAD_H_INCLUDED -#endif - #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS inline void pthread_rwlock_cleanup(void *p) { @@ -424,11 +368,6 @@ inline int pthread_rwlock_init(pthread_rwlock_t *lock, /* FUNCTION: pthread_rwlock_rdlock */ -#ifndef __CPROVER_PTHREAD_H_INCLUDED -#include -#define __CPROVER_PTHREAD_H_INCLUDED -#endif - inline int pthread_rwlock_rdlock(pthread_rwlock_t *lock) { __CPROVER_HIDE:; @@ -443,11 +382,6 @@ inline int pthread_rwlock_rdlock(pthread_rwlock_t *lock) /* FUNCTION: pthread_rwlock_tryrdlock */ -#ifndef __CPROVER_PTHREAD_H_INCLUDED -#include -#define __CPROVER_PTHREAD_H_INCLUDED -#endif - inline int pthread_rwlock_tryrdlock(pthread_rwlock_t *lock) { __CPROVER_HIDE:; @@ -460,11 +394,6 @@ inline int pthread_rwlock_tryrdlock(pthread_rwlock_t *lock) /* FUNCTION: pthread_rwlock_trywrlock */ -#ifndef __CPROVER_PTHREAD_H_INCLUDED -#include -#define __CPROVER_PTHREAD_H_INCLUDED -#endif - inline int pthread_rwlock_trywrlock(pthread_rwlock_t *lock) { __CPROVER_HIDE:; @@ -477,11 +406,6 @@ inline int pthread_rwlock_trywrlock(pthread_rwlock_t *lock) /* FUNCTION: pthread_rwlock_unlock */ -#ifndef __CPROVER_PTHREAD_H_INCLUDED -#include -#define __CPROVER_PTHREAD_H_INCLUDED -#endif - inline int pthread_rwlock_unlock(pthread_rwlock_t *lock) { __CPROVER_HIDE:; @@ -494,11 +418,6 @@ inline int pthread_rwlock_unlock(pthread_rwlock_t *lock) /* FUNCTION: pthread_rwlock_wrlock */ -#ifndef __CPROVER_PTHREAD_H_INCLUDED -#include -#define __CPROVER_PTHREAD_H_INCLUDED -#endif - inline int pthread_rwlock_wrlock(pthread_rwlock_t *lock) { __CPROVER_HIDE:; @@ -513,11 +432,6 @@ inline int pthread_rwlock_wrlock(pthread_rwlock_t *lock) /* FUNCTION: pthread_create */ -#ifndef __CPROVER_PTHREAD_H_INCLUDED -#include -#define __CPROVER_PTHREAD_H_INCLUDED -#endif - extern __CPROVER_bool __CPROVER_threads_exited[]; extern __CPROVER_thread_local unsigned long __CPROVER_thread_id; extern unsigned long __CPROVER_next_thread_id; @@ -560,11 +474,6 @@ inline int pthread_create( /* FUNCTION: pthread_cond_init */ -#ifndef __CPROVER_PTHREAD_H_INCLUDED -#include -#define __CPROVER_PTHREAD_H_INCLUDED -#endif - inline int pthread_cond_init( pthread_cond_t *cond, const pthread_condattr_t *attr) @@ -576,11 +485,6 @@ inline int pthread_cond_init( /* FUNCTION: pthread_cond_signal */ -#ifndef __CPROVER_PTHREAD_H_INCLUDED -#include -#define __CPROVER_PTHREAD_H_INCLUDED -#endif - inline int pthread_cond_signal( pthread_cond_t *cond) { __CPROVER_HIDE: @@ -592,11 +496,6 @@ inline int pthread_cond_signal( /* FUNCTION: pthread_cond_broadcast */ -#ifndef __CPROVER_PTHREAD_H_INCLUDED -#include -#define __CPROVER_PTHREAD_H_INCLUDED -#endif - inline int pthread_cond_broadcast( pthread_cond_t *cond) { __CPROVER_HIDE: @@ -608,11 +507,6 @@ inline int pthread_cond_broadcast( /* FUNCTION: pthread_cond_wait */ -#ifndef __CPROVER_PTHREAD_H_INCLUDED -#include -#define __CPROVER_PTHREAD_H_INCLUDED -#endif - inline int pthread_cond_wait( pthread_cond_t *cond, pthread_mutex_t *mutex) @@ -643,11 +537,6 @@ inline int pthread_cond_wait( /* FUNCTION: pthread_spin_lock */ -#ifndef __CPROVER_PTHREAD_H_INCLUDED -#include -#define __CPROVER_PTHREAD_H_INCLUDED -#endif - // no pthread_spinlock_t on the Mac #ifndef __APPLE__ int pthread_spin_lock(pthread_spinlock_t *lock) @@ -666,11 +555,6 @@ int pthread_spin_lock(pthread_spinlock_t *lock) /* FUNCTION: pthread_spin_unlock */ -#ifndef __CPROVER_PTHREAD_H_INCLUDED -#include -#define __CPROVER_PTHREAD_H_INCLUDED -#endif - // no pthread_spinlock_t on the Mac #ifndef __APPLE__ int pthread_spin_unlock(pthread_spinlock_t *lock) @@ -687,11 +571,6 @@ int pthread_spin_unlock(pthread_spinlock_t *lock) /* FUNCTION: pthread_spin_trylock */ -#ifndef __CPROVER_PTHREAD_H_INCLUDED -#include -#define __CPROVER_PTHREAD_H_INCLUDED -#endif - #ifndef __CPROVER_ERRNO_H_INCLUDED #include #define __CPROVER_ERRNO_H_INCLUDED @@ -721,11 +600,6 @@ int pthread_spin_trylock(pthread_spinlock_t *lock) /* FUNCTION: pthread_barrier_init */ -#ifndef __CPROVER_PTHREAD_H_INCLUDED -#include -#define __CPROVER_PTHREAD_H_INCLUDED -#endif - int __VERIFIER_nondet_int(); // no pthread_barrier_t on the Mac @@ -751,11 +625,6 @@ inline int pthread_barrier_init( /* FUNCTION: pthread_barrier_destroy */ -#ifndef __CPROVER_PTHREAD_H_INCLUDED -#include -#define __CPROVER_PTHREAD_H_INCLUDED -#endif - int __VERIFIER_nondet_int(); // no pthread_barrier_t on the Mac @@ -781,11 +650,6 @@ inline int pthread_barrier_destroy(pthread_barrier_t *barrier) /* FUNCTION: pthread_barrier_wait */ -#ifndef __CPROVER_PTHREAD_H_INCLUDED -#include -#define __CPROVER_PTHREAD_H_INCLUDED -#endif - int __VERIFIER_nondet_int(); // no pthread_barrier_t on the Mac diff --git a/src/ansi-c/library/semaphore.c b/src/ansi-c/library/semaphore.c index 5499a8ca72f..e2c458a7085 100644 --- a/src/ansi-c/library/semaphore.c +++ b/src/ansi-c/library/semaphore.c @@ -1,6 +1,8 @@ -/* FUNCTION: sem_init */ - +#ifdef LIBRARY_CHECK #include +#endif + +/* FUNCTION: sem_init */ inline int sem_init(sem_t *sem, int pshared, unsigned int value) { @@ -19,8 +21,6 @@ inline int sem_init(sem_t *sem, int pshared, unsigned int value) /* FUNCTION: sem_wait */ -#include - inline int sem_wait(sem_t *sem) { __CPROVER_HIDE:; @@ -38,8 +38,6 @@ inline int sem_wait(sem_t *sem) /* FUNCTION: sem_timedwait */ -#include - inline int sem_timedwait(sem_t *sem, const struct timespec *abstime) { __CPROVER_HIDE:; @@ -58,8 +56,6 @@ inline int sem_timedwait(sem_t *sem, const struct timespec *abstime) /* FUNCTION: sem_trywait */ -#include - inline int sem_trywait(sem_t *sem) { __CPROVER_HIDE:; @@ -77,8 +73,6 @@ inline int sem_trywait(sem_t *sem) /* FUNCTION: sem_post */ -#include - inline int sem_post(sem_t *sem) { __CPROVER_HIDE:; @@ -96,8 +90,6 @@ inline int sem_post(sem_t *sem) /* FUNCTION: sem_post_multiple */ -#include - inline int sem_post_multiple(sem_t *sem, int number) { __CPROVER_HIDE:; @@ -116,8 +108,6 @@ inline int sem_post_multiple(sem_t *sem, int number) /* FUNCTION: sem_getvalue */ -#include - inline int sem_getvalue(sem_t *sem, int *sval) { __CPROVER_HIDE:; @@ -136,8 +126,6 @@ inline int sem_getvalue(sem_t *sem, int *sval) /* FUNCTION: sem_destroy */ -#include - inline int sem_destroy(sem_t *sem) { __CPROVER_HIDE:; diff --git a/src/ansi-c/library/setjmp.c b/src/ansi-c/library/setjmp.c index 57c14998bb3..d56d06ca4f2 100644 --- a/src/ansi-c/library/setjmp.c +++ b/src/ansi-c/library/setjmp.c @@ -1,11 +1,9 @@ - -/* FUNCTION: longjmp */ - -#ifndef __CPROVER_SETJMP_H_INCLUDED +#ifdef LIBRARY_CHECK #include -#define __CPROVER_SETJMP_H_INCLUDED #endif +/* FUNCTION: longjmp */ + inline void longjmp(jmp_buf env, int val) { // does not return @@ -16,11 +14,6 @@ inline void longjmp(jmp_buf env, int val) /* FUNCTION: _longjmp */ -#ifndef __CPROVER_SETJMP_H_INCLUDED -#include -#define __CPROVER_SETJMP_H_INCLUDED -#endif - inline void _longjmp(jmp_buf env, int val) { // does not return @@ -31,11 +24,6 @@ inline void _longjmp(jmp_buf env, int val) /* FUNCTION: siglongjmp */ -#ifndef __CPROVER_SETJMP_H_INCLUDED -#include -#define __CPROVER_SETJMP_H_INCLUDED -#endif - inline void siglongjmp(sigjmp_buf env, int val) { // does not return @@ -46,11 +34,6 @@ inline void siglongjmp(sigjmp_buf env, int val) /* FUNCTION: setjmp */ -#ifndef __CPROVER_SETJMP_H_INCLUDED -#include -#define __CPROVER_SETJMP_H_INCLUDED -#endif - int __VERIFIER_nondet_int(); inline int setjmp(jmp_buf env) diff --git a/src/ansi-c/library/signal.c b/src/ansi-c/library/signal.c index 45fb723a7a4..a4f7d8a32f5 100644 --- a/src/ansi-c/library/signal.c +++ b/src/ansi-c/library/signal.c @@ -1,14 +1,8 @@ -/* FUNCTION: kill */ - -#ifndef __CPROVER_SYS_TYPES_H_INCLUDED +#ifdef LIBRARY_CHECK #include -#define __CPROVER_SYS_TYPES_H_INCLUDED #endif -#ifndef __CPROVER_SIGNAL_H_INCLUDED -#include -#define __CPROVER_SIGNAL_H_INCLUDED -#endif +/* FUNCTION: kill */ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); diff --git a/src/ansi-c/library/stdio.c b/src/ansi-c/library/stdio.c index d0ef51db92b..106f3832776 100644 --- a/src/ansi-c/library/stdio.c +++ b/src/ansi-c/library/stdio.c @@ -1,28 +1,22 @@ - -/* FUNCTION: putchar */ - -#ifndef __CPROVER_STDIO_H_INCLUDED +#ifdef LIBRARY_CHECK #include -#define __CPROVER_STDIO_H_INCLUDED +#include #endif +/* FUNCTION: putchar */ + __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); inline int putchar(int c) { __CPROVER_HIDE:; __CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool(); - printf("%c", c); + __CPROVER_printf("%c", c); return (error?-1:c); } /* FUNCTION: puts */ -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif - __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); int __VERIFIER_nondet_int(); @@ -31,23 +25,13 @@ inline int puts(const char *s) __CPROVER_HIDE:; __CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool(); int ret=__VERIFIER_nondet_int(); - printf("%s\n", s); + __CPROVER_printf("%s\n", s); if(error) ret=-1; else __CPROVER_assume(ret>=0); return ret; } /* FUNCTION: fopen */ -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif - -#ifndef __CPROVER_STDLIB_H_INCLUDED -#include -#define __CPROVER_STDLIB_H_INCLUDED -#endif - #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS inline void fclose_cleanup(void *stream) { @@ -59,6 +43,7 @@ inline void fclose_cleanup(void *stream) #endif __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); +void *malloc(__CPROVER_size_t malloc_size); inline FILE *fopen(const char *filename, const char *mode) { @@ -75,11 +60,11 @@ inline FILE *fopen(const char *filename, const char *mode) __CPROVER_bool fopen_error=__VERIFIER_nondet___CPROVER_bool(); #if !defined(__linux__) || defined(__GLIBC__) - fopen_result=fopen_error?NULL:malloc(sizeof(FILE)); + fopen_result = fopen_error ? 0 : malloc(sizeof(FILE)); #else // libraries need to expose the definition of FILE; this is the // case for musl - fopen_result=fopen_error?NULL:malloc(sizeof(int)); + fopen_result = fopen_error ? 0 : malloc(sizeof(int)); #endif #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS @@ -92,11 +77,6 @@ inline FILE *fopen(const char *filename, const char *mode) /* FUNCTION: freopen */ -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif - inline FILE* freopen(const char *filename, const char *mode, FILE *f) { __CPROVER_HIDE:; @@ -113,17 +93,8 @@ inline FILE* freopen(const char *filename, const char *mode, FILE *f) /* FUNCTION: fclose */ -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif - -#ifndef __CPROVER_STDLIB_H_INCLUDED -#include -#define __CPROVER_STDLIB_H_INCLUDED -#endif - int __VERIFIER_nondet_int(); +void free(void *ptr); inline int fclose(FILE *stream) { @@ -141,15 +112,7 @@ inline int fclose(FILE *stream) /* FUNCTION: fdopen */ -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif - -#ifndef __CPROVER_STDLIB_H_INCLUDED -#include -#define __CPROVER_STDLIB_H_INCLUDED -#endif +void *malloc(__CPROVER_size_t malloc_size); inline FILE *fdopen(int handle, const char *mode) { @@ -179,17 +142,9 @@ inline FILE *fdopen(int handle, const char *mode) // header files rename fdopen to _fdopen and would thus yield // unbounded recursion. -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif - -#ifndef __CPROVER_STDLIB_H_INCLUDED -#include -#define __CPROVER_STDLIB_H_INCLUDED -#endif - #ifdef __APPLE__ +void *malloc(__CPROVER_size_t malloc_size); + inline FILE *_fdopen(int handle, const char *mode) { __CPROVER_HIDE:; @@ -208,11 +163,6 @@ inline FILE *_fdopen(int handle, const char *mode) /* FUNCTION: fgets */ -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif - __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); int __VERIFIER_nondet_int(); @@ -262,22 +212,14 @@ char *fgets(char *str, int size, FILE *stream) /* FUNCTION: fread */ -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif +__CPROVER_size_t __VERIFIER_nondet_size_t(); -size_t __VERIFIER_nondet_size_t(); - -inline size_t fread( - void *ptr, - size_t size, - size_t nitems, - FILE *stream) +inline __CPROVER_size_t +fread(void *ptr, __CPROVER_size_t size, __CPROVER_size_t nitems, FILE *stream) { __CPROVER_HIDE:; - size_t nread=__VERIFIER_nondet_size_t(); - size_t bytes=nread*size; + __CPROVER_size_t nread = __VERIFIER_nondet_size_t(); + __CPROVER_size_t bytes = nread * size; __CPROVER_assume(nread<=nitems); #if !defined(__linux__) || defined(__GLIBC__) @@ -291,7 +233,7 @@ inline size_t fread( "fread file must be open"); #endif - for(size_t i=0; i -#define __CPROVER_STDIO_H_INCLUDED -#endif - int __VERIFIER_nondet_int(); inline int feof(FILE *stream) @@ -331,11 +268,6 @@ inline int feof(FILE *stream) /* FUNCTION: ferror */ -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif - int __VERIFIER_nondet_int(); inline int ferror(FILE *stream) @@ -360,11 +292,6 @@ inline int ferror(FILE *stream) /* FUNCTION: fileno */ -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif - int __VERIFIER_nondet_int(); inline int fileno(FILE *stream) @@ -389,11 +316,6 @@ inline int fileno(FILE *stream) /* FUNCTION: fputs */ -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif - int __VERIFIER_nondet_int(); inline int fputs(const char *s, FILE *stream) @@ -422,11 +344,6 @@ inline int fputs(const char *s, FILE *stream) /* FUNCTION: fflush */ -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif - int __VERIFIER_nondet_int(); inline int fflush(FILE *stream) @@ -447,11 +364,6 @@ inline int fflush(FILE *stream) /* FUNCTION: fpurge */ -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif - int __VERIFIER_nondet_int(); inline int fpurge(FILE *stream) @@ -476,11 +388,6 @@ inline int fpurge(FILE *stream) /* FUNCTION: fgetc */ -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif - int __VERIFIER_nondet_int(); inline int fgetc(FILE *stream) @@ -507,11 +414,6 @@ inline int fgetc(FILE *stream) /* FUNCTION: getc */ -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif - int __VERIFIER_nondet_int(); inline int getc(FILE *stream) @@ -540,11 +442,6 @@ inline int getc(FILE *stream) /* FUNCTION: getchar */ -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif - int __VERIFIER_nondet_int(); inline int getchar() @@ -559,11 +456,6 @@ inline int getchar() /* FUNCTION: getw */ -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif - int __VERIFIER_nondet_int(); inline int getw(FILE *stream) @@ -590,11 +482,6 @@ inline int getw(FILE *stream) /* FUNCTION: fseek */ -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif - int __VERIFIER_nondet_int(); inline int fseek(FILE *stream, long offset, int whence) @@ -620,11 +507,6 @@ inline int fseek(FILE *stream, long offset, int whence) /* FUNCTION: ftell */ -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif - long __VERIFIER_nondet_long(); inline long ftell(FILE *stream) @@ -648,11 +530,6 @@ inline long ftell(FILE *stream) /* FUNCTION: rewind */ -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif - void rewind(FILE *stream) { __CPROVER_HIDE: @@ -671,17 +548,12 @@ void rewind(FILE *stream) /* FUNCTION: fwrite */ -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif - -size_t __VERIFIER_nondet_size_t(); +__CPROVER_size_t __VERIFIER_nondet_size_t(); -size_t fwrite( +__CPROVER_size_t fwrite( const void *ptr, - size_t size, - size_t nitems, + __CPROVER_size_t size, + __CPROVER_size_t nitems, FILE *stream) { __CPROVER_HIDE:; @@ -699,18 +571,13 @@ size_t fwrite( "fwrite file must be open"); #endif - size_t nwrite=__VERIFIER_nondet_size_t(); + __CPROVER_size_t nwrite = __VERIFIER_nondet_size_t(); __CPROVER_assume(nwrite<=nitems); return nwrite; } /* FUNCTION: perror */ -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif - void perror(const char *s) { __CPROVER_HIDE:; @@ -721,7 +588,7 @@ void perror(const char *s) #endif // should go to stderr if(s[0]!=0) - printf("%s: ", s); + __CPROVER_printf("%s: ", s); } // TODO: print errno error @@ -729,15 +596,7 @@ void perror(const char *s) /* FUNCTION: fscanf */ -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif - -#ifndef __CPROVER_STDARG_H_INCLUDED -#include -#define __CPROVER_STDARG_H_INCLUDED -#endif +int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg); inline int fscanf(FILE *restrict stream, const char *restrict format, ...) { @@ -751,15 +610,7 @@ inline int fscanf(FILE *restrict stream, const char *restrict format, ...) /* FUNCTION: scanf */ -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif - -#ifndef __CPROVER_STDARG_H_INCLUDED -#include -#define __CPROVER_STDARG_H_INCLUDED -#endif +int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg); inline int scanf(const char *restrict format, ...) { @@ -773,15 +624,7 @@ inline int scanf(const char *restrict format, ...) /* FUNCTION: sscanf */ -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif - -#ifndef __CPROVER_STDARG_H_INCLUDED -#include -#define __CPROVER_STDARG_H_INCLUDED -#endif +int vsscanf(const char *restrict s, const char *restrict format, va_list arg); inline int sscanf(const char *restrict s, const char *restrict format, ...) { @@ -795,16 +638,6 @@ inline int sscanf(const char *restrict s, const char *restrict format, ...) /* FUNCTION: vfscanf */ -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif - -#ifndef __CPROVER_STDARG_H_INCLUDED -#include -#define __CPROVER_STDARG_H_INCLUDED -#endif - int __VERIFIER_nondet_int(); inline int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg) @@ -829,15 +662,7 @@ inline int vfscanf(FILE *restrict stream, const char *restrict format, va_list a /* FUNCTION: vscanf */ -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif - -#ifndef __CPROVER_STDARG_H_INCLUDED -#include -#define __CPROVER_STDARG_H_INCLUDED -#endif +int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg); inline int vscanf(const char *restrict format, va_list arg) { @@ -847,16 +672,6 @@ inline int vscanf(const char *restrict format, va_list arg) /* FUNCTION: vsscanf */ -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif - -#ifndef __CPROVER_STDARG_H_INCLUDED -#include -#define __CPROVER_STDARG_H_INCLUDED -#endif - int __VERIFIER_nondet_int(); inline int vsscanf(const char *restrict s, const char *restrict format, va_list arg) @@ -871,15 +686,7 @@ inline int vsscanf(const char *restrict s, const char *restrict format, va_list /* FUNCTION: fprintf */ -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif - -#ifndef __CPROVER_STDARG_H_INCLUDED -#include -#define __CPROVER_STDARG_H_INCLUDED -#endif +int vfprintf(FILE *stream, const char *restrict format, va_list arg); inline int fprintf(FILE *stream, const char *restrict format, ...) { @@ -893,16 +700,6 @@ inline int fprintf(FILE *stream, const char *restrict format, ...) /* FUNCTION: vfprintf */ -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif - -#ifndef __CPROVER_STDARG_H_INCLUDED -#include -#define __CPROVER_STDARG_H_INCLUDED -#endif - int __VERIFIER_nondet_int(); inline int vfprintf(FILE *stream, const char *restrict format, va_list arg) @@ -929,23 +726,9 @@ inline int vfprintf(FILE *stream, const char *restrict format, va_list arg) /* FUNCTION: vasprintf */ -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif - -#ifndef __CPROVER_STDARG_H_INCLUDED -#include -#define __CPROVER_STDARG_H_INCLUDED -#endif - -#ifndef __CPROVER_STDLIB_H_INCLUDED -#include -#define __CPROVER_STDLIB_H_INCLUDED -#endif - char __VERIFIER_nondet_char(); int __VERIFIER_nondet_int(); +void *malloc(__CPROVER_size_t malloc_size); inline int vasprintf(char **ptr, const char *fmt, va_list ap) { diff --git a/src/ansi-c/library/string.c b/src/ansi-c/library/string.c index 8781b77c35d..21b59222222 100644 --- a/src/ansi-c/library/string.c +++ b/src/ansi-c/library/string.c @@ -47,7 +47,7 @@ __inline char *__builtin___strcat_chk(char *dst, const char *src, __CPROVER_size __CPROVER_assert(__CPROVER_buffer_size(dst)>new_size, "strcat buffer overflow"); __CPROVER_size_t old_size=__CPROVER_zero_string_length(dst); - //" for(size_t i=0; i<__CPROVER_zero_string_length(src); i++) + //" for(__CPROVER_size_t i=0; i<__CPROVER_zero_string_length(src); i++) //" dst[old_size+i]; dst[new_size]=0; __CPROVER_is_zero_string(dst)=1; @@ -120,13 +120,6 @@ __inline char *__builtin___strncat_chk( /* FUNCTION: strcpy */ -#ifndef __CPROVER_STRING_H_INCLUDED -#include -#define __CPROVER_STRING_H_INCLUDED -#endif - -#undef strcpy - inline char *strcpy(char *dst, const char *src) { __CPROVER_HIDE:; @@ -158,14 +151,7 @@ inline char *strcpy(char *dst, const char *src) /* FUNCTION: strncpy */ -#ifndef __CPROVER_STRING_H_INCLUDED -#include -#define __CPROVER_STRING_H_INCLUDED -#endif - -#undef strncpy - -inline char *strncpy(char *dst, const char *src, size_t n) +inline char *strncpy(char *dst, const char *src, __CPROVER_size_t n) { __CPROVER_HIDE:; #ifdef __CPROVER_STRING_ABSTRACTION @@ -197,12 +183,11 @@ inline char *strncpy(char *dst, const char *src, size_t n) /* FUNCTION: __builtin___strncpy_chk */ -#ifndef __CPROVER_STRING_H_INCLUDED -#include -#define __CPROVER_STRING_H_INCLUDED -#endif - -inline char *__builtin___strncpy_chk(char *dst, const char *src, size_t n, size_t object_size) +inline char *__builtin___strncpy_chk( + char *dst, + const char *src, + __CPROVER_size_t n, + __CPROVER_size_t object_size) { __CPROVER_HIDE:; #ifdef __CPROVER_STRING_ABSTRACTION @@ -237,13 +222,6 @@ inline char *__builtin___strncpy_chk(char *dst, const char *src, size_t n, size_ /* FUNCTION: strcat */ -#ifndef __CPROVER_STRING_H_INCLUDED -#include -#define __CPROVER_STRING_H_INCLUDED -#endif - -#undef strcat - inline char *strcat(char *dst, const char *src) { __CPROVER_HIDE:; @@ -257,7 +235,7 @@ inline char *strcat(char *dst, const char *src) __CPROVER_assert(__CPROVER_buffer_size(dst)>new_size, "strcat buffer overflow"); __CPROVER_size_t old_size=__CPROVER_zero_string_length(dst); - //" for(size_t i=0; i<__CPROVER_zero_string_length(src); i++) + //" for(__CPROVER_size_t i=0; i<__CPROVER_zero_string_length(src); i++) //" dst[old_size+i]; dst[new_size]=0; __CPROVER_is_zero_string(dst)=1; @@ -283,14 +261,7 @@ inline char *strcat(char *dst, const char *src) /* FUNCTION: strncat */ -#ifndef __CPROVER_STRING_H_INCLUDED -#include -#define __CPROVER_STRING_H_INCLUDED -#endif - -#undef strncat - -inline char *strncat(char *dst, const char *src, size_t n) +inline char *strncat(char *dst, const char *src, __CPROVER_size_t n) { __CPROVER_HIDE:; #ifdef __CPROVER_STRING_ABSTRACTION @@ -334,13 +305,6 @@ inline char *strncat(char *dst, const char *src, size_t n) /* FUNCTION: strcmp */ -#ifndef __CPROVER_STRING_H_INCLUDED -#include -#define __CPROVER_STRING_H_INCLUDED -#endif - -#undef strcmp - inline int strcmp(const char *s1, const char *s2) { __CPROVER_HIDE:; @@ -380,13 +344,6 @@ inline int strcmp(const char *s1, const char *s2) /* FUNCTION: strcasecmp */ -#ifndef __CPROVER_STRING_H_INCLUDED -#include -#define __CPROVER_STRING_H_INCLUDED -#endif - -#undef strcasecmp - inline int strcasecmp(const char *s1, const char *s2) { __CPROVER_HIDE:; @@ -429,14 +386,7 @@ inline int strcasecmp(const char *s1, const char *s2) /* FUNCTION: strncmp */ -#ifndef __CPROVER_STRING_H_INCLUDED -#include -#define __CPROVER_STRING_H_INCLUDED -#endif - -#undef strncmp - -inline int strncmp(const char *s1, const char *s2, size_t n) +inline int strncmp(const char *s1, const char *s2, __CPROVER_size_t n) { __CPROVER_HIDE:; #ifdef __CPROVER_STRING_ABSTRACTION @@ -471,14 +421,7 @@ inline int strncmp(const char *s1, const char *s2, size_t n) /* FUNCTION: strncasecmp */ -#ifndef __CPROVER_STRING_H_INCLUDED -#include -#define __CPROVER_STRING_H_INCLUDED -#endif - -#undef strncasecmp - -inline int strncasecmp(const char *s1, const char *s2, size_t n) +inline int strncasecmp(const char *s1, const char *s2, __CPROVER_size_t n) { __CPROVER_HIDE:; #ifdef __CPROVER_STRING_ABSTRACTION @@ -516,14 +459,7 @@ inline int strncasecmp(const char *s1, const char *s2, size_t n) /* FUNCTION: strlen */ -#ifndef __CPROVER_STRING_H_INCLUDED -#include -#define __CPROVER_STRING_H_INCLUDED -#endif - -#undef strlen - -inline size_t strlen(const char *s) +inline __CPROVER_size_t strlen(const char *s) { __CPROVER_HIDE:; #ifdef __CPROVER_STRING_ABSTRACTION @@ -539,18 +475,8 @@ inline size_t strlen(const char *s) /* FUNCTION: strdup */ -#ifndef __CPROVER_STRING_H_INCLUDED -#include -#define __CPROVER_STRING_H_INCLUDED -#endif - -#ifndef __CPROVER_STDLIB_H_INCLUDED -#include -#define __CPROVER_STDLIB_H_INCLUDED -#endif - -#undef strdup -#undef strcpy +void *malloc(__CPROVER_size_t malloc_size); +char *strcpy(char *dst, const char *src); inline char *strdup(const char *str) { @@ -568,14 +494,7 @@ inline char *strdup(const char *str) /* FUNCTION: memcpy */ -#ifndef __CPROVER_STRING_H_INCLUDED -#include -#define __CPROVER_STRING_H_INCLUDED -#endif - -#undef memcpy - -void *memcpy(void *dst, const void *src, size_t n) +void *memcpy(void *dst, const void *src, __CPROVER_size_t n) { __CPROVER_HIDE: #ifdef __CPROVER_STRING_ABSTRACTION @@ -583,7 +502,7 @@ void *memcpy(void *dst, const void *src, size_t n) "memcpy buffer overflow"); __CPROVER_precondition(__CPROVER_buffer_size(dst)>=n, "memcpy buffer overflow"); - // for(size_t i=0; i __CPROVER_zero_string_length(src)) { @@ -625,7 +544,7 @@ void *__builtin___memcpy_chk(void *dst, const void *src, __CPROVER_size_t n, __C "memcpy buffer overflow"); __CPROVER_precondition(__CPROVER_buffer_size(dst)==s, "builtin object size"); - // for(size_t i=0; i __CPROVER_zero_string_length(src)) { @@ -658,20 +577,13 @@ void *__builtin___memcpy_chk(void *dst, const void *src, __CPROVER_size_t n, __C /* FUNCTION: memset */ -#ifndef __CPROVER_STRING_H_INCLUDED -#include -#define __CPROVER_STRING_H_INCLUDED -#endif - -#undef memset - -void *memset(void *s, int c, size_t n) +void *memset(void *s, int c, __CPROVER_size_t n) { __CPROVER_HIDE:; #ifdef __CPROVER_STRING_ABSTRACTION __CPROVER_precondition(__CPROVER_buffer_size(s)>=n, "memset buffer overflow"); - // for(size_t i=0; i __CPROVER_zero_string_length(s)) { @@ -708,7 +620,7 @@ void *__builtin_memset(void *s, int c, __CPROVER_size_t n) #ifdef __CPROVER_STRING_ABSTRACTION __CPROVER_precondition(__CPROVER_buffer_size(s)>=n, "memset buffer overflow"); - // for(size_t i=0; i __CPROVER_zero_string_length(s)) { @@ -749,7 +661,7 @@ void *__builtin___memset_chk(void *s, int c, __CPROVER_size_t n, __CPROVER_size_ "memset buffer overflow"); __CPROVER_precondition(__CPROVER_buffer_size(s)==size, "builtin object size"); - // for(size_t i=0; i __CPROVER_zero_string_length(s)) { @@ -781,14 +693,7 @@ void *__builtin___memset_chk(void *s, int c, __CPROVER_size_t n, __CPROVER_size_ /* FUNCTION: memmove */ -#ifndef __CPROVER_STRING_H_INCLUDED -#include -#define __CPROVER_STRING_H_INCLUDED -#endif - -#undef memmove - -void *memmove(void *dest, const void *src, size_t n) +void *memmove(void *dest, const void *src, __CPROVER_size_t n) { __CPROVER_HIDE:; #ifdef __CPROVER_STRING_ABSTRACTION @@ -821,14 +726,11 @@ void *memmove(void *dest, const void *src, size_t n) /* FUNCTION: __builtin___memmove_chk */ -#ifndef __CPROVER_STRING_H_INCLUDED -#include -#define __CPROVER_STRING_H_INCLUDED -#endif - -#undef memmove - -void *__builtin___memmove_chk(void *dest, const void *src, size_t n, __CPROVER_size_t size) +void *__builtin___memmove_chk( + void *dest, + const void *src, + __CPROVER_size_t n, + __CPROVER_size_t size) { __CPROVER_HIDE:; #ifdef __CPROVER_STRING_ABSTRACTION @@ -866,14 +768,7 @@ void *__builtin___memmove_chk(void *dest, const void *src, size_t n, __CPROVER_s /* FUNCTION: memcmp */ -#ifndef __CPROVER_STRING_H_INCLUDED -#include -#define __CPROVER_STRING_H_INCLUDED -#endif - -#undef memcmp - -inline int memcmp(const void *s1, const void *s2, size_t n) +inline int memcmp(const void *s1, const void *s2, __CPROVER_size_t n) { __CPROVER_HIDE:; int res=0; @@ -896,13 +791,6 @@ inline int memcmp(const void *s1, const void *s2, size_t n) /* FUNCTION: strchr */ -#ifndef __CPROVER_STRING_H_INCLUDED -#include -#define __CPROVER_STRING_H_INCLUDED -#endif - -#undef strchr - inline char *strchr(const char *src, int c) { __CPROVER_HIDE:; @@ -925,13 +813,6 @@ inline char *strchr(const char *src, int c) /* FUNCTION: strrchr */ -#ifndef __CPROVER_STRING_H_INCLUDED -#include -#define __CPROVER_STRING_H_INCLUDED -#endif - -#undef strchr - inline char *strrchr(const char *src, int c) { __CPROVER_HIDE:; @@ -954,11 +835,6 @@ inline char *strrchr(const char *src, int c) /* FUNCTION: strerror */ -#ifndef __CPROVER_STRING_H_INCLUDED -#include -#define __CPROVER_STRING_H_INCLUDED -#endif - char *strerror(int errnum) { __CPROVER_HIDE:; diff --git a/src/ansi-c/library/syslog.c b/src/ansi-c/library/syslog.c index 4acd52ca16c..c72f9c45dd0 100644 --- a/src/ansi-c/library/syslog.c +++ b/src/ansi-c/library/syslog.c @@ -1,10 +1,5 @@ /* FUNCTION: openlog */ -#ifndef __CPROVER_SYSLOG_H_INCLUDED -#include -#define __CPROVER_SYSLOG_H_INCLUDED -#endif - void openlog(const char *ident, int option, int facility) { (void)*ident; @@ -14,22 +9,12 @@ void openlog(const char *ident, int option, int facility) /* FUNCTION: closelog */ -#ifndef __CPROVER_SYSLOG_H_INCLUDED -#include -#define __CPROVER_SYSLOG_H_INCLUDED -#endif - void closelog(void) { } /* FUNCTION: syslog */ -#ifndef __CPROVER_SYSLOG_H_INCLUDED -#include -#define __CPROVER_SYSLOG_H_INCLUDED -#endif - void syslog(int priority, const char *format, ...) { (void)priority; diff --git a/src/ansi-c/library/threads.c b/src/ansi-c/library/threads.c index d0c10ac03e0..bd63208ac7d 100644 --- a/src/ansi-c/library/threads.c +++ b/src/ansi-c/library/threads.c @@ -1,45 +1,29 @@ +#ifdef LIBRARY_CHECK +#include +#endif + /* FUNCTION: thrd_create */ // following http://en.cppreference.com/w/c/thread -#ifndef __CPROVER_THREADS_H_INCLUDED -#include -#define __CPROVER_THREADS_H_INCLUDED -#endif - int thrd_create(thrd_t *thr, thrd_start_t func, void *arg) { } /* FUNCTION: thrd_equal */ -#ifndef __CPROVER_THREADS_H_INCLUDED -#include -#define __CPROVER_THREADS_H_INCLUDED -#endif - int thrd_equal( thrd_t lhs, thrd_t rhs ) { } /* FUNCTION: thrd_current */ -#ifndef __CPROVER_THREADS_H_INCLUDED -#include -#define __CPROVER_THREADS_H_INCLUDED -#endif - thrd_t thrd_current() { } /* FUNCTION: thrd_sleep */ -#ifndef __CPROVER_THREADS_H_INCLUDED -#include -#define __CPROVER_THREADS_H_INCLUDED -#endif - int thrd_sleep(const struct timespec* time_point, struct timespec* remaining) { @@ -60,33 +44,18 @@ void thrd_exit(int res) /* FUNCTION: mtx_init */ -#ifndef __CPROVER_THREADS_H_INCLUDED -#include -#define __CPROVER_THREADS_H_INCLUDED -#endif - int mtx_init( mtx_t* mutex, int type ) { } /* FUNCTION: mtx_lock */ -#ifndef __CPROVER_THREADS_H_INCLUDED -#include -#define __CPROVER_THREADS_H_INCLUDED -#endif - int mtx_lock(mtx_t* mutex) { } /* FUNCTION: mtx_timedlock */ -#ifndef __CPROVER_THREADS_H_INCLUDED -#include -#define __CPROVER_THREADS_H_INCLUDED -#endif - int mtx_timedlock(mtx_t *restrict mutex, const struct timespec *restrict time_point) { @@ -95,22 +64,12 @@ int mtx_timedlock(mtx_t *restrict mutex, /* FUNCTION: mtx_trylock */ -#ifndef __CPROVER_THREADS_H_INCLUDED -#include -#define __CPROVER_THREADS_H_INCLUDED -#endif - int mtx_trylock(mtx_t *mutex) { } /* FUNCTION: mtx_unlock */ -#ifndef __CPROVER_THREADS_H_INCLUDED -#include -#define __CPROVER_THREADS_H_INCLUDED -#endif - int mtx_unlock(mtx_t *mutex) { @@ -118,44 +77,24 @@ int mtx_unlock(mtx_t *mutex) /* FUNCTION: mtx_destroy */ -#ifndef __CPROVER_THREADS_H_INCLUDED -#include -#define __CPROVER_THREADS_H_INCLUDED -#endif - void mtx_destroy(mtx_t *mutex) { } /* FUNCTION: call_once */ -#ifndef __CPROVER_THREADS_H_INCLUDED -#include -#define __CPROVER_THREADS_H_INCLUDED -#endif - void call_once(once_flag* flag, void (*func)(void)) { } /* FUNCTION: cnd_init */ -#ifndef __CPROVER_THREADS_H_INCLUDED -#include -#define __CPROVER_THREADS_H_INCLUDED -#endif - int cnd_init(cnd_t* cond) { } /* FUNCTION: cnd_signal */ -#ifndef __CPROVER_THREADS_H_INCLUDED -#include -#define __CPROVER_THREADS_H_INCLUDED -#endif - int cnd_signal(cnd_t *cond) { @@ -163,33 +102,18 @@ int cnd_signal(cnd_t *cond) /* FUNCTION: cnd_broadcast */ -#ifndef __CPROVER_THREADS_H_INCLUDED -#include -#define __CPROVER_THREADS_H_INCLUDED -#endif - int cnd_broadcast(cnd_t *cond) { } /* FUNCTION: cnd_wait */ -#ifndef __CPROVER_THREADS_H_INCLUDED -#include -#define __CPROVER_THREADS_H_INCLUDED -#endif - int cnd_wait(cnd_t* cond, mtx_t* mutex) { } /* FUNCTION: cnd_timedwait */ -#ifndef __CPROVER_THREADS_H_INCLUDED -#include -#define __CPROVER_THREADS_H_INCLUDED -#endif - int cnd_timedwait(cnd_t* restrict cond, mtx_t* restrict mutex, const struct timespec* restrict time_point) { @@ -197,11 +121,6 @@ int cnd_timedwait(cnd_t* restrict cond, mtx_t* restrict mutex, /* FUNCTION: cnd_destroy */ -#ifndef __CPROVER_THREADS_H_INCLUDED -#include -#define __CPROVER_THREADS_H_INCLUDED -#endif - void cnd_destroy(cnd_t* cond) { } diff --git a/src/ansi-c/library/time.c b/src/ansi-c/library/time.c index 71606de0012..d92098e6584 100644 --- a/src/ansi-c/library/time.c +++ b/src/ansi-c/library/time.c @@ -1,11 +1,8 @@ -/* FUNCTION: time */ - -#ifndef __CPROVER_TIME_H_INCLUDED +#ifdef LIBRARY_CHECK #include -#define __CPROVER_TIME_H_INCLUDED #endif -#undef time +/* FUNCTION: time */ time_t __VERIFIER_nondet_time_t(); @@ -18,13 +15,6 @@ time_t time(time_t *tloc) /* FUNCTION: gmtime */ -#ifndef __CPROVER_TIME_H_INCLUDED -#include -#define __CPROVER_TIME_H_INCLUDED -#endif - -#undef gmtime - struct tm *gmtime(const time_t *clock) { // not very general, may be too restrictive @@ -43,13 +33,6 @@ struct tm *gmtime(const time_t *clock) /* FUNCTION: gmtime_r */ -#ifndef __CPROVER_TIME_H_INCLUDED -#include -#define __CPROVER_TIME_H_INCLUDED -#endif - -#undef gmtime - struct tm *gmtime_r(const time_t *clock, struct tm *result) { // need to set the fields to something meaningful @@ -59,13 +42,6 @@ struct tm *gmtime_r(const time_t *clock, struct tm *result) /* FUNCTION: localtime */ -#ifndef __CPROVER_TIME_H_INCLUDED -#include -#define __CPROVER_TIME_H_INCLUDED -#endif - -#undef localtime - struct tm *localtime(const time_t *clock) { // not very general, may be too restrictive @@ -84,13 +60,6 @@ struct tm *localtime(const time_t *clock) /* FUNCTION: localtime_r */ -#ifndef __CPROVER_TIME_H_INCLUDED -#include -#define __CPROVER_TIME_H_INCLUDED -#endif - -#undef localtime - struct tm *localtime_r(const time_t *clock, struct tm *result) { // need to set the fields to something meaningful @@ -100,13 +69,6 @@ struct tm *localtime_r(const time_t *clock, struct tm *result) /* FUNCTION: mktime */ -#ifndef __CPROVER_TIME_H_INCLUDED -#include -#define __CPROVER_TIME_H_INCLUDED -#endif - -#undef mktime - time_t __VERIFIER_nondet_time_t(); time_t mktime(struct tm *timeptr) @@ -118,13 +80,6 @@ time_t mktime(struct tm *timeptr) /* FUNCTION: timegm */ -#ifndef __CPROVER_TIME_H_INCLUDED -#include -#define __CPROVER_TIME_H_INCLUDED -#endif - -#undef timegm - time_t __VERIFIER_nondet_time_t(); time_t timegm(struct tm *timeptr) @@ -136,11 +91,6 @@ time_t timegm(struct tm *timeptr) /* FUNCTION: asctime */ -#ifndef __CPROVER_TIME_H_INCLUDED -#include -#define __CPROVER_TIME_H_INCLUDED -#endif - char *asctime(const struct tm *timeptr) { (void)*timeptr; @@ -157,11 +107,6 @@ char *asctime(const struct tm *timeptr) /* FUNCTION: ctime */ -#ifndef __CPROVER_TIME_H_INCLUDED -#include -#define __CPROVER_TIME_H_INCLUDED -#endif - char *ctime(const time_t *clock) { (void)*clock; diff --git a/src/ansi-c/library/unistd.c b/src/ansi-c/library/unistd.c index 7f57c5a5d45..806bfae7302 100644 --- a/src/ansi-c/library/unistd.c +++ b/src/ansi-c/library/unistd.c @@ -126,12 +126,8 @@ inline int _close(int fildes) #define ret_type int #define size_type unsigned #else -#ifndef __CPROVER_SYS_TYPES_H_INCLUDED -#include -#define __CPROVER_SYS_TYPES_H_INCLUDED -#endif -#define ret_type ssize_t -#define size_type size_t +#define ret_type long int +#define size_type __CPROVER_size_t #endif extern struct __CPROVER_pipet __CPROVER_pipes[]; @@ -175,12 +171,8 @@ ret_type write(int fildes, const void *buf, size_type nbyte) #define ret_type int #define size_type unsigned #else -#ifndef __CPROVER_SYS_TYPES_H_INCLUDED -#include -#define __CPROVER_SYS_TYPES_H_INCLUDED -#endif -#define ret_type ssize_t -#define size_type size_t +#define ret_type long int +#define size_type __CPROVER_size_t #endif ret_type write(int fildes, const void *buf, size_type nbyte); @@ -200,12 +192,8 @@ inline ret_type _write(int fildes, const void *buf, size_type nbyte) #define ret_type int #define size_type unsigned #else -#ifndef __CPROVER_SYS_TYPES_H_INCLUDED -#include -#define __CPROVER_SYS_TYPES_H_INCLUDED -#endif -#define ret_type ssize_t -#define size_type size_t +#define ret_type long int +#define size_type __CPROVER_size_t #endif extern struct __CPROVER_pipet __CPROVER_pipes[]; @@ -279,12 +267,8 @@ ret_type read(int fildes, void *buf, size_type nbyte) #define ret_type int #define size_type unsigned #else -#ifndef __CPROVER_SYS_TYPES_H_INCLUDED -#include -#define __CPROVER_SYS_TYPES_H_INCLUDED -#endif -#define ret_type ssize_t -#define size_type size_t +#define ret_type long int +#define size_type __CPROVER_size_t #endif ret_type read(int fildes, void *buf, size_type nbyte); diff --git a/src/ansi-c/library/windows.c b/src/ansi-c/library/windows.c index 1c6b5e758bf..d50065dc2a2 100644 --- a/src/ansi-c/library/windows.c +++ b/src/ansi-c/library/windows.c @@ -1,7 +1,12 @@ +#ifdef _WIN32 +#ifdef LIBRARY_CHECK +#include +#endif +#endif + /* FUNCTION: QueryPerformanceFrequency */ #ifdef _WIN32 -#include BOOL QueryPerformanceFrequency(LARGE_INTEGER *lpFrequency) { @@ -18,7 +23,6 @@ BOOL QueryPerformanceFrequency(LARGE_INTEGER *lpFrequency) /* FUNCTION: ExitThread */ #ifdef _WIN32 -#include inline VOID ExitThread(DWORD dwExitCode) { @@ -30,7 +34,6 @@ inline VOID ExitThread(DWORD dwExitCode) /* FUNCTION: CreateThread */ #ifdef _WIN32 -#include inline HANDLE CreateThread( LPSECURITY_ATTRIBUTES lpThreadAttributes,