File tree Expand file tree Collapse file tree 2 files changed +4
-13
lines changed
goto-cc-cbmc/malloc-may-fail-should-work-with-compiled-binaries Expand file tree Collapse file tree 2 files changed +4
-13
lines changed Original file line number Diff line number Diff line change @@ -30,13 +30,6 @@ This folder contains the CProver regression test-suite.
3030
3131- ` winbug ` :
3232 These tests are currently known to be failing on Windows,
33- but passing on other platforms.
34- The reason for this is not known, and it's currently being investigated.
35- This was discovered during work done to port CI from [ Travis]
36- and [ AWS CodeBuild] to [ GitHub Actions] .
37- Worth noting that those tests were not being run on Windows before.
38-
39-
40- [ AWS CodeBuild ] : https://aws.amazon.com/codebuild/
41- [ GitHub Actions ] : https://github.com/features/actions
42- [ Travis ] : https://travis-ci.com/
33+ but passing on other platforms. https://github.com/diffblue/cbmc/pull/5572
34+ will address one part thereof; the remaining ones are C++ tests that fail on
35+ both Windows and MacOS for our lack of C++-11 support.
Original file line number Diff line number Diff line change 33--malloc-may-fail --malloc-fail-null
44^EXIT=10$
55^SIGNAL=0$
6- \[main.assertion.1\] line 7 assertion array != .* : FAILURE
6+ \[main.assertion.1\] line 7 assertion array != NULL : FAILURE
77--
88--
99Compiling a file with goto-cc should not affect how --malloc-may-fail behaves
10- Regex in the assertion because on travis for some reason the preprocessor seems to run
11- before cbmc.
You can’t perform that action at this time.
0 commit comments