replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

C library: model _pipe 

Windows (though not the Windows Runtime) has _pipe to implement pipe.
This commit is contained in:
Michael Tautschnig 2019-01-03 11:52:13 +00:00
parent 3eaed93407
commit 1a60834eff
2 changed files with 15 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
buildspec-windows.yml
View File

@ -48,7 +48,6 @@ phases:
Remove-Item cbmc\byte_update5 -Force -Recurse
Remove-Item cbmc\byte_update6 -Force -Recurse
Remove-Item cbmc\byte_update7 -Force -Recurse
Remove-Item cbmc-library\pipe-01 -Force -Recurse
Remove-Item cpp -Force -Recurse
Remove-Item cbmc-cpp -Force -Recurse
Remove-Item goto-gcc -Force -Recurse

15
src/ansi-c/library/unistd.c
View File

@ -80,6 +80,21 @@ int pipe(int fildes[2])
return 0;
}
/* FUNCTION: _pipe */
#ifdef _WIN32
#undef pipe
int pipe(int fildes[2]);
int _pipe(int *pfds, unsigned int psize, int textmode)
{
__CPROVER_HIDE:;
(void)psize;
(void)textmode;
return pipe(pfds);
}
#endif
/* FUNCTION: close */
extern struct __CPROVER_pipet __CPROVER_pipes[];