[00:00:00] Build started [00:00:00] git clone -q --depth=50 --branch=master https://github.com/forejtv/cbmc.git C:\projects\cbmc [00:00:10] git checkout -qf aa99900bd4c889f6fcd8c0a757935a5e132195ae [00:00:11] appveyor DownloadFile http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz [00:00:13] [00:00:13] Downloading minisat2_2.2.1.orig.tar.gz (44,229 bytes)...31% [00:00:13] Downloading minisat2_2.2.1.orig.tar.gz (44,229 bytes)...100% [00:00:13] 7z x minisat2_2.2.1.orig.tar.gz [00:00:13] [00:00:13] 7-Zip [64] 16.04 : Copyright (c) 1999-2016 Igor Pavlov : 2016-10-04 [00:00:13] [00:00:13] Scanning the drive for archives: [00:00:13] 1 file, 44229 bytes (44 KiB) [00:00:13] [00:00:13] Extracting archive: minisat2_2.2.1.orig.tar.gz [00:00:13] -- [00:00:13] Path = minisat2_2.2.1.orig.tar.gz [00:00:13] Type = gzip [00:00:13] Headers Size = 10 [00:00:13] [00:00:13] Everything is Ok [00:00:13] [00:00:13] Size: 225280 [00:00:13] Compressed: 44229 [00:00:13] 7z x minisat2_2.2.1.orig.tar [00:00:13] [00:00:13] 7-Zip [64] 16.04 : Copyright (c) 1999-2016 Igor Pavlov : 2016-10-04 [00:00:13] [00:00:13] Scanning the drive for archives: [00:00:13] 1 file, 225280 bytes (220 KiB) [00:00:13] [00:00:13] Extracting archive: minisat2_2.2.1.orig.tar [00:00:13] -- [00:00:13] Path = minisat2_2.2.1.orig.tar [00:00:13] Type = tar [00:00:13] Physical Size = 225280 [00:00:13] Headers Size = 19968 [00:00:13] Code Page = UTF-8 [00:00:13] [00:00:13] Everything is Ok [00:00:13] [00:00:13] Folders: 7 [00:00:13] Files: 28 [00:00:13] Size: 197425 [00:00:13] Compressed: 225280 [00:00:13] mv minisat2-2.2.1 minisat-2.2.1 [00:00:13] cd minisat-2.2.1 [00:00:13] patch -p1 < ../scripts/minisat-2.2.1-patch [00:00:13] patching file minisat/core/Solver.cc [00:00:13] patching file minisat/core/SolverTypes.h [00:00:13] patching file minisat/mtl/IntTypes.h [00:00:13] patching file minisat/mtl/Vec.h [00:00:13] patching file minisat/simp/SimpSolver.cc [00:00:13] patching file minisat/utils/Options.h [00:00:13] patching file minisat/utils/ParseUtils.h [00:00:13] cd .. [00:00:13] appveyor DownloadFile https://sourceforge.mirrorservice.org/g/gn/gnuwin32/make/3.81/make-3.81-bin.zip [00:00:15] [00:00:15] Downloading make-3.81-bin.zip (495,645 bytes)...4% [00:00:15] Downloading make-3.81-bin.zip (495,645 bytes)...10% [00:00:15] Downloading make-3.81-bin.zip (495,645 bytes)...20% [00:00:15] Downloading make-3.81-bin.zip (495,645 bytes)...30% [00:00:15] Downloading make-3.81-bin.zip (495,645 bytes)...40% [00:00:15] Downloading make-3.81-bin.zip (495,645 bytes)...50% [00:00:15] Downloading make-3.81-bin.zip (495,645 bytes)...60% [00:00:15] Downloading make-3.81-bin.zip (495,645 bytes)...70% [00:00:15] Downloading make-3.81-bin.zip (495,645 bytes)...80% [00:00:15] Downloading make-3.81-bin.zip (495,645 bytes)...90% [00:00:15] Downloading make-3.81-bin.zip (495,645 bytes)...100% [00:00:15] 7z x make-3.81-bin.zip [00:00:15] [00:00:15] 7-Zip [64] 16.04 : Copyright (c) 1999-2016 Igor Pavlov : 2016-10-04 [00:00:15] [00:00:15] Scanning the drive for archives: [00:00:15] 1 file, 495645 bytes (485 KiB) [00:00:15] [00:00:15] Extracting archive: make-3.81-bin.zip [00:00:15] -- [00:00:15] Path = make-3.81-bin.zip [00:00:15] Type = zip [00:00:15] Physical Size = 495645 [00:00:15] Comment = Make-3.81: Binaries [00:00:15] [00:00:15] Everything is Ok [00:00:15] [00:00:15] Folders: 59 [00:00:15] Files: 44 [00:00:15] Size: 1205834 [00:00:15] Compressed: 495645 [00:00:15] appveyor DownloadFile https://sourceforge.mirrorservice.org/g/gn/gnuwin32/bison/2.4.1/bison-2.4.1-bin.zip [00:00:16] [00:00:17] Downloading bison-2.4.1-bin.zip (963,729 bytes)...2% [00:00:17] Downloading bison-2.4.1-bin.zip (963,729 bytes)...40% [00:00:17] Downloading bison-2.4.1-bin.zip (963,729 bytes)...50% [00:00:17] Downloading bison-2.4.1-bin.zip (963,729 bytes)...60% [00:00:17] Downloading bison-2.4.1-bin.zip (963,729 bytes)...70% [00:00:17] Downloading bison-2.4.1-bin.zip (963,729 bytes)...80% [00:00:17] Downloading bison-2.4.1-bin.zip (963,729 bytes)...100% [00:00:17] 7z x bison-2.4.1-bin.zip [00:00:17] [00:00:17] 7-Zip [64] 16.04 : Copyright (c) 1999-2016 Igor Pavlov : 2016-10-04 [00:00:17] [00:00:17] Scanning the drive for archives: [00:00:17] 1 file, 963729 bytes (942 KiB) [00:00:17] [00:00:17] Extracting archive: bison-2.4.1-bin.zip [00:00:17] -- [00:00:17] Path = bison-2.4.1-bin.zip [00:00:17] Type = zip [00:00:17] Physical Size = 963729 [00:00:17] Comment = Bison-2.4.1 (Yacc-compatible parser generator): Binaries [00:00:17] [00:00:17] Everything is Ok [00:00:17] [00:00:17] Folders: 74 [00:00:17] Files: 98 [00:00:17] Size: 2802334 [00:00:17] Compressed: 963729 [00:00:17] appveyor DownloadFile https://sourceforge.mirrorservice.org/g/gn/gnuwin32/flex/2.5.4a-1/flex-2.5.4a-1-bin.zip [00:00:18] [00:00:18] Downloading flex-2.5.4a-1-bin.zip (202,802 bytes)...9% [00:00:18] Downloading flex-2.5.4a-1-bin.zip (202,802 bytes)...100% [00:00:18] 7z x flex-2.5.4a-1-bin.zip [00:00:18] [00:00:18] 7-Zip [64] 16.04 : Copyright (c) 1999-2016 Igor Pavlov : 2016-10-04 [00:00:18] [00:00:18] Scanning the drive for archives: [00:00:18] 1 file, 202802 bytes (199 KiB) [00:00:18] [00:00:18] Extracting archive: flex-2.5.4a-1-bin.zip [00:00:18] -- [00:00:18] Path = flex-2.5.4a-1-bin.zip [00:00:18] Type = zip [00:00:18] Physical Size = 202802 [00:00:18] Comment = Flex 2.5.4a: Binaries [00:00:18] Flex: fast lexical analyzer generator [00:00:18] [00:00:18] Everything is Ok [00:00:18] [00:00:18] Files: 15 [00:00:18] Size: 536514 [00:00:18] Compressed: 202802 [00:00:18] appveyor DownloadFile https://sourceforge.mirrorservice.org/g/gn/gnuwin32/flex/2.5.4a-1/flex-2.5.4a-1-lib.zip [00:00:19] [00:00:19] Downloading flex-2.5.4a-1-lib.zip (3,792 bytes)...100% [00:00:19] 7z x flex-2.5.4a-1-lib.zip [00:00:19] [00:00:19] 7-Zip [64] 16.04 : Copyright (c) 1999-2016 Igor Pavlov : 2016-10-04 [00:00:19] [00:00:19] Scanning the drive for archives: [00:00:19] 1 file, 3792 bytes (4 KiB) [00:00:19] [00:00:19] Extracting archive: flex-2.5.4a-1-lib.zip [00:00:19] -- [00:00:19] Path = flex-2.5.4a-1-lib.zip [00:00:19] Type = zip [00:00:19] Physical Size = 3792 [00:00:19] Comment = Flex 2.5.4a: Developer files [00:00:19] Flex: fast lexical analyzer generator [00:00:19] [00:00:19] Everything is Ok [00:00:19] [00:00:19] Files: 5 [00:00:19] Size: 7196 [00:00:19] Compressed: 3792 [00:00:19] appveyor DownloadFile https://sourceforge.mirrorservice.org/g/gn/gnuwin32/libintl/0.14.4/libintl-0.14.4-bin.zip [00:00:20] [00:00:20] Downloading libintl-0.14.4-bin.zip (394,081 bytes)...5% [00:00:20] Downloading libintl-0.14.4-bin.zip (394,081 bytes)...30% [00:00:20] Downloading libintl-0.14.4-bin.zip (394,081 bytes)...50% [00:00:20] Downloading libintl-0.14.4-bin.zip (394,081 bytes)...100% [00:00:20] 7z x libintl-0.14.4-bin.zip [00:00:20] [00:00:20] 7-Zip [64] 16.04 : Copyright (c) 1999-2016 Igor Pavlov : 2016-10-04 [00:00:20] [00:00:20] Scanning the drive for archives: [00:00:20] 1 file, 394081 bytes (385 KiB) [00:00:20] [00:00:20] Extracting archive: libintl-0.14.4-bin.zip [00:00:20] -- [00:00:20] Path = libintl-0.14.4-bin.zip [00:00:20] Type = zip [00:00:20] Physical Size = 394081 [00:00:20] Comment = LibIntl-0.14.4: Binaries [00:00:20] LibIntl: library for native language support [00:00:20] [00:00:20] Everything is Ok [00:00:20] [00:00:20] Folders: 82 [00:00:20] Files: 93 [00:00:20] Size: 1070482 [00:00:20] Compressed: 394081 [00:00:20] appveyor DownloadFile https://sourceforge.mirrorservice.org/g/gn/gnuwin32/libiconv/1.9.2-1/libiconv-1.9.2-1-bin.zip [00:00:21] [00:00:21] Downloading libiconv-1.9.2-1-bin.zip (828,380 bytes)...2% [00:00:21] Downloading libiconv-1.9.2-1-bin.zip (828,380 bytes)...10% [00:00:21] Downloading libiconv-1.9.2-1-bin.zip (828,380 bytes)...20% [00:00:21] Downloading libiconv-1.9.2-1-bin.zip (828,380 bytes)...30% [00:00:22] Downloading libiconv-1.9.2-1-bin.zip (828,380 bytes)...40% [00:00:22] Downloading libiconv-1.9.2-1-bin.zip (828,380 bytes)...50% [00:00:22] Downloading libiconv-1.9.2-1-bin.zip (828,380 bytes)...60% [00:00:22] Downloading libiconv-1.9.2-1-bin.zip (828,380 bytes)...70% [00:00:22] Downloading libiconv-1.9.2-1-bin.zip (828,380 bytes)...80% [00:00:22] Downloading libiconv-1.9.2-1-bin.zip (828,380 bytes)...90% [00:00:22] Downloading libiconv-1.9.2-1-bin.zip (828,380 bytes)...100% [00:00:22] 7z x libiconv-1.9.2-1-bin.zip [00:00:22] [00:00:22] 7-Zip [64] 16.04 : Copyright (c) 1999-2016 Igor Pavlov : 2016-10-04 [00:00:22] [00:00:22] Scanning the drive for archives: [00:00:22] 1 file, 828380 bytes (809 KiB) [00:00:22] [00:00:22] Extracting archive: libiconv-1.9.2-1-bin.zip [00:00:22] -- [00:00:22] Path = libiconv-1.9.2-1-bin.zip [00:00:22] Type = zip [00:00:22] Physical Size = 828380 [00:00:22] Comment = LibIconv 1.9.2: Binaries [00:00:22] LibIconv: convert between character encodings [00:00:22] [00:00:22] Everything is Ok [00:00:22] [00:00:22] Files: 61 [00:00:22] Size: 1277277 [00:00:22] Compressed: 828380 [00:00:22] appveyor DownloadFile https://sourceforge.mirrorservice.org/g/gn/gnuwin32/regex/2.7/regex-2.7-bin.zip [00:00:23] [00:00:23] Downloading regex-2.7-bin.zip (73,283 bytes)...23% [00:00:23] Downloading regex-2.7-bin.zip (73,283 bytes)...90% [00:00:23] Downloading regex-2.7-bin.zip (73,283 bytes)...100% [00:00:23] 7z x regex-2.7-bin.zip [00:00:23] [00:00:23] 7-Zip [64] 16.04 : Copyright (c) 1999-2016 Igor Pavlov : 2016-10-04 [00:00:23] [00:00:23] Scanning the drive for archives: [00:00:23] 1 file, 73283 bytes (72 KiB) [00:00:23] [00:00:23] Extracting archive: regex-2.7-bin.zip [00:00:23] -- [00:00:23] Path = regex-2.7-bin.zip [00:00:23] Type = zip [00:00:23] Physical Size = 73283 [00:00:23] Comment = Regex-2.7 (searches for and matches text strings): Binaries [00:00:23] [00:00:23] Everything is Ok [00:00:23] [00:00:23] Folders: 8 [00:00:23] Files: 24 [00:00:23] Size: 147994 [00:00:23] Compressed: 73283 [00:00:23] ls C:\projects\cbmc\bin [00:00:23] bison.exe [00:00:23] flex++.exe [00:00:23] flex.exe [00:00:23] iconv.exe [00:00:23] libcharset1.dll [00:00:23] libiconv2.dll [00:00:23] libintl3.dll [00:00:23] m4.exe [00:00:23] make.exe [00:00:23] regex2.dll [00:00:23] yacc [00:00:23] ls C:\projects\cbmc\include [00:00:23] FlexLexer.h [00:00:23] regex.h [00:00:23] unistd.h [00:00:23] set [00:00:23] 7zip="C:\Program Files\7-Zip\7z.exe" [00:00:23] ALLUSERSPROFILE=C:\ProgramData [00:00:23] APPDATA=C:\Users\appveyor\AppData\Roaming [00:00:23] APPVEYOR=True [00:00:23] APPVEYOR_ACCOUNT_NAME=forejtv [00:00:23] APPVEYOR_API_URL=http://localhost:1031/ [00:00:23] APPVEYOR_BUILD_FOLDER=C:\projects\cbmc [00:00:23] APPVEYOR_BUILD_ID=6959768 [00:00:23] APPVEYOR_BUILD_NUMBER=35 [00:00:23] APPVEYOR_BUILD_VERSION=1.0.35 [00:00:23] APPVEYOR_JOB_ID=1u3g852s46s95un5 [00:00:23] APPVEYOR_PROJECT_ID=285314 [00:00:23] APPVEYOR_PROJECT_NAME=cbmc [00:00:23] APPVEYOR_PROJECT_SLUG=cbmc [00:00:23] APPVEYOR_REPO_BRANCH=master [00:00:23] APPVEYOR_REPO_COMMIT=aa99900bd4c889f6fcd8c0a757935a5e132195ae [00:00:23] APPVEYOR_REPO_COMMIT_AUTHOR=Peter Schrammel [00:00:23] APPVEYOR_REPO_COMMIT_AUTHOR_EMAIL=peterschrammel@users.noreply.github.com [00:00:23] APPVEYOR_REPO_COMMIT_MESSAGE=Merge pull request #470 from smowton/fix_address_space_size_check [00:00:23] APPVEYOR_REPO_COMMIT_MESSAGE_EXTENDED=Fix address space size check [00:00:23] APPVEYOR_REPO_COMMIT_TIMESTAMP=2017-01-25T17:40:08.0000000Z [00:00:23] APPVEYOR_REPO_NAME=forejtv/cbmc [00:00:23] APPVEYOR_REPO_PROVIDER=gitHub [00:00:23] APPVEYOR_REPO_SCM=git [00:00:23] APPVEYOR_REPO_TAG=false [00:00:23] APPVEYOR_RE_BUILD=True [00:00:23] APPVEYOR_URL=https://ci.appveyor.com [00:00:23] APR_ICONV_PATH=C:\Program Files (x86)\Subversion\iconv [00:00:23] AVVM_DOWNLOAD_URL=http://av1southus4workers.blob.core.windows.net/downloads/avvm [00:00:23] BUILD_ENV=MSVC [00:00:23] ChocolateyInstall=C:\ProgramData\chocolatey [00:00:23] ChocolateyLastPathUpdate=Wed Dec 28 22:23:13 2016 [00:00:23] CI=True [00:00:23] CodeContractsInstallDir=C:\Program Files (x86)\Microsoft\Contracts\ [00:00:23] CommonProgramFiles=C:\Program Files\Common Files [00:00:23] CommonProgramFiles(x86)=C:\Program Files (x86)\Common Files [00:00:23] CommonProgramW6432=C:\Program Files\Common Files [00:00:23] COMPUTERNAME=APPVYR-WIN [00:00:23] ComSpec=C:\windows\system32\cmd.exe [00:00:23] DXSDK_DIR=C:\Program Files (x86)\Microsoft DirectX SDK (June 2010)\ [00:00:23] EnableNuGetPackageRestore=true [00:00:23] ERLANG_HOME=C:\Program Files\erl7.3 [00:00:23] FP_NO_HOST_CHECK=NO [00:00:23] GIT_LFS_PATH=C:\Program Files\Git LFS [00:00:23] GOROOT=C:\go [00:00:23] HOMEDRIVE=C: [00:00:23] HOMEPATH=\Users\appveyor [00:00:23] INCLUDE=C:\projects\cbmc\include [00:00:23] JAVA_HOME=C:\Progra~1\Java\jdk1.8.0 [00:00:23] lastexitcode=0 [00:00:23] LOCALAPPDATA=C:\Users\appveyor\AppData\Local [00:00:23] LOGONSERVER=\\APPVYR-WIN [00:00:23] M2_HOME=C:\Program Files (x86)\Apache\Maven [00:00:23] MAVEN_HOME=C:\Program Files (x86)\Apache\Maven [00:00:23] MSYS2_PATH_TYPE=inherit [00:00:23] NUMBER_OF_PROCESSORS=2 [00:00:23] OPENSSL_CONF=C:\OpenSSL-Win32\bin\openssl.cfg [00:00:23] OS=Windows_NT [00:00:23] Path=C:\projects\cbmc\bin;C:\Perl\site\bin;C:\Perl\bin;C:\Windows\system32;C:\Windows;C:\Windows\System32\Wbem;C:\Windows\System32\WindowsPowerShell\v1.0\;C:\Program Files\7-Zip;C:\Program Files\Microsoft\Web Platform Installer\;C:\Tools\GitVersion;C:\Tools\PsTools;C:\Program Files\Git LFS;C:\Program Files (x86)\Subversion\bin;C:\Program Files\Microsoft SQL Server\120\Tools\Binn\;C:\Program Files\Microsoft SQL Server\Client SDK\ODBC\110\Tools\Binn\;C:\Program Files (x86)\Microsoft SQL Server\120\Tools\Binn\;C:\Program Files\Microsoft SQL Server\120\DTS\Binn\;C:\Program Files (x86)\Microsoft SQL Server\120\Tools\Binn\ManagementStudio\;C:\Program Files\Microsoft Windows Performance Toolkit\;C:\Program Files (x86)\Windows Kits\8.1\Windows Performance Toolkit\;C:\Tools\WebDriver;C:\Program Files (x86)\Microsoft SDKs\TypeScript\1.4\;C:\Program Files (x86)\Microsoft Visual Studio 12.0\Common7\IDE\PrivateAssemblies\;C:\Program Files (x86)\Microsoft SDKs\Azure\CLI\wbin;C:\Ruby193\bin;C:\Tools\NUnit\bin;C:\Tools\xUnit;C:\Tools\MSpec;C:\Tools\Coverity\bin;C:\Program Files (x86)\CMake\bin;C:\go\bin;C:\Program Files\Java\jdk1.8.0\bin;C:\Python27;C:\Program Files\erl7.3\bin;C:\Program Files\nodejs;C:\Program Files (x86)\iojs;C:\Program Files\iojs;C:\Users\appveyor\AppData\Roaming\npm;C:\Program Files\Microsoft SQL Server\130\Tools\Binn\;C:\Program Files (x86)\Windows Kits\10\Windows Performance Toolkit\;C:\Program Files (x86)\MSBuild\14.0\Bin;C:\Program Files (x86)\Microsoft Visual Studio 14.0\Common7\IDE\Extensions\Microsoft\SQLDB\DAC\120;C:\Tools\NuGet;C:\Program Files (x86)\Microsoft Visual Studio 14.0\Common7\IDE\CommonExtensions\Microsoft\TestWindow;C:\Program Files\Amazon\AWSCLI\;C:\Windows\SysWOW64\WindowsPowerShell\v1.0\Modules\TShell\TShell\;C:\Program Files\Microsoft DNX\Dnvm;C:\Program Files\Microsoft SQL Server\Client SDK\ODBC\130\Tools\Binn\;C:\Program Files (x86)\Microsoft SQL Server\130\Tools\Binn\;C:\Program Files (x86)\Microsoft SQL Server\130\DTS\Binn\;C:\Program Files\Microsoft SQL Server\130\DTS\Binn\;C:\Program Files (x86)\Microsoft SQL Server\110\DTS\Binn\;C:\Program Files (x86)\Microsoft SQL Server\120\DTS\Binn\;C:\Program Files (x86)\Apache\Maven\bin;C:\Program Files\LLVM\bin;C:\Program Files\Microsoft Service Fabric\bin\Fabric\Fabric.Code;C:\Program Files\Microsoft SDKs\Service Fabric\Tools\ServiceFabricLocalClusterManager;C:\Python27\Scripts;C:\Tools\NUnit3;C:\Program Files\dotnet\;C:\Program Files\Git\cmd;C:\Program Files\Git\usr\bin;C:\Program Files\Mercurial\;C:\Program Files (x86)\Yarn\bin;C:\ProgramData\chocolatey\bin;C:\Program Files (x86)\nodejs\;C:\Users\appveyor\.dnx\runtimes\dnx-clr-win-x86.1.0.0-rc1-update2\bin;C:\Users\appveyor\AppData\Local\Yarn\.bin;C:\Users\appveyor\AppData\Roaming\npm;C:\Program Files\AppVeyor\BuildAgent\ [00:00:23] PATHEXT=.COM;.EXE;.BAT;.CMD;.VBS;.VBE;.JS;.JSE;.WSF;.WSH;.MSC;.PY;.CPL [00:00:23] PROCESSOR_ARCHITECTURE=AMD64 [00:00:23] PROCESSOR_IDENTIFIER=Intel64 Family 6 Model 63 Stepping 2, GenuineIntel [00:00:23] PROCESSOR_LEVEL=6 [00:00:23] PROCESSOR_REVISION=3f02 [00:00:23] ProgramData=C:\ProgramData [00:00:23] ProgramFiles=C:\Program Files [00:00:23] ProgramFiles(x86)=C:\Program Files (x86) [00:00:23] ProgramW6432=C:\Program Files [00:00:23] PROMPT=$P$G [00:00:23] PSModulePath=C:\Users\appveyor\Documents\WindowsPowerShell\Modules;C:\Users\appveyor\Documents\WindowsPowerShell\Modules;C:\Program Files\WindowsPowerShell\Modules;C:\Windows\system32\WindowsPowerShell\v1.0\Modules\;C:\Program Files (x86)\Microsoft SQL Server\110\Tools\PowerShell\Modules\;C:\Program Files (x86)\Microsoft SQL Server\120\Tools\PowerShell\Modules\;C:\Program Files\WindowsPowerShell\Modules\;C:\Program Files (x86)\Microsoft SDKs\Azure\PowerShell\ResourceManager\AzureResourceManager\;C:\Program Files (x86)\Microsoft SDKs\Azure\PowerShell\ServiceManagement\;C:\Program Files (x86)\Microsoft SDKs\Azure\PowerShell\Storage\;C:\Program Files (x86)\AWS Tools\PowerShell\;C:\Program Files\AppVeyor\BuildAgent\Modules;C:\Program Files (x86)\Microsoft SQL Server\130\Tools\PowerShell\Modules\ [00:00:23] PUBLIC=C:\Users\Public [00:00:23] SESSIONNAME=Console [00:00:23] SystemDrive=C: [00:00:23] SystemRoot=C:\windows [00:00:23] TEMP=C:\Users\appveyor\AppData\Local\Temp\1 [00:00:23] TMP=C:\Users\appveyor\AppData\Local\Temp\1 [00:00:23] USERDOMAIN=APPVYR-WIN [00:00:23] USERDOMAIN_ROAMINGPROFILE=APPVYR-WIN [00:00:23] USERNAME=appveyor [00:00:23] USERPROFILE=C:\Users\appveyor [00:00:23] VS100COMNTOOLS=c:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\Tools\ [00:00:23] VS110COMNTOOLS=C:\Program Files (x86)\Microsoft Visual Studio 11.0\Common7\Tools\ [00:00:23] VS120COMNTOOLS=C:\Program Files (x86)\Microsoft Visual Studio 12.0\Common7\Tools\ [00:00:23] VS140COMNTOOLS=C:\Program Files (x86)\Microsoft Visual Studio 14.0\Common7\Tools\ [00:00:23] VS90COMNTOOLS=C:\Program Files (x86)\Microsoft Visual Studio 9.0\Common7\Tools\ [00:00:23] VSSDK120Install=C:\Program Files (x86)\Microsoft Visual Studio 12.0\VSSDK\ [00:00:23] VSSDK140Install=C:\Program Files (x86)\Microsoft Visual Studio 14.0\VSSDK\ [00:00:23] windir=C:\windows [00:00:23] WIX=C:\Program Files (x86)\WiX Toolset v3.10\ [00:00:23] xunit20=C:\Tools\xUnit20 [00:00:23] cd src [00:00:23] call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 [00:00:23] cl [00:00:24] Microsoft (R) C/C++ Optimizing Compiler Version 19.00.24215.1 for x64 [00:00:24] Copyright (C) Microsoft Corporation. All rights reserved. [00:00:24] [00:00:24] usage: cl [ option... ] filename... [ /link linkoption... ] [00:00:24] sed -i "s/BUILD_ENV.*/BUILD_ENV = MSVC/" config.inc [00:00:24] sed -i "128s/$/ \/std:c++14/" common [00:00:24] make --version [00:00:24] GNU Make 3.81 [00:00:24] Copyright (C) 2006 Free Software Foundation, Inc. [00:00:24] This is free software; see the source for copying conditions. [00:00:24] There is NO warranty; not even for MERCHANTABILITY or FITNESS FOR A [00:00:24] PARTICULAR PURPOSE. [00:00:24] [00:00:24] This program built for i386-pc-mingw32 [00:00:24] make [00:00:25] ## Entering big-int [00:00:25] make -C big-int [00:00:25] make[1]: Entering directory `C:/projects/cbmc/src/big-int' [00:00:25] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 /nologo /c /EHsc bigint-func.cc /Fobigint-func.obj [00:00:25] bigint-func.cc [00:00:25] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 /nologo /c /EHsc bigint.cc /Fobigint.obj [00:00:25] bigint.cc [00:00:25] bigint.cc(636): warning C4267: 'initializing': conversion from 'size_t' to 'unsigned int', possible loss of data [00:00:25] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 /nologo /c /EHsc bigint-test.cc /Fobigint-test.obj [00:00:25] bigint-test.cc [00:00:25] cl /Fetest-bigint.exe bigint-func.obj bigint.obj bigint-test.obj [00:00:25] Microsoft (R) C/C++ Optimizing Compiler Version 19.00.24215.1 for x64 [00:00:25] Copyright (C) Microsoft Corporation. All rights reserved. [00:00:25] [00:00:25] Microsoft (R) Incremental Linker Version 14.00.24215.1 [00:00:25] Copyright (C) Microsoft Corporation. All rights reserved. [00:00:25] [00:00:25] /out:test-bigint.exe [00:00:25] bigint-func.obj [00:00:25] bigint.obj [00:00:25] bigint-test.obj [00:00:26] lib /NOLOGO /OUT:big-int.lib bigint-func.obj bigint.obj [00:00:26] make[1]: Leaving directory `C:/projects/cbmc/src/big-int' [00:00:26] ## Entering util [00:00:26] make -C util [00:00:26] make[1]: Entering directory `C:/projects/cbmc/src/util' [00:00:26] cl /Feirep_ids_convert.exe irep_ids_convert.cpp [00:00:26] Microsoft (R) C/C++ Optimizing Compiler Version 19.00.24215.1 for x64 [00:00:26] Copyright (C) Microsoft Corporation. All rights reserved. [00:00:26] [00:00:26] irep_ids_convert.cpp [00:00:26] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\xlocale(341): warning C4530: C++ exception handler used, but unwind semantics are not enabled. Specify /EHsc [00:00:26] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\exception(359): warning C4577: 'noexcept' used with no exception handling mode specified; termination on exception is not guaranteed. Specify /EHsc [00:00:26] Microsoft (R) Incremental Linker Version 14.00.24215.1 [00:00:26] Copyright (C) Microsoft Corporation. All rights reserved. [00:00:26] [00:00:26] /out:irep_ids_convert.exe [00:00:26] irep_ids_convert.obj [00:00:27] ./irep_ids_convert.exe header < irep_ids.txt > irep_ids.h [00:00:27] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc arith_tools.cpp /Foarith_tools.obj [00:00:27] arith_tools.cpp [00:00:27] arith_tools.cpp(258): warning C4244: 'argument': conversion from 'BigInt::ullong_t' to 'unsigned int', possible loss of data [00:00:27] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc base_type.cpp /Fobase_type.obj [00:00:27] base_type.cpp [00:00:28] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cmdline.cpp /Focmdline.obj [00:00:28] cmdline.cpp [00:00:29] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc config.cpp /Foconfig.obj [00:00:29] config.cpp [00:00:31] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc symbol_table.cpp /Fosymbol_table.obj [00:00:31] symbol_table.cpp [00:00:32] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc expr.cpp /Foexpr.obj [00:00:32] expr.cpp [00:00:33] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc expr_util.cpp /Foexpr_util.obj [00:00:33] expr_util.cpp [00:00:33] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc irep.cpp /Foirep.obj [00:00:33] irep.cpp [00:00:34] c:\projects\cbmc\src\util\irep_hash.h(94): warning C4267: 'argument': conversion from 'size_t' to 'unsigned int', possible loss of data [00:00:34] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc language.cpp /Folanguage.obj [00:00:34] language.cpp [00:00:35] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc lispexpr.cpp /Folispexpr.obj [00:00:35] lispexpr.cpp [00:00:36] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc lispirep.cpp /Folispirep.obj [00:00:36] lispirep.cpp [00:00:37] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc source_location.cpp /Fosource_location.obj [00:00:37] source_location.cpp [00:00:37] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc message.cpp /Fomessage.obj [00:00:37] message.cpp [00:00:38] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc language_file.cpp /Folanguage_file.obj [00:00:38] language_file.cpp [00:00:39] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc mp_arith.cpp /Fomp_arith.obj [00:00:39] mp_arith.cpp [00:00:39] mp_arith.cpp(135): warning C4267: 'argument': conversion from 'size_t' to 'unsigned int', possible loss of data [00:00:40] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc namespace.cpp /Fonamespace.obj [00:00:40] namespace.cpp [00:00:41] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc parse_options.cpp /Foparse_options.obj [00:00:41] parse_options.cpp [00:00:41] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc rename.cpp /Forename.obj [00:00:41] rename.cpp [00:00:42] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc replace_expr.cpp /Foreplace_expr.obj [00:00:42] replace_expr.cpp [00:00:42] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc threeval.cpp /Fothreeval.obj [00:00:42] threeval.cpp [00:00:43] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc typecheck.cpp /Fotypecheck.obj [00:00:43] typecheck.cpp [00:00:43] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc graph.cpp /Fograph.obj [00:00:43] graph.cpp [00:00:44] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc type.cpp /Fotype.obj [00:00:44] type.cpp [00:00:44] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc pointer_predicates.cpp /Fopointer_predicates.obj [00:00:44] pointer_predicates.cpp [00:00:45] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc merge_irep.cpp /Fomerge_irep.obj [00:00:45] merge_irep.cpp [00:00:45] c:\projects\cbmc\src\util\irep_hash.h(94): warning C4267: 'argument': conversion from 'size_t' to 'unsigned int', possible loss of data [00:00:46] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc run.cpp /Forun.obj [00:00:46] run.cpp [00:00:46] run.cpp(98): warning C4244: 'initializing': conversion from 'intptr_t' to 'int', possible loss of data [00:00:47] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc parser.cpp /Foparser.obj [00:00:47] parser.cpp [00:00:47] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc replace_symbol.cpp /Foreplace_symbol.obj [00:00:47] replace_symbol.cpp [00:00:48] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc json.cpp /Fojson.obj [00:00:48] json.cpp [00:00:49] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc get_base_name.cpp /Foget_base_name.obj [00:00:49] get_base_name.cpp [00:00:49] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc simplify_expr.cpp /Fosimplify_expr.obj [00:00:49] simplify_expr.cpp [00:00:52] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc simplify_expr_floatbv.cpp /Fosimplify_expr_floatbv.obj [00:00:52] simplify_expr_floatbv.cpp [00:00:52] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc simplify_expr_int.cpp /Fosimplify_expr_int.obj [00:00:52] simplify_expr_int.cpp [00:00:54] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc simplify_expr_array.cpp /Fosimplify_expr_array.obj [00:00:54] simplify_expr_array.cpp [00:00:55] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc simplify_expr_struct.cpp /Fosimplify_expr_struct.obj [00:00:55] simplify_expr_struct.cpp [00:00:56] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc simplify_expr_boolean.cpp /Fosimplify_expr_boolean.obj [00:00:56] simplify_expr_boolean.cpp [00:00:57] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc simplify_expr_pointer.cpp /Fosimplify_expr_pointer.obj [00:00:57] simplify_expr_pointer.cpp [00:00:58] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc get_module.cpp /Foget_module.obj [00:00:58] get_module.cpp [00:00:59] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc string_hash.cpp /Fostring_hash.obj [00:00:59] string_hash.cpp [00:00:59] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc string_container.cpp /Fostring_container.obj [00:00:59] string_container.cpp [00:01:00] string_container.cpp(116): warning C4267: '=': conversion from 'size_t' to 'unsigned int', possible loss of data [00:01:00] string_container.cpp(121): warning C4267: 'return': conversion from 'size_t' to 'unsigned int', possible loss of data [00:01:00] string_container.cpp(151): warning C4267: '=': conversion from 'size_t' to 'unsigned int', possible loss of data [00:01:00] string_container.cpp(156): warning C4267: 'return': conversion from 'size_t' to 'unsigned int', possible loss of data [00:01:00] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc identifier.cpp /Foidentifier.obj [00:01:00] identifier.cpp [00:01:01] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc rational.cpp /Forational.obj [00:01:01] rational.cpp [00:01:01] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc options.cpp /Fooptions.obj [00:01:01] options.cpp [00:01:02] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc dstring.cpp /Fodstring.obj [00:01:02] dstring.cpp [00:01:02] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc find_symbols.cpp /Fofind_symbols.obj [00:01:02] find_symbols.cpp [00:01:03] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc rational_tools.cpp /Forational_tools.obj [00:01:03] rational_tools.cpp [00:01:04] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc ui_message.cpp /Foui_message.obj [00:01:04] ui_message.cpp [00:01:05] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc simplify_utils.cpp /Fosimplify_utils.obj [00:01:05] simplify_utils.cpp [00:01:06] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc time_stopping.cpp /Fotime_stopping.obj [00:01:06] time_stopping.cpp [00:01:07] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc symbol.cpp /Fosymbol.obj [00:01:07] symbol.cpp [00:01:08] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc irep_hash_container.cpp /Foirep_hash_container.obj [00:01:08] irep_hash_container.cpp [00:01:08] irep_hash_container.cpp(66): warning C4267: 'argument': conversion from 'size_t' to 'unsigned int', possible loss of data [00:01:08] irep_hash_container.cpp(68): warning C4267: 'argument': conversion from 'size_t' to 'unsigned int', possible loss of data [00:01:08] irep_hash_container.cpp(72): warning C4267: 'argument': conversion from 'size_t' to 'unsigned int', possible loss of data [00:01:08] irep_hash_container.cpp(75): warning C4267: 'argument': conversion from 'size_t' to 'unsigned int', possible loss of data [00:01:08] irep_hash_container.cpp(81): warning C4267: 'argument': conversion from 'size_t' to 'unsigned int', possible loss of data [00:01:08] irep_hash_container.cpp(84): warning C4267: 'argument': conversion from 'size_t' to 'unsigned int', possible loss of data [00:01:09] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cout_message.cpp /Focout_message.obj [00:01:09] cout_message.cpp [00:01:10] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc type_eq.cpp /Fotype_eq.obj [00:01:10] type_eq.cpp [00:01:10] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc guard.cpp /Foguard.obj [00:01:11] guard.cpp [00:01:11] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc array_name.cpp /Foarray_name.obj [00:01:11] array_name.cpp [00:01:12] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc message_stream.cpp /Fomessage_stream.obj [00:01:12] message_stream.cpp [00:01:13] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc substitute.cpp /Fosubstitute.obj [00:01:13] substitute.cpp [00:01:13] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc decision_procedure.cpp /Fodecision_procedure.obj [00:01:13] decision_procedure.cpp [00:01:13] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc union_find.cpp /Founion_find.obj [00:01:13] union_find.cpp [00:01:14] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc xml.cpp /Foxml.obj [00:01:14] xml.cpp [00:01:15] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc xml_irep.cpp /Foxml_irep.obj [00:01:15] xml_irep.cpp [00:01:15] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc xml_expr.cpp /Foxml_expr.obj [00:01:15] xml_expr.cpp [00:01:17] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc std_types.cpp /Fostd_types.obj [00:01:17] std_types.cpp [00:01:18] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc std_code.cpp /Fostd_code.obj [00:01:18] std_code.cpp [00:01:18] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc format_constant.cpp /Foformat_constant.obj [00:01:18] format_constant.cpp [00:01:19] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc find_macros.cpp /Fofind_macros.obj [00:01:19] find_macros.cpp [00:01:20] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc ref_expr_set.cpp /Foref_expr_set.obj [00:01:20] ref_expr_set.cpp [00:01:20] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc std_expr.cpp /Fostd_expr.obj [00:01:20] std_expr.cpp [00:01:21] std_expr.cpp(221): warning C4267: 'argument': conversion from 'size_t' to 'unsigned int', possible loss of data [00:01:21] std_expr.cpp(241): warning C4267: 'argument': conversion from 'size_t' to 'unsigned int', possible loss of data [00:01:21] std_expr.cpp(267): warning C4267: 'argument': conversion from 'size_t' to 'unsigned int', possible loss of data [00:01:21] std_expr.cpp(268): warning C4267: 'argument': conversion from 'size_t' to 'unsigned int', possible loss of data [00:01:21] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc irep_serialization.cpp /Foirep_serialization.obj [00:01:21] irep_serialization.cpp [00:01:21] irep_serialization.cpp(155): warning C4267: 'argument': conversion from 'size_t' to 'const unsigned int', possible loss of data [00:01:21] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\utility(200): warning C4267: 'initializing': conversion from 'size_t' to 'const unsigned int', possible loss of data [00:01:21] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\xmemory0(737): note: see reference to function template instantiation 'std::pair::pair(std::pair &&) noexcept' being compiled [00:01:21] with [00:01:21] [ [00:01:21] _Kty=unsigned int, [00:01:21] _Ty=std::size_t [00:01:21] ] [00:01:21] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\xmemory0(737): note: see reference to function template instantiation 'std::pair::pair(std::pair &&) noexcept' being compiled [00:01:21] with [00:01:21] [ [00:01:21] _Kty=unsigned int, [00:01:21] _Ty=std::size_t [00:01:21] ] [00:01:21] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\xmemory0(857): note: see reference to function template instantiation 'void std::allocator<_Other>::construct<_Objty,_Ty>(_Objty *,_Ty &&)' being compiled [00:01:21] with [00:01:21] [ [00:01:21] _Other=std::_Tree_node,void *>, [00:01:21] _Objty=std::pair, [00:01:21] _Ty=std::pair [00:01:21] ] [00:01:21] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\xmemory0(857): note: see reference to function template instantiation 'void std::allocator<_Other>::construct<_Objty,_Ty>(_Objty *,_Ty &&)' being compiled [00:01:21] with [00:01:21] [ [00:01:21] _Other=std::_Tree_node,void *>, [00:01:21] _Objty=std::pair, [00:01:21] _Ty=std::pair [00:01:21] ] [00:01:21] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\xmemory0(996): note: see reference to function template instantiation 'void std::allocator_traits<_Alloc>::construct<_Ty,std::pair>(std::allocator<_Other> &,_Objty *,std::pair &&)' being compiled [00:01:21] with [00:01:21] [ [00:01:21] _Alloc=std::allocator,void *>>, [00:01:21] _Ty=std::pair, [00:01:21] _Other=std::_Tree_node,void *>, [00:01:21] _Objty=std::pair [00:01:21] ] [00:01:21] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\xmemory0(995): note: see reference to function template instantiation 'void std::allocator_traits<_Alloc>::construct<_Ty,std::pair>(std::allocator<_Other> &,_Objty *,std::pair &&)' being compiled [00:01:21] with [00:01:21] [ [00:01:21] _Alloc=std::allocator,void *>>, [00:01:21] _Ty=std::pair, [00:01:21] _Other=std::_Tree_node,void *>, [00:01:21] _Objty=std::pair [00:01:21] ] [00:01:21] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\xtree(889): note: see reference to function template instantiation 'void std::_Wrap_alloc>::construct<_Ty,std::pair>(_Ty *,std::pair &&)' being compiled [00:01:21] with [00:01:21] [ [00:01:21] _Other=std::_Tree_node,void *>, [00:01:21] _Ty=std::pair [00:01:21] ] [00:01:21] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\xtree(887): note: see reference to function template instantiation 'void std::_Wrap_alloc>::construct<_Ty,std::pair>(_Ty *,std::pair &&)' being compiled [00:01:21] with [00:01:21] [ [00:01:21] _Other=std::_Tree_node,void *>, [00:01:21] _Ty=std::pair [00:01:21] ] [00:01:21] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\xtree(1076): note: see reference to function template instantiation 'std::_Tree_node,void *> *std::_Tree_comp_alloc<_Traits>::_Buynode>(std::pair &&)' being compiled [00:01:21] with [00:01:21] [ [00:01:21] _Kty=unsigned int, [00:01:21] _Ty=std::size_t, [00:01:21] _Traits=std::_Tmap_traits,std::allocator>,false> [00:01:21] ] [00:01:21] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\xtree(1076): note: see reference to function template instantiation 'std::_Tree_node,void *> *std::_Tree_comp_alloc<_Traits>::_Buynode>(std::pair &&)' being compiled [00:01:21] with [00:01:21] [ [00:01:21] _Kty=unsigned int, [00:01:21] _Ty=std::size_t, [00:01:21] _Traits=std::_Tmap_traits,std::allocator>,false> [00:01:21] ] [00:01:21] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\map(194): note: see reference to function template instantiation 'std::pair>>>,bool> std::_Tree>::emplace>(std::pair &&)' being compiled [00:01:21] with [00:01:21] [ [00:01:21] _Kty=unsigned int, [00:01:21] _Ty=std::size_t, [00:01:21] _Pr=std::less, [00:01:21] _Alloc=std::allocator> [00:01:21] ] [00:01:21] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\map(194): note: see reference to function template instantiation 'std::pair>>>,bool> std::_Tree>::emplace>(std::pair &&)' being compiled [00:01:21] with [00:01:21] [ [00:01:21] _Kty=unsigned int, [00:01:21] _Ty=std::size_t, [00:01:21] _Pr=std::less, [00:01:21] _Alloc=std::allocator> [00:01:21] ] [00:01:21] irep_serialization.cpp(185): note: see reference to function template instantiation 'std::pair>>>,bool> std::map<_Kty,_Ty,std::less<_Kty>,std::allocator>>::insert,void>(_Valty &&)' being compiled [00:01:21] with [00:01:21] [ [00:01:21] _Kty=unsigned int, [00:01:21] _Ty=std::size_t, [00:01:21] _Valty=std::pair [00:01:21] ] [00:01:21] irep_serialization.cpp(184): note: see reference to function template instantiation 'std::pair>>>,bool> std::map<_Kty,_Ty,std::less<_Kty>,std::allocator>>::insert,void>(_Valty &&)' being compiled [00:01:21] with [00:01:21] [ [00:01:21] _Kty=unsigned int, [00:01:21] _Ty=std::size_t, [00:01:21] _Valty=std::pair [00:01:21] ] [00:01:22] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc fixedbv.cpp /Fofixedbv.obj [00:01:22] fixedbv.cpp [00:01:23] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc rename_symbol.cpp /Forename_symbol.obj [00:01:23] rename_symbol.cpp [00:01:24] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc ieee_float.cpp /Foieee_float.obj [00:01:24] ieee_float.cpp [00:01:25] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc signal_catcher.cpp /Fosignal_catcher.obj [00:01:25] signal_catcher.cpp [00:01:25] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc pointer_offset_size.cpp /Fopointer_offset_size.obj [00:01:25] pointer_offset_size.cpp [00:01:26] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc bv_arithmetic.cpp /Fobv_arithmetic.obj [00:01:26] bv_arithmetic.cpp [00:01:27] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc tempdir.cpp /Fotempdir.obj [00:01:27] tempdir.cpp [00:01:27] tempdir.cpp(63): warning C4996: 'unlink': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _unlink. See online help for details. [00:01:27] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\corecrt_io.h(553): note: see declaration of 'unlink' [00:01:27] tempdir.cpp(172): warning C4996: 'chdir': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _chdir. See online help for details. [00:01:27] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\direct.h(101): note: see declaration of 'chdir' [00:01:27] tempdir.cpp(190): warning C4996: 'chdir': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _chdir. See online help for details. [00:01:27] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\direct.h(101): note: see declaration of 'chdir' [00:01:27] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc tempfile.cpp /Fotempfile.obj [00:01:27] tempfile.cpp [00:01:28] tempfile.cpp(138): warning C4267: 'argument': conversion from 'size_t' to 'int', possible loss of data [00:01:28] tempfile.cpp(136): warning C4996: 'strdup': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _strdup. See online help for details. [00:01:28] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\string.h(530): note: see declaration of 'strdup' [00:01:28] tempfile.cpp(164): warning C4996: 'unlink': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _unlink. See online help for details. [00:01:28] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\corecrt_io.h(553): note: see declaration of 'unlink' [00:01:28] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc timer.cpp /Fotimer.obj [00:01:28] timer.cpp [00:01:28] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc unicode.cpp /Founicode.obj [00:01:28] unicode.cpp [00:01:29] unicode.cpp(36): warning C4267: 'argument': conversion from 'size_t' to 'int', possible loss of data [00:01:29] unicode.cpp(138): warning C4267: 'argument': conversion from 'size_t' to 'int', possible loss of data [00:01:29] unicode.cpp(252): warning C4996: 'strdup': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _strdup. See online help for details. [00:01:29] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\string.h(530): note: see declaration of 'strdup' [00:01:29] ./irep_ids_convert.exe table < irep_ids.txt > irep_ids.inc [00:01:29] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc irep_ids.cpp /Foirep_ids.obj [00:01:29] irep_ids.cpp [00:01:29] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc byte_operators.cpp /Fobyte_operators.obj [00:01:29] byte_operators.cpp [00:01:30] c:\projects\cbmc\src\util\byte_operators.cpp(39) : warning C4715: 'byte_extract_id': not all control paths return a value [00:01:30] c:\projects\cbmc\src\util\byte_operators.cpp(66) : warning C4715: 'byte_update_id': not all control paths return a value [00:01:30] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc string2int.cpp /Fostring2int.obj [00:01:30] string2int.cpp [00:01:30] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc file_util.cpp /Fofile_util.obj [00:01:30] file_util.cpp [00:01:31] file_util.cpp(57): warning C4996: 'getcwd': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _getcwd. See online help for details. [00:01:31] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\direct.h(93): note: see declaration of 'getcwd' [00:01:31] file_util.cpp(93): warning C4996: 'unlink': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _unlink. See online help for details. [00:01:31] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\corecrt_io.h(553): note: see declaration of 'unlink' [00:01:31] file_util.cpp(96): warning C4996: 'unlink': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _unlink. See online help for details. [00:01:31] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\corecrt_io.h(553): note: see declaration of 'unlink' [00:01:31] file_util.cpp(115): warning C4996: 'rmdir': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _rmdir. See online help for details. [00:01:31] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\direct.h(115): note: see declaration of 'rmdir' [00:01:31] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc memory_info.cpp /Fomemory_info.obj [00:01:31] memory_info.cpp [00:01:31] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc pipe_stream.cpp /Fopipe_stream.obj [00:01:31] pipe_stream.cpp [00:01:32] pipe_stream.cpp(419): warning C4244: 'argument': conversion from 'std::streamsize' to 'int', possible loss of data [00:01:32] pipe_stream.cpp(425): warning C4244: 'argument': conversion from 'std::streamsize' to 'int', possible loss of data [00:01:32] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc irep_hash.cpp /Foirep_hash.obj [00:01:32] irep_hash.cpp [00:01:32] c:\projects\cbmc\src\util\irep_hash.h(94): warning C4267: 'argument': conversion from 'size_t' to 'unsigned int', possible loss of data [00:01:32] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc endianness_map.cpp /Foendianness_map.obj [00:01:32] endianness_map.cpp [00:01:33] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc ssa_expr.cpp /Fossa_expr.obj [00:01:33] ssa_expr.cpp [00:01:34] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc json_expr.cpp /Fojson_expr.obj [00:01:34] json_expr.cpp [00:01:36] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc string_utils.cpp /Fostring_utils.obj [00:01:36] string_utils.cpp [00:01:37] lib /NOLOGO /OUT:util.lib arith_tools.obj base_type.obj cmdline.obj config.obj symbol_table.obj expr.obj expr_util.obj irep.obj language.obj lispexpr.obj lispirep.obj source_location.obj message.obj language_file.obj mp_arith.obj namespace.obj parse_options.obj rename.obj replace_expr.obj threeval.obj typecheck.obj graph.obj type.obj pointer_predicates.obj merge_irep.obj run.obj parser.obj replace_symbol.obj json.obj get_base_name.obj simplify_expr.obj simplify_expr_floatbv.obj simplify_expr_int.obj simplify_expr_array.obj simplify_expr_struct.obj simplify_expr_boolean.obj simplify_expr_pointer.obj get_module.obj string_hash.obj string_container.obj identifier.obj rational.obj options.obj dstring.obj find_symbols.obj rational_tools.obj ui_message.obj simplify_utils.obj time_stopping.obj symbol.obj irep_hash_container.obj cout_message.obj type_eq.obj guard.obj array_name.obj message_stream.obj substitute.obj decision_procedure.obj union_find.obj xml.obj xml_irep.obj xml_expr.obj std_types.obj std_code.obj format_constant.obj find_macros.obj ref_expr_set.obj std_expr.obj irep_serialization.obj fixedbv.obj rename_symbol.obj ieee_float.obj signal_catcher.obj pointer_offset_size.obj bv_arithmetic.obj tempdir.obj tempfile.obj timer.obj unicode.obj irep_ids.obj byte_operators.obj string2int.obj file_util.obj memory_info.obj pipe_stream.obj irep_hash.obj endianness_map.obj ssa_expr.obj json_expr.obj string_utils.obj [00:01:37] make[1]: Leaving directory `C:/projects/cbmc/src/util' [00:01:37] ## Entering langapi [00:01:37] make -C langapi [00:01:37] make[1]: Entering directory `C:/projects/cbmc/src/langapi' [00:01:37] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc mode.cpp /Fomode.obj [00:01:37] mode.cpp [00:01:37] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc language_ui.cpp /Folanguage_ui.obj [00:01:37] language_ui.cpp [00:01:39] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc languages.cpp /Folanguages.obj [00:01:39] languages.cpp [00:01:39] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc language_util.cpp /Folanguage_util.obj [00:01:40] language_util.cpp [00:01:41] lib /NOLOGO /OUT:langapi.lib mode.obj language_ui.obj languages.obj language_util.obj [00:01:41] make[1]: Leaving directory `C:/projects/cbmc/src/langapi' [00:01:41] ## Entering ansi-c [00:01:41] make -C ansi-c [00:01:41] make[1]: Entering directory `C:/projects/cbmc/src/ansi-c' [00:01:41] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc c_typecast.cpp /Foc_typecast.obj [00:01:41] c_typecast.cpp [00:01:42] bison -y -v $flags -pyyansi_c -d parser.y -o ansi_c_y.tab.cpp [00:01:42] if [ -e ansi_c_y.tab.hpp ] ; then mv ansi_c_y.tab.hpp ansi_c_y.tab.h ; else \ [00:01:42] mv ansi_c_y.tab.cpp.h ansi_c_y.tab.h ; fi [00:01:42] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc ansi_c_y.tab.cpp /Foansi_c_y.tab.obj [00:01:42] ansi_c_y.tab.cpp [00:01:43] ansi_c_y.tab.cpp(3614): warning C4065: switch statement contains 'default' but no 'case' labels [00:01:52] flex -Pyyansi_c -oansi_c_lex.yy.cpp scanner.l [00:01:52] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc ansi_c_lex.yy.cpp /Foansi_c_lex.yy.obj [00:01:52] ansi_c_lex.yy.cpp [00:01:52] ansi_c_lex.yy.cpp(7391): warning C4244: 'initializing': conversion from '__int64' to 'int', possible loss of data [00:01:52] ansi_c_lex.yy.cpp(7578): warning C4996: 'isatty': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _isatty. See online help for details. [00:01:52] scanner.l(19): note: see declaration of 'isatty' [00:01:54] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc ansi_c_parser.cpp /Foansi_c_parser.obj [00:01:54] ansi_c_parser.cpp [00:01:55] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc expr2c.cpp /Foexpr2c.obj [00:01:55] expr2c.cpp [00:02:00] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc ansi_c_language.cpp /Foansi_c_language.obj [00:02:00] ansi_c_language.cpp [00:02:01] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc c_sizeof.cpp /Foc_sizeof.obj [00:02:01] c_sizeof.cpp [00:02:02] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc ansi_c_scope.cpp /Foansi_c_scope.obj [00:02:02] ansi_c_scope.cpp [00:02:03] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc c_types.cpp /Foc_types.obj [00:02:03] c_types.cpp [00:02:04] c:\projects\cbmc\src\ansi-c\c_types.cpp(153) : warning C4715: 'size_type': not all control paths return a value [00:02:04] c:\projects\cbmc\src\ansi-c\c_types.cpp(589) : warning C4715: 'pointer_diff_type': not all control paths return a value [00:02:04] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc ansi_c_typecheck.cpp /Foansi_c_typecheck.obj [00:02:04] ansi_c_typecheck.cpp [00:02:05] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc c_preprocess.cpp /Foc_preprocess.obj [00:02:05] c_preprocess.cpp [00:02:06] c_preprocess.cpp(556): warning C4996: 'unlink': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _unlink. See online help for details. [00:02:06] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\stdio.h(380): note: see declaration of 'unlink' [00:02:06] c_preprocess.cpp(557): warning C4996: 'unlink': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _unlink. See online help for details. [00:02:06] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\stdio.h(380): note: see declaration of 'unlink' [00:02:06] c_preprocess.cpp(558): warning C4996: 'unlink': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _unlink. See online help for details. [00:02:06] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\stdio.h(380): note: see declaration of 'unlink' [00:02:06] c_preprocess.cpp(567): warning C4996: 'unlink': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _unlink. See online help for details. [00:02:06] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\stdio.h(380): note: see declaration of 'unlink' [00:02:06] c_preprocess.cpp(568): warning C4996: 'unlink': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _unlink. See online help for details. [00:02:06] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\stdio.h(380): note: see declaration of 'unlink' [00:02:06] c_preprocess.cpp(574): warning C4996: 'unlink': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _unlink. See online help for details. [00:02:06] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\stdio.h(380): note: see declaration of 'unlink' [00:02:06] c_preprocess.cpp(690): warning C4996: 'unlink': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _unlink. See online help for details. [00:02:06] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\stdio.h(380): note: see declaration of 'unlink' [00:02:06] c_preprocess.cpp(694): warning C4996: 'unlink': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _unlink. See online help for details. [00:02:06] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\stdio.h(380): note: see declaration of 'unlink' [00:02:06] c_preprocess.cpp(695): warning C4996: 'unlink': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _unlink. See online help for details. [00:02:06] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\stdio.h(380): note: see declaration of 'unlink' [00:02:06] c_preprocess.cpp(705): warning C4996: 'unlink': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _unlink. See online help for details. [00:02:06] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\stdio.h(380): note: see declaration of 'unlink' [00:02:06] c_preprocess.cpp(975): warning C4996: 'unlink': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _unlink. See online help for details. [00:02:06] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\stdio.h(380): note: see declaration of 'unlink' [00:02:06] c_preprocess.cpp(981): warning C4996: 'unlink': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _unlink. See online help for details. [00:02:06] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\stdio.h(380): note: see declaration of 'unlink' [00:02:06] c_preprocess.cpp(985): warning C4996: 'unlink': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _unlink. See online help for details. [00:02:06] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\stdio.h(380): note: see declaration of 'unlink' [00:02:06] c_preprocess.cpp(1113): warning C4996: 'unlink': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _unlink. See online help for details. [00:02:06] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\stdio.h(380): note: see declaration of 'unlink' [00:02:06] c_preprocess.cpp(1117): warning C4996: 'unlink': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _unlink. See online help for details. [00:02:06] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\stdio.h(380): note: see declaration of 'unlink' [00:02:06] c_preprocess.cpp(1118): warning C4996: 'unlink': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _unlink. See online help for details. [00:02:06] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\stdio.h(380): note: see declaration of 'unlink' [00:02:06] c_preprocess.cpp(1150): warning C4996: 'unlink': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _unlink. See online help for details. [00:02:06] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\stdio.h(380): note: see declaration of 'unlink' [00:02:06] c:\projects\cbmc\src\ansi-c\c_preprocess.cpp(121) : warning C4715: 'type_max': not all control paths return a value [00:02:07] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc c_storage_spec.cpp /Foc_storage_spec.obj [00:02:07] c_storage_spec.cpp [00:02:08] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc c_typecheck_base.cpp /Foc_typecheck_base.obj [00:02:08] c_typecheck_base.cpp [00:02:10] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc c_typecheck_initializer.cpp /Foc_typecheck_initializer.obj [00:02:10] c_typecheck_initializer.cpp [00:02:11] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc c_typecheck_typecast.cpp /Foc_typecheck_typecast.obj [00:02:11] c_typecheck_typecast.cpp [00:02:12] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc c_typecheck_code.cpp /Foc_typecheck_code.obj [00:02:13] c_typecheck_code.cpp [00:02:14] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc c_typecheck_expr.cpp /Foc_typecheck_expr.obj [00:02:14] c_typecheck_expr.cpp [00:02:17] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc c_typecheck_type.cpp /Foc_typecheck_type.obj [00:02:17] c_typecheck_type.cpp [00:02:20] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc string_constant.cpp /Fostring_constant.obj [00:02:20] string_constant.cpp [00:02:21] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc c_qualifiers.cpp /Foc_qualifiers.obj [00:02:21] c_qualifiers.cpp [00:02:21] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc c_typecheck_argc_argv.cpp /Foc_typecheck_argc_argv.obj [00:02:21] c_typecheck_argc_argv.cpp [00:02:22] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc ansi_c_parse_tree.cpp /Foansi_c_parse_tree.obj [00:02:22] ansi_c_parse_tree.cpp [00:02:23] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc preprocessor_line.cpp /Fopreprocessor_line.obj [00:02:23] preprocessor_line.cpp [00:02:24] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc ansi_c_convert_type.cpp /Foansi_c_convert_type.obj [00:02:24] ansi_c_convert_type.cpp [00:02:25] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc type2name.cpp /Fotype2name.obj [00:02:25] type2name.cpp [00:02:26] cl /Felibrary/converter.exe library/converter.cpp [00:02:26] Microsoft (R) C/C++ Optimizing Compiler Version 19.00.24215.1 for x64 [00:02:26] Copyright (C) Microsoft Corporation. All rights reserved. [00:02:26] [00:02:26] converter.cpp [00:02:26] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\xlocale(341): warning C4530: C++ exception handler used, but unwind semantics are not enabled. Specify /EHsc [00:02:26] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\exception(359): warning C4577: 'noexcept' used with no exception handling mode specified; termination on exception is not guaranteed. Specify /EHsc [00:02:26] Microsoft (R) Incremental Linker Version 14.00.24215.1 [00:02:26] Copyright (C) Microsoft Corporation. All rights reserved. [00:02:26] [00:02:26] /out:library/converter.exe [00:02:26] converter.obj [00:02:26] cat library/*.c | library/converter.exe > cprover_library.inc [00:02:26] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cprover_library.cpp /Focprover_library.obj [00:02:26] cprover_library.cpp [00:02:27] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc anonymous_member.cpp /Foanonymous_member.obj [00:02:27] anonymous_member.cpp [00:02:28] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc printf_formatter.cpp /Foprintf_formatter.obj [00:02:28] printf_formatter.cpp [00:02:29] cl /Fefile_converter.exe file_converter.cpp [00:02:29] Microsoft (R) C/C++ Optimizing Compiler Version 19.00.24215.1 for x64 [00:02:29] Copyright (C) Microsoft Corporation. All rights reserved. [00:02:29] [00:02:29] file_converter.cpp [00:02:29] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\xlocale(341): warning C4530: C++ exception handler used, but unwind semantics are not enabled. Specify /EHsc [00:02:29] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\exception(359): warning C4577: 'noexcept' used with no exception handling mode specified; termination on exception is not guaranteed. Specify /EHsc [00:02:29] Microsoft (R) Incremental Linker Version 14.00.24215.1 [00:02:29] Copyright (C) Microsoft Corporation. All rights reserved. [00:02:29] [00:02:29] /out:file_converter.exe [00:02:29] file_converter.obj [00:02:29] ./file_converter.exe < gcc_builtin_headers_generic.h > gcc_builtin_headers_generic.inc [00:02:29] ./file_converter.exe < gcc_builtin_headers_ia32.h > gcc_builtin_headers_ia32.inc [00:02:29] ./file_converter.exe < gcc_builtin_headers_ia32-2.h > gcc_builtin_headers_ia32-2.inc [00:02:29] ./file_converter.exe < gcc_builtin_headers_alpha.h > gcc_builtin_headers_alpha.inc [00:02:29] ./file_converter.exe < gcc_builtin_headers_arm.h > gcc_builtin_headers_arm.inc [00:02:29] ./file_converter.exe < gcc_builtin_headers_mips.h > gcc_builtin_headers_mips.inc [00:02:29] ./file_converter.exe < gcc_builtin_headers_power.h > gcc_builtin_headers_power.inc [00:02:30] ./file_converter.exe < arm_builtin_headers.h > arm_builtin_headers.inc [00:02:30] ./file_converter.exe < cw_builtin_headers.h > cw_builtin_headers.inc [00:02:30] ./file_converter.exe < clang_builtin_headers.h > clang_builtin_headers.inc [00:02:30] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc ansi_c_internal_additions.cpp /Foansi_c_internal_additions.obj [00:02:30] ansi_c_internal_additions.cpp [00:02:30] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc padding.cpp /Fopadding.obj [00:02:30] padding.cpp [00:02:31] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc ansi_c_declaration.cpp /Foansi_c_declaration.obj [00:02:31] ansi_c_declaration.cpp [00:02:32] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc designator.cpp /Fodesignator.obj [00:02:32] designator.cpp [00:02:33] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc ansi_c_entry_point.cpp /Foansi_c_entry_point.obj [00:02:33] ansi_c_entry_point.cpp [00:02:34] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc literals/parse_float.cpp /Foliterals/parse_float.obj [00:02:34] parse_float.cpp [00:02:35] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc literals/unescape_string.cpp /Foliterals/unescape_string.obj [00:02:35] unescape_string.cpp [00:02:35] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc literals/convert_float_literal.cpp /Foliterals/convert_float_literal.obj [00:02:35] convert_float_literal.cpp [00:02:36] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc literals/convert_character_literal.cpp /Foliterals/convert_character_literal.obj [00:02:36] convert_character_literal.cpp [00:02:37] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc literals/convert_integer_literal.cpp /Foliterals/convert_integer_literal.obj [00:02:37] convert_integer_literal.cpp [00:02:38] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc literals/convert_string_literal.cpp /Foliterals/convert_string_literal.obj [00:02:38] convert_string_literal.cpp [00:02:39] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc c_misc.cpp /Foc_misc.obj [00:02:39] c_misc.cpp [00:02:39] lib /NOLOGO /OUT:ansi-c.lib c_typecast.obj ansi_c_y.tab.obj ansi_c_lex.yy.obj ansi_c_parser.obj expr2c.obj ansi_c_language.obj c_sizeof.obj ansi_c_scope.obj c_types.obj ansi_c_typecheck.obj c_preprocess.obj c_storage_spec.obj c_typecheck_base.obj c_typecheck_initializer.obj c_typecheck_typecast.obj c_typecheck_code.obj c_typecheck_expr.obj c_typecheck_type.obj string_constant.obj c_qualifiers.obj c_typecheck_argc_argv.obj ansi_c_parse_tree.obj preprocessor_line.obj ansi_c_convert_type.obj type2name.obj cprover_library.obj anonymous_member.obj printf_formatter.obj ansi_c_internal_additions.obj padding.obj ansi_c_declaration.obj designator.obj ansi_c_entry_point.obj literals/parse_float.obj literals/unescape_string.obj literals/convert_float_literal.obj literals/convert_character_literal.obj literals/convert_integer_literal.obj literals/convert_string_literal.obj c_misc.obj [00:02:39] make[1]: Leaving directory `C:/projects/cbmc/src/ansi-c' [00:02:39] ## Entering linking [00:02:39] make -C linking [00:02:39] make[1]: Entering directory `C:/projects/cbmc/src/linking' [00:02:39] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc linking.cpp /Folinking.obj [00:02:39] linking.cpp [00:02:42] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc zero_initializer.cpp /Fozero_initializer.obj [00:02:42] zero_initializer.cpp [00:02:43] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc static_lifetime_init.cpp /Fostatic_lifetime_init.obj [00:02:43] static_lifetime_init.cpp [00:02:44] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc remove_internal_symbols.cpp /Foremove_internal_symbols.obj [00:02:44] remove_internal_symbols.cpp [00:02:45] lib /NOLOGO /OUT:linking.lib linking.obj zero_initializer.obj static_lifetime_init.obj remove_internal_symbols.obj [00:02:45] make[1]: Leaving directory `C:/projects/cbmc/src/linking' [00:02:45] ## Entering cpp [00:02:45] make -C cpp [00:02:45] make[1]: Entering directory `C:/projects/cbmc/src/cpp' [00:02:45] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_id.cpp /Focpp_id.obj [00:02:45] cpp_id.cpp [00:02:47] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_language.cpp /Focpp_language.obj [00:02:47] cpp_language.cpp [00:02:49] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc expr2cpp.cpp /Foexpr2cpp.obj [00:02:49] expr2cpp.cpp [00:02:51] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_parser.cpp /Focpp_parser.obj [00:02:51] cpp_parser.cpp [00:02:52] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_typecheck.cpp /Focpp_typecheck.obj [00:02:52] cpp_typecheck.cpp [00:02:54] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_convert_type.cpp /Focpp_convert_type.obj [00:02:54] cpp_convert_type.cpp [00:02:55] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_typecheck_expr.cpp /Focpp_typecheck_expr.obj [00:02:55] cpp_typecheck_expr.cpp [00:02:59] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_typecheck_code.cpp /Focpp_typecheck_code.obj [00:02:59] cpp_typecheck_code.cpp [00:03:00] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_typecheck_type.cpp /Focpp_typecheck_type.obj [00:03:00] cpp_typecheck_type.cpp [00:03:02] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc parse.cpp /Foparse.obj [00:03:02] parse.cpp [00:03:06] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_parse_tree.cpp /Focpp_parse_tree.obj [00:03:06] cpp_parse_tree.cpp [00:03:06] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_token_buffer.cpp /Focpp_token_buffer.obj [00:03:06] cpp_token_buffer.cpp [00:03:07] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_typecheck_fargs.cpp /Focpp_typecheck_fargs.obj [00:03:07] cpp_typecheck_fargs.cpp [00:03:08] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_typecheck_resolve.cpp /Focpp_typecheck_resolve.obj [00:03:08] cpp_typecheck_resolve.cpp [00:03:12] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_util.cpp /Focpp_util.obj [00:03:12] cpp_util.cpp [00:03:13] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_enum_type.cpp /Focpp_enum_type.obj [00:03:13] cpp_enum_type.cpp [00:03:13] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_typecheck_function.cpp /Focpp_typecheck_function.obj [00:03:13] cpp_typecheck_function.cpp [00:03:15] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_typecheck_namespace.cpp /Focpp_typecheck_namespace.obj [00:03:15] cpp_typecheck_namespace.cpp [00:03:16] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_name.cpp /Focpp_name.obj [00:03:16] cpp_name.cpp [00:03:17] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_is_pod.cpp /Focpp_is_pod.obj [00:03:17] cpp_is_pod.cpp [00:03:18] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_scope.cpp /Focpp_scope.obj [00:03:18] cpp_scope.cpp [00:03:20] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc template_map.cpp /Fotemplate_map.obj [00:03:20] template_map.cpp [00:03:21] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_scopes.cpp /Focpp_scopes.obj [00:03:21] cpp_scopes.cpp [00:03:22] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_declarator.cpp /Focpp_declarator.obj [00:03:22] cpp_declarator.cpp [00:03:23] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_instantiate_template.cpp /Focpp_instantiate_template.obj [00:03:23] cpp_instantiate_template.cpp [00:03:25] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_internal_additions.cpp /Focpp_internal_additions.obj [00:03:25] cpp_internal_additions.cpp [00:03:26] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_type2name.cpp /Focpp_type2name.obj [00:03:26] cpp_type2name.cpp [00:03:27] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_typecheck_linkage_spec.cpp /Focpp_typecheck_linkage_spec.obj [00:03:27] cpp_typecheck_linkage_spec.cpp [00:03:28] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_typecheck_template.cpp /Focpp_typecheck_template.obj [00:03:28] cpp_typecheck_template.cpp [00:03:31] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_typecheck_method_bodies.cpp /Focpp_typecheck_method_bodies.obj [00:03:31] cpp_typecheck_method_bodies.cpp [00:03:32] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_typecheck_initializer.cpp /Focpp_typecheck_initializer.obj [00:03:32] cpp_typecheck_initializer.cpp [00:03:33] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_typecheck_compound_type.cpp /Focpp_typecheck_compound_type.obj [00:03:33] cpp_typecheck_compound_type.cpp [00:03:37] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_constructor.cpp /Focpp_constructor.obj [00:03:37] cpp_constructor.cpp [00:03:39] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_destructor.cpp /Focpp_destructor.obj [00:03:39] cpp_destructor.cpp [00:03:41] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_typecheck_conversions.cpp /Focpp_typecheck_conversions.obj [00:03:41] cpp_typecheck_conversions.cpp [00:03:43] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_typecheck_declaration.cpp /Focpp_typecheck_declaration.obj [00:03:43] cpp_typecheck_declaration.cpp [00:03:45] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_declarator_converter.cpp /Focpp_declarator_converter.obj [00:03:45] cpp_declarator_converter.cpp [00:03:47] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_declaration.cpp /Focpp_declaration.obj [00:03:47] cpp_declaration.cpp [00:03:48] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_namespace_spec.cpp /Focpp_namespace_spec.obj [00:03:48] cpp_namespace_spec.cpp [00:03:49] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_typecheck_using.cpp /Focpp_typecheck_using.obj [00:03:49] cpp_typecheck_using.cpp [00:03:50] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_exception_id.cpp /Focpp_exception_id.obj [00:03:50] cpp_exception_id.cpp [00:03:51] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_typecheck_enum_type.cpp /Focpp_typecheck_enum_type.obj [00:03:51] cpp_typecheck_enum_type.cpp [00:03:52] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_typecheck_bases.cpp /Focpp_typecheck_bases.obj [00:03:52] cpp_typecheck_bases.cpp [00:03:54] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_typecheck_constructor.cpp /Focpp_typecheck_constructor.obj [00:03:54] cpp_typecheck_constructor.cpp [00:03:56] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_typecheck_destructor.cpp /Focpp_typecheck_destructor.obj [00:03:56] cpp_typecheck_destructor.cpp [00:03:58] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_typecheck_virtual_table.cpp /Focpp_typecheck_virtual_table.obj [00:03:58] cpp_typecheck_virtual_table.cpp [00:03:59] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc cpp_typecheck_static_assert.cpp /Focpp_typecheck_static_assert.obj [00:03:59] cpp_typecheck_static_assert.cpp [00:04:01] lib /NOLOGO /OUT:cpp.lib cpp_id.obj cpp_language.obj expr2cpp.obj cpp_parser.obj cpp_typecheck.obj cpp_convert_type.obj cpp_typecheck_expr.obj cpp_typecheck_code.obj cpp_typecheck_type.obj parse.obj cpp_parse_tree.obj cpp_token_buffer.obj cpp_typecheck_fargs.obj cpp_typecheck_resolve.obj cpp_util.obj cpp_enum_type.obj cpp_typecheck_function.obj cpp_typecheck_namespace.obj cpp_name.obj cpp_is_pod.obj cpp_scope.obj template_map.obj cpp_scopes.obj cpp_declarator.obj cpp_instantiate_template.obj cpp_internal_additions.obj cpp_type2name.obj cpp_typecheck_linkage_spec.obj cpp_typecheck_template.obj cpp_typecheck_method_bodies.obj cpp_typecheck_initializer.obj cpp_typecheck_compound_type.obj cpp_constructor.obj cpp_destructor.obj cpp_typecheck_conversions.obj cpp_typecheck_declaration.obj cpp_declarator_converter.obj cpp_declaration.obj cpp_namespace_spec.obj cpp_typecheck_using.obj cpp_exception_id.obj cpp_typecheck_enum_type.obj cpp_typecheck_bases.obj cpp_typecheck_constructor.obj cpp_typecheck_destructor.obj cpp_typecheck_virtual_table.obj cpp_typecheck_static_assert.obj [00:04:01] make[1]: Leaving directory `C:/projects/cbmc/src/cpp' [00:04:01] ## Entering xmllang [00:04:01] make -C xmllang [00:04:01] make[1]: Entering directory `C:/projects/cbmc/src/xmllang' [00:04:01] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc xml_parser.cpp /Foxml_parser.obj [00:04:01] xml_parser.cpp [00:04:02] bison -y -v $flags -pyyxml -d parser.y -o xml_y.tab.cpp [00:04:02] if [ -e xml_y.tab.hpp ] ; then mv xml_y.tab.hpp xml_y.tab.h ; else \ [00:04:02] mv xml_y.tab.cpp.h xml_y.tab.h ; fi [00:04:02] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc xml_y.tab.cpp /Foxml_y.tab.obj [00:04:02] xml_y.tab.cpp [00:04:02] xml_y.tab.cpp(1098): warning C4065: switch statement contains 'default' but no 'case' labels [00:04:02] parser.y(89): warning C4996: 'strdup': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _strdup. See online help for details. [00:04:02] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\string.h(530): note: see declaration of 'strdup' [00:04:03] flex -Pyyxml -oxml_lex.yy.cpp scanner.l [00:04:03] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc xml_lex.yy.cpp /Foxml_lex.yy.obj [00:04:03] xml_lex.yy.cpp [00:04:03] scanner.l(66): warning C4996: 'strdup': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _strdup. See online help for details. [00:04:03] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\string.h(530): note: see declaration of 'strdup' [00:04:03] scanner.l(67): warning C4996: 'strdup': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _strdup. See online help for details. [00:04:03] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\string.h(530): note: see declaration of 'strdup' [00:04:03] scanner.l(74): warning C4996: 'strdup': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _strdup. See online help for details. [00:04:03] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\string.h(530): note: see declaration of 'strdup' [00:04:03] scanner.l(76): warning C4996: 'strdup': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _strdup. See online help for details. [00:04:03] C:\Program Files (x86)\Windows Kits\10\include\10.0.14393.0\ucrt\string.h(530): note: see declaration of 'strdup' [00:04:03] xml_lex.yy.cpp(1281): warning C4244: 'initializing': conversion from '__int64' to 'int', possible loss of data [00:04:03] xml_lex.yy.cpp(1468): warning C4996: 'isatty': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _isatty. See online help for details. [00:04:03] scanner.l(8): note: see declaration of 'isatty' [00:04:04] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc xml_parse_tree.cpp /Foxml_parse_tree.obj [00:04:04] xml_parse_tree.cpp [00:04:04] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc graphml.cpp /Fographml.obj [00:04:04] graphml.cpp [00:04:07] lib /NOLOGO /OUT:xmllang.lib xml_parser.obj xml_y.tab.obj xml_lex.yy.obj xml_parse_tree.obj graphml.obj [00:04:07] make[1]: Leaving directory `C:/projects/cbmc/src/xmllang' [00:04:07] ## Entering assembler [00:04:07] make -C assembler [00:04:07] make[1]: Entering directory `C:/projects/cbmc/src/assembler' [00:04:07] flex -Pyyassembler -oassembler_lex.yy.cpp scanner.l [00:04:07] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc assembler_lex.yy.cpp /Foassembler_lex.yy.obj [00:04:07] assembler_lex.yy.cpp [00:04:07] assembler_lex.yy.cpp(1161): warning C4244: 'initializing': conversion from '__int64' to 'int', possible loss of data [00:04:07] assembler_lex.yy.cpp(1348): warning C4996: 'isatty': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _isatty. See online help for details. [00:04:07] scanner.l(8): note: see declaration of 'isatty' [00:04:07] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc assembler_parser.cpp /Foassembler_parser.obj [00:04:07] assembler_parser.cpp [00:04:08] lib /NOLOGO /OUT:assembler.lib assembler_lex.yy.obj assembler_parser.obj [00:04:08] make[1]: Leaving directory `C:/projects/cbmc/src/assembler' [00:04:08] ## Entering java_bytecode [00:04:08] make -C java_bytecode [00:04:08] make[1]: Entering directory `C:/projects/cbmc/src/java_bytecode' [00:04:08] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc java_bytecode_language.cpp /Fojava_bytecode_language.obj [00:04:08] java_bytecode_language.cpp [00:04:10] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc java_bytecode_parse_tree.cpp /Fojava_bytecode_parse_tree.obj [00:04:10] java_bytecode_parse_tree.cpp [00:04:12] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc java_bytecode_typecheck.cpp /Fojava_bytecode_typecheck.obj [00:04:12] java_bytecode_typecheck.cpp [00:04:13] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc expr2java.cpp /Foexpr2java.obj [00:04:13] expr2java.cpp [00:04:14] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc java_bytecode_convert_class.cpp /Fojava_bytecode_convert_class.obj [00:04:14] java_bytecode_convert_class.cpp [00:04:15] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc java_types.cpp /Fojava_types.obj [00:04:15] java_types.cpp [00:04:16] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc java_entry_point.cpp /Fojava_entry_point.obj [00:04:16] java_entry_point.cpp [00:04:18] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc java_bytecode_typecheck_code.cpp /Fojava_bytecode_typecheck_code.obj [00:04:18] java_bytecode_typecheck_code.cpp [00:04:19] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc java_bytecode_typecheck_expr.cpp /Fojava_bytecode_typecheck_expr.obj [00:04:19] java_bytecode_typecheck_expr.cpp [00:04:20] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc java_bytecode_typecheck_type.cpp /Fojava_bytecode_typecheck_type.obj [00:04:20] java_bytecode_typecheck_type.cpp [00:04:21] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc java_bytecode_internal_additions.cpp /Fojava_bytecode_internal_additions.obj [00:04:21] java_bytecode_internal_additions.cpp [00:04:22] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc java_root_class.cpp /Fojava_root_class.obj [00:04:22] java_root_class.cpp [00:04:22] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc java_bytecode_parser.cpp /Fojava_bytecode_parser.obj [00:04:22] java_bytecode_parser.cpp [00:04:25] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc bytecode_info.cpp /Fobytecode_info.obj [00:04:25] bytecode_info.cpp [00:04:25] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc java_class_loader.cpp /Fojava_class_loader.obj [00:04:25] java_class_loader.cpp [00:04:27] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc jar_file.cpp /Fojar_file.obj [00:04:27] jar_file.cpp [00:04:28] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc java_object_factory.cpp /Fojava_object_factory.obj [00:04:28] java_object_factory.cpp [00:04:29] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc java_bytecode_convert_method.cpp /Fojava_bytecode_convert_method.obj [00:04:29] java_bytecode_convert_method.cpp [00:04:30] java_bytecode_convert_method.cpp(1895): warning C4267: 'argument': conversion from 'size_t' to 'unsigned int', possible loss of data [00:04:30] java_bytecode_convert_method.cpp(1912): warning C4267: 'argument': conversion from 'size_t' to 'unsigned int', possible loss of data [00:04:36] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc java_local_variable_table.cpp /Fojava_local_variable_table.obj [00:04:36] java_local_variable_table.cpp [00:04:37] java_local_variable_table.cpp(261): warning C4267: 'initializing': conversion from 'size_t' to 'unsigned int', possible loss of data [00:04:37] java_local_variable_table.cpp(314): warning C4267: 'initializing': conversion from 'size_t' to 'unsigned int', possible loss of data [00:04:37] java_local_variable_table.cpp(327): warning C4267: 'initializing': conversion from 'size_t' to 'unsigned int', possible loss of data [00:04:37] java_local_variable_table.cpp(362): warning C4267: 'argument': conversion from 'size_t' to 'unsigned int', possible loss of data [00:04:37] java_local_variable_table.cpp(424): warning C4267: '=': conversion from 'size_t' to 'unsigned int', possible loss of data [00:04:37] java_local_variable_table.cpp(431): warning C4267: 'argument': conversion from 'size_t' to 'const unsigned int', possible loss of data [00:04:37] java_local_variable_table.cpp(493): warning C4267: 'argument': conversion from 'size_t' to 'unsigned int', possible loss of data [00:04:37] java_local_variable_table.cpp(499): warning C4267: 'argument': conversion from 'size_t' to 'unsigned int', possible loss of data [00:04:37] java_local_variable_table.cpp(542): warning C4267: '=': conversion from 'size_t' to 'unsigned int', possible loss of data [00:04:37] java_local_variable_table.cpp(40): warning C4267: '=': conversion from 'size_t' to 'unsigned int', possible loss of data [00:04:37] java_local_variable_table.cpp(34): note: while compiling class template member function 'void procedure_local_cfg_baset::nodet,P,T>::operator ()(const procedure_local_cfg_baset::nodet,P,T>::method_with_amapt &)' [00:04:37] with [00:04:37] [ [00:04:37] P=java_bytecode_convert_methodt::method_with_amapt, [00:04:37] T=unsigned int [00:04:37] ] [00:04:37] ..\analyses/cfg_dominators.h(103): note: see reference to function template instantiation 'void procedure_local_cfg_baset::nodet,P,T>::operator ()(const procedure_local_cfg_baset::nodet,P,T>::method_with_amapt &)' being compiled [00:04:37] with [00:04:37] [ [00:04:37] P=java_bytecode_convert_methodt::method_with_amapt, [00:04:37] T=unsigned int [00:04:37] ] [00:04:37] ..\analyses/cfg_dominators.h(34): note: see reference to class template instantiation 'procedure_local_cfg_baset::nodet,P,T>' being compiled [00:04:37] with [00:04:37] [ [00:04:37] P=java_bytecode_convert_methodt::method_with_amapt, [00:04:37] T=unsigned int [00:04:37] ] [00:04:37] java_local_variable_table.cpp(431): note: see reference to class template instantiation 'cfg_dominators_templatet' being compiled [00:04:37] java_local_variable_table.cpp(54): warning C4267: 'argument': conversion from 'size_t' to 'const unsigned int', possible loss of data [00:04:37] java_local_variable_table.cpp(71): warning C4267: 'argument': conversion from 'size_t' to 'const unsigned int', possible loss of data [00:04:40] lib /NOLOGO /OUT:java_bytecode.lib java_bytecode_language.obj java_bytecode_parse_tree.obj java_bytecode_typecheck.obj expr2java.obj java_bytecode_convert_class.obj java_types.obj java_entry_point.obj java_bytecode_typecheck_code.obj java_bytecode_typecheck_expr.obj java_bytecode_typecheck_type.obj java_bytecode_internal_additions.obj java_root_class.obj java_bytecode_parser.obj bytecode_info.obj java_class_loader.obj jar_file.obj java_object_factory.obj java_bytecode_convert_method.obj java_local_variable_table.obj [00:04:40] make[1]: Leaving directory `C:/projects/cbmc/src/java_bytecode' [00:04:40] ## Entering jsil [00:04:40] make -C jsil [00:04:40] make[1]: Entering directory `C:/projects/cbmc/src/jsil' [00:04:40] bison -y -v $flags -pyyjsil -d parser.y -o jsil_y.tab.cpp [00:04:40] if [ -e jsil_y.tab.hpp ] ; then mv jsil_y.tab.hpp jsil_y.tab.h ; else \ [00:04:40] mv jsil_y.tab.cpp.h jsil_y.tab.h ; fi [00:04:40] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc jsil_y.tab.cpp /Fojsil_y.tab.obj [00:04:40] jsil_y.tab.cpp [00:04:40] jsil_y.tab.cpp(1486): warning C4065: switch statement contains 'default' but no 'case' labels [00:04:41] flex -Pyyjsil -ojsil_lex.yy.cpp scanner.l [00:04:41] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc jsil_lex.yy.cpp /Fojsil_lex.yy.obj [00:04:41] jsil_lex.yy.cpp [00:04:42] jsil_lex.yy.cpp(2831): warning C4244: 'initializing': conversion from '__int64' to 'int', possible loss of data [00:04:42] jsil_lex.yy.cpp(3018): warning C4996: 'isatty': The POSIX name for this item is deprecated. Instead, use the ISO C and C++ conformant name: _isatty. See online help for details. [00:04:42] scanner.l(8): note: see declaration of 'isatty' [00:04:43] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc jsil_convert.cpp /Fojsil_convert.obj [00:04:43] jsil_convert.cpp [00:04:44] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc jsil_language.cpp /Fojsil_language.obj [00:04:44] jsil_language.cpp [00:04:45] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc jsil_parse_tree.cpp /Fojsil_parse_tree.obj [00:04:45] jsil_parse_tree.cpp [00:04:46] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc jsil_types.cpp /Fojsil_types.obj [00:04:46] jsil_types.cpp [00:04:47] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc jsil_parser.cpp /Fojsil_parser.obj [00:04:47] jsil_parser.cpp [00:04:48] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc jsil_typecheck.cpp /Fojsil_typecheck.obj [00:04:48] jsil_typecheck.cpp [00:04:48] jsil_typecheck.cpp(1382): warning C4101: 'e': unreferenced local variable [00:04:49] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc expr2jsil.cpp /Foexpr2jsil.obj [00:04:49] expr2jsil.cpp [00:04:50] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc jsil_entry_point.cpp /Fojsil_entry_point.obj [00:04:50] jsil_entry_point.cpp [00:04:52] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. /nologo /c /EHsc jsil_internal_additions.cpp /Fojsil_internal_additions.obj [00:04:52] jsil_internal_additions.cpp [00:04:53] lib /NOLOGO /OUT:jsil.lib jsil_y.tab.obj jsil_lex.yy.obj jsil_convert.obj jsil_language.obj jsil_parse_tree.obj jsil_types.obj jsil_parser.obj jsil_typecheck.obj expr2jsil.obj jsil_entry_point.obj jsil_internal_additions.obj [00:04:53] make[1]: Leaving directory `C:/projects/cbmc/src/jsil' [00:04:53] ## Entering solvers [00:04:53] make -C solvers [00:04:53] make[1]: Entering directory `C:/projects/cbmc/src/solvers' [00:04:53] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS /nologo /c /EHsc sat/satcheck_minisat2.cpp /Fosat/satcheck_minisat2.obj [00:04:53] satcheck_minisat2.cpp [00:04:53] ../../minisat-2.2.1\minisat/core/SolverTypes.h(97): warning C4800: 'int': forcing value to bool 'true' or 'false' (performance warning) [00:04:53] ../../minisat-2.2.1\minisat/core/SolverTypes.h(130): warning C4200: nonstandard extension used: zero-sized array in struct/union [00:04:53] ../../minisat-2.2.1\minisat/core/SolverTypes.h(130): note: This member will be ignored by a defaulted constructor or copy/move assignment operator [00:04:53] ../../minisat-2.2.1\minisat/core/Solver.h(299): warning C4244: '+=': conversion from 'double' to 'float', possible loss of data [00:04:53] ../../minisat-2.2.1\minisat/core/Solver.h(302): warning C4305: '*=': truncation from 'double' to 'float' [00:04:53] ../../minisat-2.2.1\minisat/simp/SimpSolver.h(169): warning C4800: 'const char': forcing value to bool 'true' or 'false' (performance warning) [00:04:53] sat/satcheck_minisat2.cpp(41): warning C4267: 'argument': conversion from 'size_t' to 'int', possible loss of data [00:04:54] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS /nologo /c /EHsc sat/cnf.cpp /Fosat/cnf.obj [00:04:54] cnf.cpp [00:04:54] sat/cnf.cpp(557): warning C4267: 'argument': conversion from 'size_t' to 'literalt::var_not', possible loss of data [00:04:55] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS /nologo /c /EHsc sat/dimacs_cnf.cpp /Fosat/dimacs_cnf.obj [00:04:55] dimacs_cnf.cpp [00:04:56] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS /nologo /c /EHsc sat/cnf_clause_list.cpp /Fosat/cnf_clause_list.obj [00:04:56] cnf_clause_list.cpp [00:04:57] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS /nologo /c /EHsc sat/pbs_dimacs_cnf.cpp /Fosat/pbs_dimacs_cnf.obj [00:04:57] pbs_dimacs_cnf.cpp [00:04:59] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS /nologo /c /EHsc sat/read_dimacs_cnf.cpp /Fosat/read_dimacs_cnf.obj [00:04:59] read_dimacs_cnf.cpp [00:04:59] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS /nologo /c /EHsc sat/resolution_proof.cpp /Fosat/resolution_proof.obj [00:04:59] resolution_proof.cpp [00:05:00] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS /nologo /c /EHsc sat/satcheck.cpp /Fosat/satcheck.obj [00:05:00] satcheck.cpp [00:05:00] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS /nologo /c /EHsc qbf/qdimacs_cnf.cpp /Foqbf/qdimacs_cnf.obj [00:05:00] qdimacs_cnf.cpp [00:05:01] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS /nologo /c /EHsc qbf/qbf_quantor.cpp /Foqbf/qbf_quantor.obj [00:05:01] qbf_quantor.cpp [00:05:03] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS /nologo /c /EHsc qbf/qbf_skizzo.cpp /Foqbf/qbf_skizzo.obj [00:05:03] qbf_skizzo.cpp [00:05:04] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS /nologo /c /EHsc qbf/qdimacs_core.cpp /Foqbf/qdimacs_core.obj [00:05:04] qdimacs_core.cpp [00:05:05] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS /nologo /c /EHsc qbf/qbf_qube.cpp /Foqbf/qbf_qube.obj [00:05:05] qbf_qube.cpp [00:05:06] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS /nologo /c /EHsc qbf/qbf_qube_core.cpp /Foqbf/qbf_qube_core.obj [00:05:06] qbf_qube_core.cpp [00:05:08] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS /nologo /c /EHsc prop/prop.cpp /Foprop/prop.obj [00:05:08] prop.cpp [00:05:08] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS /nologo /c /EHsc prop/prop_conv.cpp /Foprop/prop_conv.obj [00:05:08] prop_conv.cpp [00:05:09] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS /nologo /c /EHsc prop/prop_conv_store.cpp /Foprop/prop_conv_store.obj [00:05:10] prop_conv_store.cpp [00:05:11] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS /nologo /c /EHsc prop/cover_goals.cpp /Foprop/cover_goals.obj [00:05:11] cover_goals.cpp [00:05:11] prop/cover_goals.cpp(127): warning C4267: '=': conversion from 'size_t' to 'unsigned int', possible loss of data [00:05:12] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS /nologo /c /EHsc prop/literal.cpp /Foprop/literal.obj [00:05:12] literal.cpp [00:05:12] cl /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++14 -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS /nologo /c /EHsc prop/aig.cpp /Foprop/aig.obj [00:05:12] aig.cpp [00:05:13] c:\projects\cbmc\src\solvers\prop\aig.h(100): warning C4267: 'argument': conversion from 'size_t' to 'literalt::var_not', possible loss of data [00:05:13] prop/aig.cpp(29): error C2039: 'to_string': is not a member of 'std' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\map(15): note: see declaration of 'std' [00:05:13] prop/aig.cpp(29): error C3861: 'to_string': identifier not found [00:05:13] prop/aig.cpp(46): error C2039: 'to_string': is not a member of 'std' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\map(15): note: see declaration of 'std' [00:05:13] prop/aig.cpp(46): error C3861: 'to_string': identifier not found [00:05:13] prop/aig.cpp(64): warning C4267: 'argument': conversion from 'size_t' to 'literalt::var_not', possible loss of data [00:05:13] prop/aig.cpp(160): error C2679: binary '<<': no operator found which takes a right-hand operand of type 'std::string' (or there is no acceptable conversion) [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(495): note: could be 'std::basic_ostream> &std::basic_ostream>::operator <<(std::basic_streambuf> *)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(475): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(const void *)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(455): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(long double)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(435): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(double)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(415): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(float)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(395): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(unsigned __int64)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(375): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(__int64)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(355): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(unsigned long)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(335): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(long)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(315): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(unsigned int)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(290): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(int)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(270): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(unsigned short)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(236): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(short)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(216): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(bool)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(209): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(std::ios_base &(__cdecl *)(std::ios_base &))' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(202): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(std::basic_ios> &(__cdecl *)(std::basic_ios> &))' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(196): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(std::basic_ostream> &(__cdecl *)(std::basic_ostream> &))' [00:05:13] c:\projects\cbmc\src\solvers\prop\aig.h(138): note: or 'std::ostream &operator <<(std::ostream &,const aigt &)' [00:05:13] ..\solvers/prop/literal.h(190): note: or 'std::ostream &operator <<(std::ostream &,literalt)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(692): note: or 'std::basic_ostream> &std::operator <<>(std::basic_ostream> &,const char *)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(739): note: or 'std::basic_ostream> &std::operator <<>(std::basic_ostream> &,char)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(777): note: or 'std::basic_ostream> &std::operator <<>(std::basic_ostream> &,const char *)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(824): note: or 'std::basic_ostream> &std::operator <<>(std::basic_ostream> &,char)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(950): note: or 'std::basic_ostream> &std::operator <<>(std::basic_ostream> &,const signed char *)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(957): note: or 'std::basic_ostream> &std::operator <<>(std::basic_ostream> &,signed char)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(964): note: or 'std::basic_ostream> &std::operator <<>(std::basic_ostream> &,const unsigned char *)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(971): note: or 'std::basic_ostream> &std::operator <<>(std::basic_ostream> &,unsigned char)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(981): note: or 'std::basic_ostream> &std::operator <<,std::string>(std::basic_ostream> &&,const _Ty &)' [00:05:13] with [00:05:13] [ [00:05:13] _Ty=std::string [00:05:13] ] [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(1019): note: or 'std::basic_ostream> &std::operator <<>(std::basic_ostream> &,const std::error_code &)' [00:05:13] prop/aig.cpp(160): note: while trying to match the argument list '(std::ostream, std::string)' [00:05:13] prop/aig.cpp(196): error C2679: binary '<<': no operator found which takes a right-hand operand of type 'std::string' (or there is no acceptable conversion) [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(495): note: could be 'std::basic_ostream> &std::basic_ostream>::operator <<(std::basic_streambuf> *)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(475): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(const void *)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(455): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(long double)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(435): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(double)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(415): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(float)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(395): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(unsigned __int64)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(375): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(__int64)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(355): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(unsigned long)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(335): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(long)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(315): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(unsigned int)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(290): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(int)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(270): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(unsigned short)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(236): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(short)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(216): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(bool)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(209): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(std::ios_base &(__cdecl *)(std::ios_base &))' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(202): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(std::basic_ios> &(__cdecl *)(std::basic_ios> &))' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(196): note: or 'std::basic_ostream> &std::basic_ostream>::operator <<(std::basic_ostream> &(__cdecl *)(std::basic_ostream> &))' [00:05:13] c:\projects\cbmc\src\solvers\prop\aig.h(138): note: or 'std::ostream &operator <<(std::ostream &,const aigt &)' [00:05:13] ..\solvers/prop/literal.h(190): note: or 'std::ostream &operator <<(std::ostream &,literalt)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(692): note: or 'std::basic_ostream> &std::operator <<>(std::basic_ostream> &,const char *)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(739): note: or 'std::basic_ostream> &std::operator <<>(std::basic_ostream> &,char)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(777): note: or 'std::basic_ostream> &std::operator <<>(std::basic_ostream> &,const char *)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(824): note: or 'std::basic_ostream> &std::operator <<>(std::basic_ostream> &,char)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(950): note: or 'std::basic_ostream> &std::operator <<>(std::basic_ostream> &,const signed char *)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(957): note: or 'std::basic_ostream> &std::operator <<>(std::basic_ostream> &,signed char)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(964): note: or 'std::basic_ostream> &std::operator <<>(std::basic_ostream> &,const unsigned char *)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(971): note: or 'std::basic_ostream> &std::operator <<>(std::basic_ostream> &,unsigned char)' [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(981): note: or 'std::basic_ostream> &std::operator <<,std::string>(std::basic_ostream> &&,const _Ty &)' [00:05:13] with [00:05:13] [ [00:05:13] _Ty=std::string [00:05:13] ] [00:05:13] C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\ostream(1019): note: or 'std::basic_ostream> &std::operator <<>(std::basic_ostream> &,const std::error_code &)' [00:05:13] prop/aig.cpp(196): note: while trying to match the argument list '(std::basic_ostream>, std::string)' [00:05:13] prop/aig.cpp(276): warning C4267: 'argument': conversion from 'size_t' to 'literalt::var_not', possible loss of data [00:05:13] make[1]: *** [prop/aig.obj] Error 2 [00:05:13] make[1]: Leaving directory `C:/projects/cbmc/src/solvers' [00:05:13] make: *** [solvers.dir] Error 2 [00:05:13] Command exited with code 2 [00:05:13] $blockRdp = $true; iex ((new-object net.webclient).DownloadString('https://raw.githubusercontent.com/appveyor/ci/master/scripts/enable-rdp.ps1')) [00:05:17] Remote Desktop connection details: [00:05:17] Server: 74.205.54.20:34189 [00:05:17] Username: appveyor [00:05:17] Password: I93Tt8dGw2J(-u6 [00:05:17] There is 'Delete me to continue build.txt' file has been created on Desktop - delete it to continue the build.