diff --git a/regression/cbmc/fgets1/main.c b/regression/cbmc/fgets1/main.c new file mode 100644 index 00000000000..8c4e418885b --- /dev/null +++ b/regression/cbmc/fgets1/main.c @@ -0,0 +1,22 @@ +#include +#include + +int main() +{ + char buffer[3]={'a', 'b', '\0'}; + FILE *f=fdopen(0, "r"); + if(!f) + return 1; + + char *p=fgets(buffer, 3, f); + if(p) + { + assert(buffer[1]==p[1]); + assert(buffer[2]=='\0'); + assert(p[1]=='b'); // expected to fail + } + + fclose(f); + + return 0; +} diff --git a/regression/cbmc/fgets1/test.desc b/regression/cbmc/fgets1/test.desc new file mode 100644 index 00000000000..3a8c4e6a733 --- /dev/null +++ b/regression/cbmc/fgets1/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--bounds-check --pointer-check +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +\[main.assertion.3\] assertion p\[1\]=='b': FAILURE +\*\* 1 of 38 failed \(2 iterations\) +-- +^warning: ignoring diff --git a/src/ansi-c/library/getopt.c b/src/ansi-c/library/getopt.c index d3eedda9814..458f9d2e414 100644 --- a/src/ansi-c/library/getopt.c +++ b/src/ansi-c/library/getopt.c @@ -3,22 +3,67 @@ extern char *optarg; extern int optind; +#ifndef __CPROVER_STRING_H_INCLUDED +#include +#define __CPROVER_STRING_H_INCLUDED +#endif + inline int getopt(int argc, char * const argv[], const char *optstring) { __CPROVER_HIDE:; - int result_index; - __CPROVER_assume(result_index>=0); - (void)*optstring; - if(optind>=argc) + int result=-1; + + if(optind==0) + optind=1; + + if(optind>=argc || argv[optind][0]!='-') return -1; - __CPROVER_assume(result_index=optind); + + size_t result_index; + __CPROVER_assume( + result_index +#define __CPROVER_STDLIB_H_INCLUDED +#endif + inline int fclose(FILE *stream) { __CPROVER_HIDE:; @@ -135,11 +147,48 @@ inline FILE *fdopen(int handle, const char *mode) "fdopen zero-termination of 2nd argument"); #endif + #if !defined(__linux__) || defined(__GLIBC__) FILE *f=malloc(sizeof(FILE)); + #else + // libraries need to expose the definition of FILE; this is the + // case for musl + FILE *f=malloc(sizeof(int)); + #endif return f; } +/* FUNCTION: _fdopen */ + +// This is for Apple + +#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__ +inline FILE *_fdopen(int handle, const char *mode) +{ + __CPROVER_HIDE:; + (void)handle; + (void)*mode; + #ifdef __CPROVER_STRING_ABSTRACTION + __CPROVER_assert(__CPROVER_is_zero_string(mode), + "fdopen zero-termination of 2nd argument"); + #endif + + FILE *f=malloc(sizeof(FILE)); + + return f; +} +#endif + /* FUNCTION: fgets */ #ifndef __CPROVER_STDIO_H_INCLUDED @@ -147,7 +196,7 @@ inline FILE *fdopen(int handle, const char *mode) #define __CPROVER_STDIO_H_INCLUDED #endif -inline char *fgets(char *str, int size, FILE *stream) +char *fgets(char *str, int size, FILE *stream) { __CPROVER_HIDE:; __CPROVER_bool error; @@ -169,6 +218,16 @@ inline char *fgets(char *str, int size, FILE *stream) __CPROVER_is_zero_string(str)=!error; __CPROVER_zero_string_length(str)=resulting_size; } + #else + if(size>0) + { + int str_length; + __CPROVER_assume(str_length>=0 && str_length +#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 + +inline int vasprintf(char **ptr, const char *fmt, va_list ap) +{ + (void)*fmt; + (void)ap; + + int result_buffer_size; + if(result_buffer_size<=0) + return -1; + + *ptr=malloc(result_buffer_size); + for(int i=0; i