Counter-example traces for struct types incomplete #6845
Description
Description
CBMC version: 5.44
Operating system: Ubuntu 18.04
Exact command line resulting in the issue: cbmc struct.c --function main --trace
What behaviour did you expect: a better display
What happened instead:
There is a state on which the struct display strange value see the
struct.c Code
#include <assert.h>
struct str
{
float x;
short y;
int z;
};
int main (void)
{
int q;
struct str s;
s.x = q;
s.y = s.x+1;
s.z = s.y + s.x;
assert(q == s.z);
return 1;
}Trace Display Standard Output
Using the standard output here is what i get, look on state 25
Command used : cbmc struct.c --function main --trace
CBMC Trace
CBMC version 5.44.0 (cbmc-5.44.0) 64-bit x86_64 linux
Parsing struct.c
Converting
Type-checking struct
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.00456427s
size of program expression: 47 steps
simple slicing removed 5 assignments
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 2.4675e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.0324137s
Running propositional reduction
Post-processing
Runtime Post-process: 0.000135331s
Solving with MiniSAT 2.2.1 with simplifier
4219 variables, 16057 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.0945321s
Runtime decision procedure: 0.127061s
Building error trace
** Results:
struct.c function main
[main.assertion.1] line 19 assertion q == s.z: FAILURE
Trace for main.assertion.1:
State 24 file struct.c function main line 12 thread 0
----------------------------------------------------
q=0 (00000000 00000000 00000000 00000000)
State 25 file struct.c function main line 13 thread 0
----------------------------------------------------
s={ .x=s!0@1#1..x, .y=s!0@1#1..y, .$pad2=s!0@1#1..$pad2, .z=s!0@1#1..z } ({ ?, ?, ?, ? })
State 26 file struct.c function main line 15 thread 0
----------------------------------------------------
s.x=0.0f (00000000 00000000 00000000 00000000)
State 27 file struct.c function main line 16 thread 0
----------------------------------------------------
s.y=1 (00000000 00000001)
State 28 file struct.c function main line 17 thread 0
----------------------------------------------------
s.z=1 (00000000 00000000 00000000 00000001)
Violated property:
file struct.c function main line 19 thread 0
assertion q == s.z
q == s.z
XML UI output
Using XML UI option
Command cbmc struct.c --function main --trace --xml-ui
The types are not displayed for the child of the structure, e.g. struct
<?xml version="1.0" encoding="UTF-8"?>
<cprover>
<program>CBMC 5.44.0 (cbmc-5.44.0)</program>
<message type="STATUS-MESSAGE">
<text>CBMC version 5.44.0 (cbmc-5.44.0) 64-bit x86_64 linux</text>
</message>
<message type="STATUS-MESSAGE">
<text>Parsing struct.c</text>
</message>
<message type="STATUS-MESSAGE">
<text>Converting</text>
</message>
<message type="STATUS-MESSAGE">
<text>Type-checking struct</text>
</message>
<message type="STATUS-MESSAGE">
<text>Generating GOTO Program</text>
</message>
<message type="STATUS-MESSAGE">
<text>Adding CPROVER library (x86_64)</text>
</message>
<message type="STATUS-MESSAGE">
<text>Removal of function pointers and virtual functions</text>
</message>
<message type="STATUS-MESSAGE">
<text>Generic Property Instrumentation</text>
</message>
<message type="STATUS-MESSAGE">
<text>Running with 8 object bits, 56 offset bits (default)</text>
</message>
<message type="STATUS-MESSAGE">
<text>Starting Bounded Model Checking</text>
</message>
<message type="STATUS-MESSAGE">
<text>Runtime Symex: 0.00473181s</text>
</message>
<message type="STATUS-MESSAGE">
<text>size of program expression: 47 steps</text>
</message>
<message type="STATUS-MESSAGE">
<text>simple slicing removed 5 assignments</text>
</message>
<message type="STATUS-MESSAGE">
<text>Generated 1 VCC(s), 1 remaining after simplification</text>
</message>
<message type="STATUS-MESSAGE">
<text>Runtime Postprocess Equation: 3.13e-05s</text>
</message>
<message type="STATUS-MESSAGE">
<text>Passing problem to propositional reduction</text>
</message>
<message type="STATUS-MESSAGE">
<text>converting SSA</text>
</message>
<message type="STATUS-MESSAGE">
<text>Runtime Convert SSA: 0.0326509s</text>
</message>
<message type="STATUS-MESSAGE">
<text>Running propositional reduction</text>
</message>
<message type="STATUS-MESSAGE">
<text>Post-processing</text>
</message>
<message type="STATUS-MESSAGE">
<text>Runtime Post-process: 0.000163779s</text>
</message>
<message type="STATUS-MESSAGE">
<text>Solving with MiniSAT 2.2.1 with simplifier</text>
</message>
<message type="STATUS-MESSAGE">
<text>4219 variables, 16057 clauses</text>
</message>
<message type="STATUS-MESSAGE">
<text>SAT checker: instance is SATISFIABLE</text>
</message>
<message type="STATUS-MESSAGE">
<text>Runtime Solver: 0.0951822s</text>
</message>
<message type="STATUS-MESSAGE">
<text>Runtime decision procedure: 0.127961s</text>
</message>
<message type="STATUS-MESSAGE">
<text>Building error trace</text>
</message>
<result property="main.assertion.1" status="FAILURE">
<goto_trace>
<function_call hidden="true" step_nr="2" thread="0">
<function display_name="__CPROVER_initialize" identifier="__CPROVER_initialize">
<location file="<built-in-additions>" line="40" working-directory="/home/testData/struct"/>
</function>
</function_call>
<assignment assignment_type="state" base_name="__CPROVER_alloca_object" display_name="__CPROVER_alloca_object" hidden="true" identifier="__CPROVER_alloca_object" mode="C" step_nr="3" thread="0">
<location file="<built-in-additions>" line="20" working-directory="/home/testData/struct"/>
<type>const void *</type>
<full_lhs>__CPROVER_alloca_object</full_lhs>
<full_lhs_value binary="0000000000000000000000000000000000000000000000000000000000000000">NULL</full_lhs_value>
</assignment>
<assignment assignment_type="state" base_name="__CPROVER_dead_object" display_name="__CPROVER_dead_object" hidden="true" identifier="__CPROVER_dead_object" mode="C" step_nr="4" thread="0">
<location file="<built-in-additions>" line="14" working-directory="/home/testData/struct"/>
<type>const void *</type>
<full_lhs>__CPROVER_dead_object</full_lhs>
<full_lhs_value binary="0000000000000000000000000000000000000000000000000000000000000000">NULL</full_lhs_value>
</assignment>
<assignment assignment_type="state" base_name="__CPROVER_deallocated" display_name="__CPROVER_deallocated" hidden="true" identifier="__CPROVER_deallocated" mode="C" step_nr="5" thread="0">
<location file="<built-in-additions>" line="13" working-directory="/home/testData/struct"/>
<type>const void *</type>
<full_lhs>__CPROVER_deallocated</full_lhs>
<full_lhs_value binary="0000000000000000000000000000000000000000000000000000000000000000">NULL</full_lhs_value>
</assignment>
<assignment assignment_type="state" base_name="__CPROVER_malloc_failure_mode_assert_then_assume" display_name="__CPROVER_malloc_failure_mode_assert_then_assume" hidden="true" identifier="__CPROVER_malloc_failure_mode_assert_then_assume" mode="C" step_nr="6" thread="0">
<location file="<built-in-additions>" line="23" working-directory="/home/testData/struct"/>
<type>signed int</type>
<full_lhs>__CPROVER_malloc_failure_mode_assert_then_assume</full_lhs>
<full_lhs_value binary="00000000000000000000000000000010">2</full_lhs_value>
</assignment>
<assignment assignment_type="state" base_name="__CPROVER_malloc_failure_mode_return_null" display_name="__CPROVER_malloc_failure_mode_return_null" hidden="true" identifier="__CPROVER_malloc_failure_mode_return_null" mode="C" step_nr="7" thread="0">
<location file="<built-in-additions>" line="22" working-directory="/home/testData/struct"/>
<type>signed int</type>
<full_lhs>__CPROVER_malloc_failure_mode_return_null</full_lhs>
<full_lhs_value binary="00000000000000000000000000000001">1</full_lhs_value>
</assignment>
<assignment assignment_type="state" base_name="__CPROVER_malloc_is_new_array" display_name="__CPROVER_malloc_is_new_array" hidden="true" identifier="__CPROVER_malloc_is_new_array" mode="C" step_nr="8" thread="0">
<location file="<built-in-additions>" line="17" working-directory="/home/testData/struct"/>
<type>__CPROVER_bool</type>
<full_lhs>__CPROVER_malloc_is_new_array</full_lhs>
<full_lhs_value>FALSE</full_lhs_value>
</assignment>
<assignment assignment_type="state" base_name="__CPROVER_malloc_object" display_name="__CPROVER_malloc_object" hidden="true" identifier="__CPROVER_malloc_object" mode="C" step_nr="9" thread="0">
<location file="<built-in-additions>" line="15" working-directory="/home/testData/struct"/>
<type>const void *</type>
<full_lhs>__CPROVER_malloc_object</full_lhs>
<full_lhs_value binary="0000000000000000000000000000000000000000000000000000000000000000">NULL</full_lhs_value>
</assignment>
<assignment assignment_type="state" base_name="__CPROVER_malloc_size" display_name="__CPROVER_malloc_size" hidden="true" identifier="__CPROVER_malloc_size" mode="C" step_nr="10" thread="0">
<location file="<built-in-additions>" line="16" working-directory="/home/testData/struct"/>
<type>__CPROVER_size_t</type>
<full_lhs>__CPROVER_malloc_size</full_lhs>
<full_lhs_value binary="0000000000000000000000000000000000000000000000000000000000000000">0ul</full_lhs_value>
</assignment>
<assignment assignment_type="state" base_name="__CPROVER_max_malloc_size" display_name="__CPROVER_max_malloc_size" hidden="true" identifier="__CPROVER_max_malloc_size" mode="C" step_nr="11" thread="0">
<location file="<built-in-additions>" line="24" working-directory="/home/testData/struct"/>
<type>__CPROVER_size_t</type>
<full_lhs>__CPROVER_max_malloc_size</full_lhs>
<full_lhs_value binary="0000000010000000000000000000000000000000000000000000000000000000">36028797018963968ul</full_lhs_value>
</assignment>
<assignment assignment_type="state" base_name="__CPROVER_memory_leak" display_name="__CPROVER_memory_leak" hidden="true" identifier="__CPROVER_memory_leak" mode="C" step_nr="12" thread="0">
<location file="<built-in-additions>" line="18" working-directory="/home/testData/struct"/>
<type>const void *</type>
<full_lhs>__CPROVER_memory_leak</full_lhs>
<full_lhs_value binary="0000000000000000000000000000000000000000000000000000000000000000">NULL</full_lhs_value>
</assignment>
<assignment assignment_type="state" base_name="__CPROVER_next_thread_id" display_name="__CPROVER_next_thread_id" hidden="true" identifier="__CPROVER_next_thread_id" mode="C" step_nr="13" thread="0">
<location file="<built-in-additions>" line="8" working-directory="/home/testData/struct"/>
<type>unsigned long int</type>
<full_lhs>__CPROVER_next_thread_id</full_lhs>
<full_lhs_value binary="0000000000000000000000000000000000000000000000000000000000000000">0ul</full_lhs_value>
</assignment>
<assignment assignment_type="state" base_name="__CPROVER_next_thread_key" display_name="__CPROVER_next_thread_key" hidden="true" identifier="__CPROVER_next_thread_key" mode="C" step_nr="14" thread="0">
<location file="<built-in-additions>" line="11" working-directory="/home/testData/struct"/>
<type>unsigned long int</type>
<full_lhs>__CPROVER_next_thread_key</full_lhs>
<full_lhs_value binary="0000000000000000000000000000000000000000000000000000000000000000">0ul</full_lhs_value>
</assignment>
<assignment assignment_type="state" base_name="__CPROVER_pipe_count" display_name="__CPROVER_pipe_count" hidden="true" identifier="__CPROVER_pipe_count" mode="C" step_nr="15" thread="0">
<location file="<built-in-additions>" line="38" working-directory="/home/testData/struct"/>
<type>unsigned int</type>
<full_lhs>__CPROVER_pipe_count</full_lhs>
<full_lhs_value binary="00000000000000000000000000000000">0u</full_lhs_value>
</assignment>
<assignment assignment_type="state" base_name="__CPROVER_rounding_mode" display_name="__CPROVER_rounding_mode" hidden="true" identifier="__CPROVER_rounding_mode" mode="C" step_nr="16" thread="0">
<location file="<built-in-additions>" line="29" working-directory="/home/testData/struct"/>
<type>signed int</type>
<full_lhs>__CPROVER_rounding_mode</full_lhs>
<full_lhs_value binary="00000000000000000000000000000000">0</full_lhs_value>
</assignment>
<assignment assignment_type="state" base_name="__CPROVER_thread_id" display_name="__CPROVER_thread_id" hidden="true" identifier="__CPROVER_thread_id" mode="C" step_nr="17" thread="0">
<location file="<built-in-additions>" line="6" working-directory="/home/testData/struct"/>
<type>unsigned long int</type>
<full_lhs>__CPROVER_thread_id</full_lhs>
<full_lhs_value binary="0000000000000000000000000000000000000000000000000000000000000000">0ul</full_lhs_value>
</assignment>
<assignment assignment_type="state" base_name="__CPROVER_thread_key_dtors" display_name="__CPROVER_thread_key_dtors" hidden="true" identifier="__CPROVER_thread_key_dtors" mode="C" step_nr="18" thread="0">
<location file="<built-in-additions>" line="10" working-directory="/home/testData/struct"/>
<type>void (*[INFINITY()])(void *)</type>
<full_lhs>__CPROVER_thread_key_dtors</full_lhs>
<full_lhs_value>__CPROVER_thread_key_dtors!0#1</full_lhs_value>
</assignment>
<assignment assignment_type="state" base_name="__CPROVER_thread_keys" display_name="__CPROVER_thread_keys" hidden="true" identifier="__CPROVER_thread_keys" mode="C" step_nr="19" thread="0">
<location file="<built-in-additions>" line="9" working-directory="/home/testData/struct"/>
<type>const void *[INFINITY()]</type>
<full_lhs>__CPROVER_thread_keys</full_lhs>
<full_lhs_value>__CPROVER_thread_keys!0#1</full_lhs_value>
</assignment>
<assignment assignment_type="state" base_name="__CPROVER_threads_exited" display_name="__CPROVER_threads_exited" hidden="true" identifier="__CPROVER_threads_exited" mode="C" step_nr="20" thread="0">
<location file="<built-in-additions>" line="7" working-directory="/home/testData/struct"/>
<type>__CPROVER_bool [INFINITY()]</type>
<full_lhs>__CPROVER_threads_exited</full_lhs>
<full_lhs_value>__CPROVER_threads_exited#1</full_lhs_value>
</assignment>
<function_return hidden="true" step_nr="21" thread="0">
<function display_name="__CPROVER_initialize" identifier="__CPROVER_initialize">
<location file="<built-in-additions>" line="40" working-directory="/home/testData/struct"/>
</function>
</function_return>
<location-only hidden="false" step_nr="22" thread="0">
<location file="struct.c" line="10" working-directory="/home/testData/struct"/>
</location-only>
<function_call hidden="false" step_nr="23" thread="0">
<function display_name="main" identifier="main">
<location file="struct.c" line="10" working-directory="/home/testData/struct"/>
</function>
<location file="struct.c" line="10" working-directory="/home/testData/struct"/>
</function_call>
<assignment assignment_type="state" base_name="q" display_name="main::1::q" hidden="false" identifier="main::1::q" mode="C" step_nr="24" thread="0">
<location file="struct.c" function="main" line="12" working-directory="/home/testData/struct"/>
<type>signed int</type>
<full_lhs>q</full_lhs>
<full_lhs_value binary="00000000000000000000000000000000">0</full_lhs_value>
</assignment>
<assignment assignment_type="state" base_name="s" display_name="main::1::s" hidden="false" identifier="main::1::s" mode="C" step_nr="25" thread="0">
<location file="struct.c" function="main" line="13" working-directory="/home/testData/struct"/>
<type>struct str</type>
<full_lhs>s</full_lhs>
<full_lhs_value>{ .x=s!0@1#1..x, .y=s!0@1#1..y, .$pad2=s!0@1#1..$pad2, .z=s!0@1#1..z }</full_lhs_value>
</assignment>
<assignment assignment_type="state" base_name="s" display_name="main::1::s" hidden="false" identifier="main::1::s" mode="C" step_nr="26" thread="0">
<location file="struct.c" function="main" line="15" working-directory="/home/testData/struct"/>
<type>struct str</type>
<full_lhs>s.x</full_lhs>
<full_lhs_value binary="00000000000000000000000000000000">0.0f</full_lhs_value>
</assignment>
<assignment assignment_type="state" base_name="s" display_name="main::1::s" hidden="false" identifier="main::1::s" mode="C" step_nr="27" thread="0">
<location file="struct.c" function="main" line="16" working-directory="/home/testData/struct"/>
<type>struct str</type>
<full_lhs>s.y</full_lhs>
<full_lhs_value binary="0000000000000001">1</full_lhs_value>
</assignment>
<assignment assignment_type="state" base_name="s" display_name="main::1::s" hidden="false" identifier="main::1::s" mode="C" step_nr="28" thread="0">
<location file="struct.c" function="main" line="17" working-directory="/hometestData/struct"/>
<type>struct str</type>
<full_lhs>s.z</full_lhs>
<full_lhs_value binary="00000000000000000000000000000001">1</full_lhs_value>
</assignment>
<failure hidden="false" property="main.assertion.1" reason="assertion q == s.z" step_nr="29" thread="0">
<location file="struct.c" function="main" line="19" working-directory="/home/testData/struct"/>
</failure>
</goto_trace>
</result>
<message type="STATUS-MESSAGE">
<text>VERIFICATION FAILED</text>
</message>
<cprover-status>FAILURE</cprover-status>
</cprover>I am expecting that the type of s.x s.y s.z is not marked as struct str but as the type of the child, in my example
float, short and int respectively
Any ideas?
Thanks