Skip to content

C library: cleanup and syntax error fixes #1243

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Sep 1, 2017
Merged

C library: cleanup and syntax error fixes #1243

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
10a0c01
Pointers returned by getenv must not be manipulated
tautschnig Aug 15, 2017
6d68345
ansi-c library: explicit non-det initialisation, cleanup, syntax fixes
tautschnig Aug 15, 2017
e49c751
Improve ansi-c library syntax check and run via travis
tautschnig Aug 15, 2017
b142da4
Check for memory leaks in C++ new/delete
tautschnig Jan 5, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions .travis.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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" &&
Expand Down
9 changes: 5 additions & 4 deletions src/ansi-c/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ; \
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

why did this change?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This warning should no longer be silenced as all local variables are now initialised (with non-deterministic values).

ec=$$? ; \
$(RM) __libcheck.s __libcheck.i __libcheck.c ; \
[ $$ec -eq 0 ] || exit $$ec ; \
Expand Down
4 changes: 3 additions & 1 deletion src/ansi-c/library/fcntl.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
27 changes: 19 additions & 8 deletions src/ansi-c/library/getopt.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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];
Expand All @@ -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
Expand Down
12 changes: 9 additions & 3 deletions src/ansi-c/library/inet.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:;
Expand All @@ -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:;
Expand All @@ -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:;
Expand All @@ -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;
}
Loading