Skip to content

Re-enable failing test: symex/show-trace1 #1361

Closed
@thk123

Description

@thk123

In enabling the symex regression folder it appears this test doesn't work. The result still seems to match (i.e it verifies it can violate an assertion which it still thinks it can violate), but the information the test.desc is looking for is not present in the trace.

The counter example that is produces is:

State 2 file <built-in-additions> line 40 thread 0
----------------------------------------------------
  __CPROVER_dead_object#0=NULL (0000000000000000000000000000000000000000000000000000000000000000)

State 3 file <built-in-additions> line 39 thread 0
----------------------------------------------------
  __CPROVER_deallocated#0=NULL (0000000000000000000000000000000000000000000000000000000000000000)

State 4 file <built-in-additions> line 43 thread 0
----------------------------------------------------
  __CPROVER_malloc_is_new_array#0=FALSE (0)

State 5 file <built-in-additions> line 41 thread 0
----------------------------------------------------
  __CPROVER_malloc_object#0=NULL (0000000000000000000000000000000000000000000000000000000000000000)

State 6 file <built-in-additions> line 42 thread 0
----------------------------------------------------
  __CPROVER_malloc_size#0=0ul (0000000000000000000000000000000000000000000000000000000000000000)

State 7 file <built-in-additions> line 44 thread 0
----------------------------------------------------
  __CPROVER_memory_leak#0=NULL (0000000000000000000000000000000000000000000000000000000000000000)

State 8 file <built-in-additions> line 31 thread 0
----------------------------------------------------
  __CPROVER_next_thread_id#0=0ul (0000000000000000000000000000000000000000000000000000000000000000)

State 9 file <built-in-additions> line 99 thread 0
----------------------------------------------------
  __CPROVER_pipe_count#0=0u (00000000000000000000000000000000)

State 10 file <built-in-additions> line 66 thread 0
----------------------------------------------------
  __CPROVER_rounding_mode#0=0 (00000000000000000000000000000000)

State 11 file <built-in-additions> line 29 thread 0
----------------------------------------------------
  __CPROVER_thread_id#0=0ul (0000000000000000000000000000000000000000000000000000000000000000)

State 12 file <built-in-additions> line 30 thread 0
----------------------------------------------------
  __CPROVER_threads_exited#0=__CPROVER_threads_exited#1 (?)

But the test.desc is looking for:

^  i=2 .*$
^  j=3 .*$
^  k=6 .*$

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions