Merge pull request #1326 from tautschnig/ansi-c-library-fixes

[develop->master] C library: cleanup and syntax error fixes

Author: Daniel Kroening

.travis.yml

@@ -158,6 +158,8 @@ install:
   - ccache --max-size=1G
   - COMMAND="make -C src minisat2-download" &&
     eval ${PRE_COMMAND} ${COMMAND}
+  - COMMAND="make -C src/ansi-c library_check" &&
+    eval ${PRE_COMMAND} ${COMMAND}
   - COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g $EXTRA_CXXFLAGS\" -j2" &&
     eval ${PRE_COMMAND} ${COMMAND}
   - COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"$FLAGS $EXTRA_CXXFLAGS\" -j2 clobber.dir memory-models.dir musketeer.dir" &&

src/ansi-c/Makefile

@@ -94,14 +94,15 @@ else
 endif
 library_check: library/*.c
 	for f in $(filter-out $(platform_unavail), $^) ; do \
+		echo "Checking $$f" ; \
 		cp $$f __libcheck.c ; \
-		sed -i 's/__builtin_[^v]/s&/' __libcheck.c ; \
-		sed -i 's/__sync_/s&/' __libcheck.c ; \
-		sed -i 's/__noop/s&/' __libcheck.c ; \
+		perl -p -i -e 's/(__builtin_[^v])/s$$1/' __libcheck.c ; \
+		perl -p -i -e 's/(__sync_)/s$$1/' __libcheck.c ; \
+		perl -p -i -e 's/(__noop)/s$$1/' __libcheck.c ; \
 		$(CC) -std=gnu99 -E -include library/cprover.h -D__CPROVER_bool=_Bool \
 			-D__CPROVER_thread_local=__thread -DLIBRARY_CHECK -o __libcheck.i __libcheck.c ; \
 		$(CC) -S -Wall -Werror -pedantic -Wextra -std=gnu99 __libcheck.i -o __libcheck.s \
-			-Wno-unused-label -Wno-uninitialized ; \
+			-Wno-unused-label ; \
 		ec=$$? ; \
 		$(RM) __libcheck.s __libcheck.i __libcheck.c ; \
 		[ $$ec -eq 0 ] || exit $$ec ; \

src/ansi-c/library/fcntl.c

@@ -5,10 +5,12 @@
 #define __CPROVER_FCNTL_H_INCLUDED
 #endif
 
+int __VERIFIER_nondet_int();
+
 int fcntl(int fd, int cmd, ...)
 {
 __CPROVER_HIDE:;
-  int return_value;
+  int return_value=__VERIFIER_nondet_int();
   (void)fd;
   (void)cmd;
   return return_value;

src/ansi-c/library/getopt.c

@@ -8,8 +8,11 @@ extern int optind;
 #define __CPROVER_STRING_H_INCLUDED
 #endif
 
-inline int getopt(int argc, char * const argv[],
-                  const char *optstring)
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+size_t __VERIFIER_nondet_size_t();
+
+inline int getopt(
+  int argc, char * const argv[], const char *optstring)
 {
   __CPROVER_HIDE:;
   int result=-1;
@@ -20,25 +23,26 @@ inline int getopt(int argc, char * const argv[],
   if(optind>=argc || argv[optind][0]!='-')
     return -1;
 
-  size_t result_index;
+  size_t result_index=__VERIFIER_nondet_size_t();
   __CPROVER_assume(
     result_index<strlen(optstring) && optstring[result_index]!=':');
   #ifdef __CPROVER_STRING_ABSTRACTION
   __CPROVER_assert(__CPROVER_is_zero_string(optstring),
     "getopt zero-termination of 3rd argument");
   #endif
 
-  _Bool found;
+  __CPROVER_bool found=__VERIFIER_nondet___CPROVER_bool();
   if(found)
   {
     result=optstring[result_index];
+    __CPROVER_bool skipped=__VERIFIER_nondet___CPROVER_bool();
     if(skipped)
       ++optind;
   }
 
   if(result!=-1 && optind<argc && optstring[result_index+1]==':')
   {
-    _Bool has_no_arg;
+    __CPROVER_bool has_no_arg=__VERIFIER_nondet___CPROVER_bool();
     if(has_no_arg)
     {
       optarg=argv[optind];
@@ -53,10 +57,17 @@ inline int getopt(int argc, char * const argv[],
 
 /* FUNCTION: getopt_long */
 
-int getopt(int argc, char * const argv[], const char *optstring);
+#ifndef __CPROVER_GETOPT_H_INCLUDED
+#include <getopt.h>
+#define __CPROVER_GETOPT_H_INCLUDED
+#endif
 
-inline int getopt_long(int argc, char * const argv[], const char *optstring,
-                const struct option *longopts, int *longindex)
+inline int getopt_long(
+  int argc,
+  char * const argv[],
+  const char *optstring,
+  const struct option *longopts,
+  int *longindex)
 {
   // trigger valid-pointer checks (if enabled), even though we don't
   // use the parameter in this model

src/ansi-c/library/inet.c

@@ -2,6 +2,8 @@
 
 #include <arpa/inet.h>
 
+in_addr_t __VERIFIER_nondet_in_addr_t();
+
 in_addr_t inet_addr(const char *cp)
 {
   __CPROVER_HIDE:;
@@ -10,12 +12,14 @@ in_addr_t inet_addr(const char *cp)
   __CPROVER_assert(__CPROVER_is_zero_string(cp), "inet_addr zero-termination of argument");
   #endif
 
-  in_addr_t result;
+  in_addr_t result=__VERIFIER_nondet_in_addr_t();
   return result;
 }
 
 /* FUNCTION: inet_aton */
 
+int __VERIFIER_nondet_int();
+
 int inet_aton(const char *cp, struct in_addr *pin)
 {
   __CPROVER_HIDE:;
@@ -25,12 +29,14 @@ int inet_aton(const char *cp, struct in_addr *pin)
   __CPROVER_assert(__CPROVER_is_zero_string(cp), "inet_aton zero-termination of name argument");
   #endif
 
-  int result;
+  int result=__VERIFIER_nondet_int();
   return result;
 }
 
 /* FUNCTION: inet_network */
 
+in_addr_t __VERIFIER_nondet_in_addr_t();
+
 in_addr_t inet_network(const char *cp)
 {
   __CPROVER_HIDE:;
@@ -39,6 +45,6 @@ in_addr_t inet_network(const char *cp)
   __CPROVER_assert(__CPROVER_is_zero_string(cp), "inet_network zero-termination of name argument");
   #endif
 
-  in_addr_t result;
+  in_addr_t result=__VERIFIER_nondet_in_addr_t();
   return result;
 }