File tree 2 files changed +4
-13
lines changed
goto-cc-cbmc/malloc-may-fail-should-work-with-compiled-binaries
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.
30
30
31
31
- ` winbug ` :
32
32
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 3
3
--malloc-may-fail --malloc-fail-null
4
4
^EXIT=10$
5
5
^SIGNAL=0$
6
- \[main.assertion.1\] line 7 assertion array != .* : FAILURE
6
+ \[main.assertion.1\] line 7 assertion array != NULL : FAILURE
7
7
--
8
8
--
9
9
Compiling 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