Skip to content

Reenable failing symex regressions on Windows. #1381

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
thk123 opened this issue Sep 13, 2017 · 2 comments
Closed

Reenable failing symex regressions on Windows. #1381

thk123 opened this issue Sep 13, 2017 · 2 comments

Comments

@thk123
Copy link
Contributor

thk123 commented Sep 13, 2017

Failing symex tests on Windows:

Running tests
  Running array1/test.desc  [OK]
  Running function_pointer1/test.desc  [OK]
  Running if1/test.desc  [OK]
  Running malloc1/test.desc  [OK]
  Running pointer1/test.desc  [OK]
  Running pointer2/test.desc  [OK]
  Running pointer3/test.desc  [OK]
  Running show-trace1/test.desc  [OK]
  Running struct1/test.desc  [OK]
  Running struct2/test.desc  [OK]
  Running struct3/test.desc  [OK]
  Running va_args_1/test.desc  [OK]
  Running va_args_10/test.desc  [FAILED]
  Running va_args_2/test.desc  [FAILED]
  Running va_args_3/test.desc  [FAILED]
  Running va_args_4/test.desc  [OK]
  Running va_args_5/test.desc  [FAILED]
  Running va_args_6/test.desc  [FAILED]
  Running va_args_7/test.desc  [OK]
  Running va_args_8/test.desc  [OK]
  Running va_args_9/test.desc  [OK]
Tests failed
  5 of 21 tests failed
Failed test: va_args_10
Parsing main.c
main.c
Converting
Type-checking main
Generating GOTO Program
Adding CPROVER library (x86_64)
Partial Inlining
Generic Property Instrumentation
Removal of function pointers and virtual functions
failed to dereference `symbol'
Number of visited locations: 28 (out of 79)
Number of dropped states: 1
Number of paths: 0
Number of infeasible paths: 0
Generated 0 VCC(s), 0 remaining after simplification
Runtime: 0s total, 0s SAT
** Results:
[main.assertion.1] assertion m3 == 6: SUCCESS
** 0 of 1 failed
VERIFICATION SUCCESSFUL
EXIT=0
SIGNAL=0
Failed test.desc lines:
^EXIT=10$ [FAILED]
^VERIFICATION FAILED$ [FAILED]
Failed test: va_args_2
Parsing main.c
main.c
Converting
Type-checking main
Generating GOTO Program
Adding CPROVER library (x86_64)
Partial Inlining
Generic Property Instrumentation
Removal of function pointers and virtual functions
failed to dereference `symbol'
Number of visited locations: 27 (out of 71)
Number of dropped states: 1
Number of paths: 0
Number of infeasible paths: 0
Generated 0 VCC(s), 0 remaining after simplification
Runtime: 0s total, 0s SAT
** Results:
[main.assertion.1] assertion m == 8: SUCCESS
** 0 of 1 failed
VERIFICATION SUCCESSFUL
EXIT=0
SIGNAL=0
Failed test.desc lines:
^EXIT=10$ [FAILED]
^VERIFICATION FAILED$ [FAILED]
Failed test: va_args_3
Parsing main.c
main.c
Converting
Type-checking main
Generating GOTO Program
Adding CPROVER library (x86_64)
Partial Inlining
Generic Property Instrumentation
Removal of function pointers and virtual functions
failed to dereference `symbol'
Number of visited locations: 26 (out of 69)
Number of dropped states: 1
Number of paths: 0
Number of infeasible paths: 0
Generated 0 VCC(s), 0 remaining after simplification
Runtime: 0s total, 0s SAT
** Results:
[main.assertion.1] assertion m == 1: SUCCESS
** 0 of 1 failed
VERIFICATION SUCCESSFUL
EXIT=0
SIGNAL=0
Failed test.desc lines:
^EXIT=10$ [FAILED]
^VERIFICATION FAILED$ [FAILED]
Failed test: va_args_5
Parsing main.c
main.c
Converting
Type-checking main
Generating GOTO Program
Adding CPROVER library (x86_64)
Partial Inlining
Generic Property Instrumentation
Removal of function pointers and virtual functions
failed to dereference `symbol'
Number of visited locations: 27 (out of 71)
Number of dropped states: 1
Number of paths: 0
Number of infeasible paths: 0
Generated 0 VCC(s), 0 remaining after simplification
Runtime: 0s total, 0s SAT
** Results:
[main.assertion.1] assertion m == 8: SUCCESS
** 0 of 1 failed
VERIFICATION SUCCESSFUL
EXIT=0
SIGNAL=0
Failed test.desc lines:
^EXIT=10$ [FAILED]
^VERIFICATION FAILED$ [FAILED]
Failed test: va_args_6
Parsing main.c
main.c
Converting
Type-checking main
Generating GOTO Program
Adding CPROVER library (x86_64)
Partial Inlining
Generic Property Instrumentation
Removal of function pointers and virtual functions
failed to dereference `symbol'
Number of visited locations: 26 (out of 69)
Number of dropped states: 1
Number of paths: 0
Number of infeasible paths: 0
Generated 0 VCC(s), 0 remaining after simplification
Runtime: 0s total, 0s SAT
** Results:
[main.assertion.1] assertion m == 2: SUCCESS
** 0 of 1 failed
VERIFICATION SUCCESSFUL
EXIT=0
SIGNAL=0
Failed test.desc lines:
^EXIT=10$ [FAILED]
^VERIFICATION FAILED$ [FAILED]
make[1]: *** [test] Error 1
make[1]: Leaving directory `C:/projects/cbmc/regression/symex'
make: *** [test] Error 1

These are currently manually disabled for just Windows. (Disabled in appveyor.yml)

thk123 pushed a commit to thk123/cbmc that referenced this issue Sep 13, 2017
Only fail on Windows, see diffblue#1381 for issue to re-enable
@thk123
Copy link
Contributor Author

thk123 commented Sep 13, 2017

Disabled by PR: #1378

@tautschnig
Copy link
Collaborator

We no longer use AppVeyor or selectively disable tests for Windows. Closing.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants