Skip to content

Reenable failing symex regressions on Windows.  #1381

Closed
@thk123

Description

@thk123

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)

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions