-
-
Save jkbbwr/d22fc3efcc01ffc4cd0a671fbdef904c to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| <?xml version="1.0" encoding="UTF-8"?> | |
| <cprover> | |
| <program>CBMC 5.11 (cbmc-5.11)</program> | |
| <message type="STATUS-MESSAGE"> | |
| <text>CBMC version 5.11 (cbmc-5.11) 64-bit x86_64 linux</text> | |
| </message> | |
| <message type="STATUS-MESSAGE"> | |
| <text>Reading GOTO program from file</text> | |
| </message> | |
| <message type="STATUS-MESSAGE"> | |
| <text>Reading: main.goto</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>Rewriting existing assertions as assumptions</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>size of program expression: 65 steps</text> | |
| </message> | |
| <message type="STATUS-MESSAGE"> | |
| <text>Generated 2 VCC(s), 2 remaining after simplification</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>Aiming to cover 2 goal(s)</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>Solving with MiniSAT 2.2.1 with simplifier</text> | |
| </message> | |
| <message type="STATUS-MESSAGE"> | |
| <text>333 variables, 141 clauses</text> | |
| </message> | |
| <message type="STATUS-MESSAGE"> | |
| <text>SAT checker: instance is SATISFIABLE</text> | |
| </message> | |
| <message type="STATUS-MESSAGE"> | |
| <text>Covered function main block 1</text> | |
| </message> | |
| <message type="STATUS-MESSAGE"> | |
| <text>Covered function main block 2</text> | |
| </message> | |
| <message type="STATUS-MESSAGE"> | |
| <text>Runtime decision procedure: 0.000766299s</text> | |
| </message> | |
| <goal description="block 1" id="main.coverage.1" status="SATISFIED"> | |
| <location file="main.c" function="main" line="6" working-directory="/home/jakob/tmp"/> | |
| </goal> | |
| <goal description="block 2" id="main.coverage.2" status="SATISFIED"> | |
| <location file="main.c" function="main" line="6" working-directory="/home/jakob/tmp"/> | |
| </goal> | |
| <test> | |
| <inputs/> | |
| <goal id="main.coverage.1"/> | |
| <goal id="main.coverage.2"/> | |
| </test> | |
| <message type="STATUS-MESSAGE"> | |
| <text>** 2 of 2 covered (100.0%)</text> | |
| </message> | |
| <message type="STATUS-MESSAGE"> | |
| <text>** Used 1 iteration</text> | |
| </message> | |
| </cprover> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| <?xml version="1.0" encoding="UTF-8"?> | |
| <cprover> | |
| <program>CBMC 5.11 (cbmc-5.11)</program> | |
| <message type="STATUS-MESSAGE"> | |
| <text>CBMC version 5.11 (cbmc-5.11) 64-bit x86_64 linux</text> | |
| </message> | |
| <message type="STATUS-MESSAGE"> | |
| <text>Reading GOTO program from file</text> | |
| </message> | |
| <message type="STATUS-MESSAGE"> | |
| <text>Reading: main.goto</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> | |
| <property class="assertion" name="main.assertion.1"> | |
| <location file="main.c" function="main" line="8" working-directory="/home/jakob/tmp"/> | |
| <description>assertion global > 0</description> | |
| <expression>global > 0</expression> | |
| </property> | |
| <property class="assertion" name="main.assertion.2"> | |
| <location file="main.c" function="main" line="9" working-directory="/home/jakob/tmp"/> | |
| <description>assertion *ptr > 0</description> | |
| <expression>*ptr > 0</expression> | |
| </property> | |
| </cprover> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| <?xml version="1.0" encoding="UTF-8"?> | |
| <cprover> | |
| <program>CBMC 5.11 (cbmc-5.11)</program> | |
| <message type="STATUS-MESSAGE"> | |
| <text>CBMC version 5.11 (cbmc-5.11) 64-bit x86_64 linux</text> | |
| </message> | |
| <message type="STATUS-MESSAGE"> | |
| <text>Reading GOTO program from file</text> | |
| </message> | |
| <message type="STATUS-MESSAGE"> | |
| <text>Reading: main.goto</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>size of program expression: 63 steps</text> | |
| </message> | |
| <message type="STATUS-MESSAGE"> | |
| <text>simple slicing removed 5 assignments</text> | |
| </message> | |
| <message type="STATUS-MESSAGE"> | |
| <text>Generated 2 VCC(s), 2 remaining after simplification</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>Running propositional reduction</text> | |
| </message> | |
| <message type="STATUS-MESSAGE"> | |
| <text>Post-processing</text> | |
| </message> | |
| <message type="STATUS-MESSAGE"> | |
| <text>Solving with MiniSAT 2.2.1 with simplifier</text> | |
| </message> | |
| <message type="STATUS-MESSAGE"> | |
| <text>333 variables, 141 clauses</text> | |
| </message> | |
| <message type="STATUS-MESSAGE"> | |
| <text>SAT checker: instance is SATISFIABLE</text> | |
| </message> | |
| <message type="STATUS-MESSAGE"> | |
| <text>Runtime decision procedure: 0.000961716s</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="31" working-directory="/home/jakob/tmp"/> | |
| </function> | |
| </function_call> | |
| <assignment assignment_type="state" base_name="__CPROVER_dead_object" display_name="__CPROVER_dead_object" hidden="true" identifier="__CPROVER_dead_object" mode="C" step_nr="3" thread="0"> | |
| <location file="<built-in-additions>" line="11" working-directory="/home/jakob/tmp"/> | |
| <type>const void *</type> | |
| <full_lhs>__CPROVER_dead_object</full_lhs> | |
| <full_lhs_value>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="4" thread="0"> | |
| <location file="<built-in-additions>" line="10" working-directory="/home/jakob/tmp"/> | |
| <type>const void *</type> | |
| <full_lhs>__CPROVER_deallocated</full_lhs> | |
| <full_lhs_value>NULL</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="5" thread="0"> | |
| <location file="<built-in-additions>" line="14" working-directory="/home/jakob/tmp"/> | |
| <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="6" thread="0"> | |
| <location file="<built-in-additions>" line="12" working-directory="/home/jakob/tmp"/> | |
| <type>const void *</type> | |
| <full_lhs>__CPROVER_malloc_object</full_lhs> | |
| <full_lhs_value>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="7" thread="0"> | |
| <location file="<built-in-additions>" line="13" working-directory="/home/jakob/tmp"/> | |
| <type>__CPROVER_size_t</type> | |
| <full_lhs>__CPROVER_malloc_size</full_lhs> | |
| <full_lhs_value>0ul</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="8" thread="0"> | |
| <location file="<built-in-additions>" line="15" working-directory="/home/jakob/tmp"/> | |
| <type>const void *</type> | |
| <full_lhs>__CPROVER_memory_leak</full_lhs> | |
| <full_lhs_value>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="9" thread="0"> | |
| <location file="<built-in-additions>" line="8" working-directory="/home/jakob/tmp"/> | |
| <type>unsigned long int</type> | |
| <full_lhs>__CPROVER_next_thread_id</full_lhs> | |
| <full_lhs_value>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="10" thread="0"> | |
| <location file="<built-in-additions>" line="29" working-directory="/home/jakob/tmp"/> | |
| <type>unsigned int</type> | |
| <full_lhs>__CPROVER_pipe_count</full_lhs> | |
| <full_lhs_value>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="11" thread="0"> | |
| <location file="<built-in-additions>" line="20" working-directory="/home/jakob/tmp"/> | |
| <type>signed int</type> | |
| <full_lhs>__CPROVER_rounding_mode</full_lhs> | |
| <full_lhs_value>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="12" thread="0"> | |
| <location file="<built-in-additions>" line="6" working-directory="/home/jakob/tmp"/> | |
| <type>unsigned long int</type> | |
| <full_lhs>__CPROVER_thread_id</full_lhs> | |
| <full_lhs_value>0ul</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="13" thread="0"> | |
| <location file="<built-in-additions>" line="7" working-directory="/home/jakob/tmp"/> | |
| <type>__CPROVER_bool [INFINITY()]</type> | |
| <full_lhs>__CPROVER_threads_exited</full_lhs> | |
| <full_lhs_value>__CPROVER_threads_exited#1</full_lhs_value> | |
| </assignment> | |
| <assignment assignment_type="state" base_name="global" display_name="global" hidden="true" identifier="global" mode="C" step_nr="14" thread="0"> | |
| <location file="main.c" line="3" working-directory="/home/jakob/tmp"/> | |
| <type>signed int</type> | |
| <full_lhs>global</full_lhs> | |
| <full_lhs_value>0</full_lhs_value> | |
| </assignment> | |
| <function_return hidden="true" step_nr="15" thread="0"> | |
| <function display_name="__CPROVER_initialize" identifier="__CPROVER_initialize"> | |
| <location file="<built-in-additions>" line="31" working-directory="/home/jakob/tmp"/> | |
| </function> | |
| </function_return> | |
| <location-only hidden="false" step_nr="16" thread="0"> | |
| <location file="main.c" line="5" working-directory="/home/jakob/tmp"/> | |
| </location-only> | |
| <function_call hidden="false" step_nr="17" thread="0"> | |
| <function display_name="main" identifier="main"> | |
| <location file="main.c" line="5" working-directory="/home/jakob/tmp"/> | |
| </function> | |
| <location file="main.c" line="5" working-directory="/home/jakob/tmp"/> | |
| </function_call> | |
| <assignment assignment_type="state" base_name="ptr" display_name="main::1::ptr" hidden="false" identifier="main::1::ptr" mode="C" step_nr="18" thread="0"> | |
| <location file="main.c" function="main" line="6" working-directory="/home/jakob/tmp"/> | |
| <type>signed int *</type> | |
| <full_lhs>ptr</full_lhs> | |
| <full_lhs_value>((signed int *)NULL)</full_lhs_value> | |
| </assignment> | |
| <assignment assignment_type="state" base_name="return_value_malloc" display_name="main::$tmp::return_value_malloc" hidden="true" identifier="main::$tmp::return_value_malloc" mode="C" step_nr="19" thread="0"> | |
| <location file="main.c" function="main" line="6" working-directory="/home/jakob/tmp"/> | |
| <type>void *</type> | |
| <full_lhs>return_value_malloc</full_lhs> | |
| <full_lhs_value>NULL</full_lhs_value> | |
| </assignment> | |
| <function_call hidden="false" step_nr="21" thread="0"> | |
| <function display_name="malloc" identifier="malloc"> | |
| <location file="<builtin-library-malloc>" line="6" working-directory="/home/jakob/tmp"/> | |
| </function> | |
| <location file="main.c" function="main" line="6" working-directory="/home/jakob/tmp"/> | |
| </function_call> | |
| <assignment assignment_type="actual_parameter" base_name="malloc_size" display_name="malloc::malloc_size" hidden="false" identifier="malloc::malloc_size" mode="C" step_nr="22" thread="0"> | |
| <location file="main.c" function="main" line="6" working-directory="/home/jakob/tmp"/> | |
| <type>__CPROVER_size_t</type> | |
| <full_lhs>malloc_size</full_lhs> | |
| <full_lhs_value>4ul</full_lhs_value> | |
| </assignment> | |
| <assignment assignment_type="state" base_name="malloc_res" display_name="malloc::1::malloc_res" hidden="true" identifier="malloc::1::malloc_res" mode="C" step_nr="23" thread="0"> | |
| <location file="<builtin-library-malloc>" function="malloc" line="11" working-directory="/home/jakob/tmp"/> | |
| <type>void *</type> | |
| <full_lhs>malloc_res</full_lhs> | |
| <full_lhs_value>NULL</full_lhs_value> | |
| </assignment> | |
| <assignment assignment_type="state" base_name="malloc_value" display_name="malloc::$tmp::malloc_value" hidden="true" identifier="malloc::$tmp::malloc_value" mode="C" step_nr="24" thread="0"> | |
| <location file="<builtin-library-malloc>" function="malloc" line="12" working-directory="/home/jakob/tmp"/> | |
| <type>void *</type> | |
| <full_lhs>malloc_value</full_lhs> | |
| <full_lhs_value>NULL</full_lhs_value> | |
| </assignment> | |
| <assignment assignment_type="state" base_name="dynamic_object1" display_name="symex_dynamic::dynamic_object1" hidden="true" identifier="symex_dynamic::dynamic_object1" mode="C" step_nr="25" thread="0"> | |
| <location file="<builtin-library-malloc>" function="malloc" line="12" working-directory="/home/jakob/tmp"/> | |
| <type>signed int</type> | |
| <full_lhs>dynamic_object1</full_lhs> | |
| <full_lhs_value>-2147483648</full_lhs_value> | |
| </assignment> | |
| <assignment assignment_type="state" base_name="malloc_value" display_name="malloc::$tmp::malloc_value" hidden="true" identifier="malloc::$tmp::malloc_value" mode="C" step_nr="26" thread="0"> | |
| <location file="<builtin-library-malloc>" function="malloc" line="12" working-directory="/home/jakob/tmp"/> | |
| <type>void *</type> | |
| <full_lhs>malloc_value</full_lhs> | |
| <full_lhs_value>(const void *)&dynamic_object1</full_lhs_value> | |
| </assignment> | |
| <assignment assignment_type="state" base_name="malloc_res" display_name="malloc::1::malloc_res" hidden="true" identifier="malloc::1::malloc_res" mode="C" step_nr="27" thread="0"> | |
| <location file="<builtin-library-malloc>" function="malloc" line="12" working-directory="/home/jakob/tmp"/> | |
| <type>void *</type> | |
| <full_lhs>malloc_res</full_lhs> | |
| <full_lhs_value>(const void *)&dynamic_object1</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="28" thread="0"> | |
| <location file="<builtin-library-malloc>" function="malloc" line="15" working-directory="/home/jakob/tmp"/> | |
| <type>const void *</type> | |
| <full_lhs>__CPROVER_deallocated</full_lhs> | |
| <full_lhs_value>NULL</full_lhs_value> | |
| </assignment> | |
| <assignment assignment_type="state" base_name="record_malloc" display_name="malloc::1::record_malloc" hidden="true" identifier="malloc::1::record_malloc" mode="C" step_nr="29" thread="0"> | |
| <location file="<builtin-library-malloc>" function="malloc" line="18" working-directory="/home/jakob/tmp"/> | |
| <type>__CPROVER_bool</type> | |
| <full_lhs>record_malloc</full_lhs> | |
| <full_lhs_value>FALSE</full_lhs_value> | |
| </assignment> | |
| <assignment assignment_type="state" base_name="record_malloc" display_name="malloc::1::record_malloc" hidden="true" identifier="malloc::1::record_malloc" mode="C" step_nr="30" thread="0"> | |
| <location file="<builtin-library-malloc>" function="malloc" line="18" working-directory="/home/jakob/tmp"/> | |
| <type>__CPROVER_bool</type> | |
| <full_lhs>record_malloc</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="31" thread="0"> | |
| <location file="<builtin-library-malloc>" function="malloc" line="19" working-directory="/home/jakob/tmp"/> | |
| <type>const void *</type> | |
| <full_lhs>__CPROVER_malloc_object</full_lhs> | |
| <full_lhs_value>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="32" thread="0"> | |
| <location file="<builtin-library-malloc>" function="malloc" line="20" working-directory="/home/jakob/tmp"/> | |
| <type>__CPROVER_size_t</type> | |
| <full_lhs>__CPROVER_malloc_size</full_lhs> | |
| <full_lhs_value>0ul</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="33" thread="0"> | |
| <location file="<builtin-library-malloc>" function="malloc" line="21" working-directory="/home/jakob/tmp"/> | |
| <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="record_may_leak" display_name="malloc::1::record_may_leak" hidden="true" identifier="malloc::1::record_may_leak" mode="C" step_nr="34" thread="0"> | |
| <location file="<builtin-library-malloc>" function="malloc" line="24" working-directory="/home/jakob/tmp"/> | |
| <type>__CPROVER_bool</type> | |
| <full_lhs>record_may_leak</full_lhs> | |
| <full_lhs_value>FALSE</full_lhs_value> | |
| </assignment> | |
| <assignment assignment_type="state" base_name="record_may_leak" display_name="malloc::1::record_may_leak" hidden="true" identifier="malloc::1::record_may_leak" mode="C" step_nr="35" thread="0"> | |
| <location file="<builtin-library-malloc>" function="malloc" line="24" working-directory="/home/jakob/tmp"/> | |
| <type>__CPROVER_bool</type> | |
| <full_lhs>record_may_leak</full_lhs> | |
| <full_lhs_value>FALSE</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="36" thread="0"> | |
| <location file="<builtin-library-malloc>" function="malloc" line="25" working-directory="/home/jakob/tmp"/> | |
| <type>const void *</type> | |
| <full_lhs>__CPROVER_memory_leak</full_lhs> | |
| <full_lhs_value>NULL</full_lhs_value> | |
| </assignment> | |
| <assignment assignment_type="state" base_name="malloc#return_value" display_name="malloc#return_value" hidden="true" identifier="malloc#return_value" mode="C" step_nr="37" thread="0"> | |
| <location file="<builtin-library-malloc>" function="malloc" line="27" working-directory="/home/jakob/tmp"/> | |
| <type>void *</type> | |
| <full_lhs>malloc#return_value</full_lhs> | |
| <full_lhs_value>(const void *)&dynamic_object1</full_lhs_value> | |
| </assignment> | |
| <function_return hidden="true" step_nr="38" thread="0"> | |
| <function display_name="malloc" identifier="malloc"> | |
| <location file="<builtin-library-malloc>" line="6" working-directory="/home/jakob/tmp"/> | |
| </function> | |
| <location file="<builtin-library-malloc>" function="malloc" line="28" working-directory="/home/jakob/tmp"/> | |
| </function_return> | |
| <assignment assignment_type="state" base_name="return_value_malloc" display_name="main::$tmp::return_value_malloc" hidden="true" identifier="main::$tmp::return_value_malloc" mode="C" step_nr="39" thread="0"> | |
| <location file="main.c" function="main" line="6" working-directory="/home/jakob/tmp"/> | |
| <type>void *</type> | |
| <full_lhs>return_value_malloc</full_lhs> | |
| <full_lhs_value>(const void *)&dynamic_object1</full_lhs_value> | |
| </assignment> | |
| <assignment assignment_type="state" base_name="ptr" display_name="main::1::ptr" hidden="false" identifier="main::1::ptr" mode="C" step_nr="40" thread="0"> | |
| <location file="main.c" function="main" line="6" working-directory="/home/jakob/tmp"/> | |
| <type>signed int *</type> | |
| <full_lhs>ptr</full_lhs> | |
| <full_lhs_value>&dynamic_object1</full_lhs_value> | |
| </assignment> | |
| <failure hidden="false" property="main.assertion.1" reason="assertion global > 0" step_nr="41" thread="0"> | |
| <location file="main.c" function="main" line="8" working-directory="/home/jakob/tmp"/> | |
| </failure> | |
| </goto_trace> | |
| </result> | |
| <result property="main.assertion.2" 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="31" working-directory="/home/jakob/tmp"/> | |
| </function> | |
| </function_call> | |
| <assignment assignment_type="state" base_name="__CPROVER_dead_object" display_name="__CPROVER_dead_object" hidden="true" identifier="__CPROVER_dead_object" mode="C" step_nr="3" thread="0"> | |
| <location file="<built-in-additions>" line="11" working-directory="/home/jakob/tmp"/> | |
| <type>const void *</type> | |
| <full_lhs>__CPROVER_dead_object</full_lhs> | |
| <full_lhs_value>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="4" thread="0"> | |
| <location file="<built-in-additions>" line="10" working-directory="/home/jakob/tmp"/> | |
| <type>const void *</type> | |
| <full_lhs>__CPROVER_deallocated</full_lhs> | |
| <full_lhs_value>NULL</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="5" thread="0"> | |
| <location file="<built-in-additions>" line="14" working-directory="/home/jakob/tmp"/> | |
| <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="6" thread="0"> | |
| <location file="<built-in-additions>" line="12" working-directory="/home/jakob/tmp"/> | |
| <type>const void *</type> | |
| <full_lhs>__CPROVER_malloc_object</full_lhs> | |
| <full_lhs_value>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="7" thread="0"> | |
| <location file="<built-in-additions>" line="13" working-directory="/home/jakob/tmp"/> | |
| <type>__CPROVER_size_t</type> | |
| <full_lhs>__CPROVER_malloc_size</full_lhs> | |
| <full_lhs_value>0ul</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="8" thread="0"> | |
| <location file="<built-in-additions>" line="15" working-directory="/home/jakob/tmp"/> | |
| <type>const void *</type> | |
| <full_lhs>__CPROVER_memory_leak</full_lhs> | |
| <full_lhs_value>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="9" thread="0"> | |
| <location file="<built-in-additions>" line="8" working-directory="/home/jakob/tmp"/> | |
| <type>unsigned long int</type> | |
| <full_lhs>__CPROVER_next_thread_id</full_lhs> | |
| <full_lhs_value>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="10" thread="0"> | |
| <location file="<built-in-additions>" line="29" working-directory="/home/jakob/tmp"/> | |
| <type>unsigned int</type> | |
| <full_lhs>__CPROVER_pipe_count</full_lhs> | |
| <full_lhs_value>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="11" thread="0"> | |
| <location file="<built-in-additions>" line="20" working-directory="/home/jakob/tmp"/> | |
| <type>signed int</type> | |
| <full_lhs>__CPROVER_rounding_mode</full_lhs> | |
| <full_lhs_value>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="12" thread="0"> | |
| <location file="<built-in-additions>" line="6" working-directory="/home/jakob/tmp"/> | |
| <type>unsigned long int</type> | |
| <full_lhs>__CPROVER_thread_id</full_lhs> | |
| <full_lhs_value>0ul</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="13" thread="0"> | |
| <location file="<built-in-additions>" line="7" working-directory="/home/jakob/tmp"/> | |
| <type>__CPROVER_bool [INFINITY()]</type> | |
| <full_lhs>__CPROVER_threads_exited</full_lhs> | |
| <full_lhs_value>__CPROVER_threads_exited#1</full_lhs_value> | |
| </assignment> | |
| <assignment assignment_type="state" base_name="global" display_name="global" hidden="true" identifier="global" mode="C" step_nr="14" thread="0"> | |
| <location file="main.c" line="3" working-directory="/home/jakob/tmp"/> | |
| <type>signed int</type> | |
| <full_lhs>global</full_lhs> | |
| <full_lhs_value>0</full_lhs_value> | |
| </assignment> | |
| <function_return hidden="true" step_nr="15" thread="0"> | |
| <function display_name="__CPROVER_initialize" identifier="__CPROVER_initialize"> | |
| <location file="<built-in-additions>" line="31" working-directory="/home/jakob/tmp"/> | |
| </function> | |
| </function_return> | |
| <location-only hidden="false" step_nr="16" thread="0"> | |
| <location file="main.c" line="5" working-directory="/home/jakob/tmp"/> | |
| </location-only> | |
| <function_call hidden="false" step_nr="17" thread="0"> | |
| <function display_name="main" identifier="main"> | |
| <location file="main.c" line="5" working-directory="/home/jakob/tmp"/> | |
| </function> | |
| <location file="main.c" line="5" working-directory="/home/jakob/tmp"/> | |
| </function_call> | |
| <assignment assignment_type="state" base_name="ptr" display_name="main::1::ptr" hidden="false" identifier="main::1::ptr" mode="C" step_nr="18" thread="0"> | |
| <location file="main.c" function="main" line="6" working-directory="/home/jakob/tmp"/> | |
| <type>signed int *</type> | |
| <full_lhs>ptr</full_lhs> | |
| <full_lhs_value>((signed int *)NULL)</full_lhs_value> | |
| </assignment> | |
| <assignment assignment_type="state" base_name="return_value_malloc" display_name="main::$tmp::return_value_malloc" hidden="true" identifier="main::$tmp::return_value_malloc" mode="C" step_nr="19" thread="0"> | |
| <location file="main.c" function="main" line="6" working-directory="/home/jakob/tmp"/> | |
| <type>void *</type> | |
| <full_lhs>return_value_malloc</full_lhs> | |
| <full_lhs_value>NULL</full_lhs_value> | |
| </assignment> | |
| <function_call hidden="false" step_nr="21" thread="0"> | |
| <function display_name="malloc" identifier="malloc"> | |
| <location file="<builtin-library-malloc>" line="6" working-directory="/home/jakob/tmp"/> | |
| </function> | |
| <location file="main.c" function="main" line="6" working-directory="/home/jakob/tmp"/> | |
| </function_call> | |
| <assignment assignment_type="actual_parameter" base_name="malloc_size" display_name="malloc::malloc_size" hidden="false" identifier="malloc::malloc_size" mode="C" step_nr="22" thread="0"> | |
| <location file="main.c" function="main" line="6" working-directory="/home/jakob/tmp"/> | |
| <type>__CPROVER_size_t</type> | |
| <full_lhs>malloc_size</full_lhs> | |
| <full_lhs_value>4ul</full_lhs_value> | |
| </assignment> | |
| <assignment assignment_type="state" base_name="malloc_res" display_name="malloc::1::malloc_res" hidden="true" identifier="malloc::1::malloc_res" mode="C" step_nr="23" thread="0"> | |
| <location file="<builtin-library-malloc>" function="malloc" line="11" working-directory="/home/jakob/tmp"/> | |
| <type>void *</type> | |
| <full_lhs>malloc_res</full_lhs> | |
| <full_lhs_value>NULL</full_lhs_value> | |
| </assignment> | |
| <assignment assignment_type="state" base_name="malloc_value" display_name="malloc::$tmp::malloc_value" hidden="true" identifier="malloc::$tmp::malloc_value" mode="C" step_nr="24" thread="0"> | |
| <location file="<builtin-library-malloc>" function="malloc" line="12" working-directory="/home/jakob/tmp"/> | |
| <type>void *</type> | |
| <full_lhs>malloc_value</full_lhs> | |
| <full_lhs_value>NULL</full_lhs_value> | |
| </assignment> | |
| <assignment assignment_type="state" base_name="dynamic_object1" display_name="symex_dynamic::dynamic_object1" hidden="true" identifier="symex_dynamic::dynamic_object1" mode="C" step_nr="25" thread="0"> | |
| <location file="<builtin-library-malloc>" function="malloc" line="12" working-directory="/home/jakob/tmp"/> | |
| <type>signed int</type> | |
| <full_lhs>dynamic_object1</full_lhs> | |
| <full_lhs_value>-2147483648</full_lhs_value> | |
| </assignment> | |
| <assignment assignment_type="state" base_name="malloc_value" display_name="malloc::$tmp::malloc_value" hidden="true" identifier="malloc::$tmp::malloc_value" mode="C" step_nr="26" thread="0"> | |
| <location file="<builtin-library-malloc>" function="malloc" line="12" working-directory="/home/jakob/tmp"/> | |
| <type>void *</type> | |
| <full_lhs>malloc_value</full_lhs> | |
| <full_lhs_value>(const void *)&dynamic_object1</full_lhs_value> | |
| </assignment> | |
| <assignment assignment_type="state" base_name="malloc_res" display_name="malloc::1::malloc_res" hidden="true" identifier="malloc::1::malloc_res" mode="C" step_nr="27" thread="0"> | |
| <location file="<builtin-library-malloc>" function="malloc" line="12" working-directory="/home/jakob/tmp"/> | |
| <type>void *</type> | |
| <full_lhs>malloc_res</full_lhs> | |
| <full_lhs_value>(const void *)&dynamic_object1</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="28" thread="0"> | |
| <location file="<builtin-library-malloc>" function="malloc" line="15" working-directory="/home/jakob/tmp"/> | |
| <type>const void *</type> | |
| <full_lhs>__CPROVER_deallocated</full_lhs> | |
| <full_lhs_value>NULL</full_lhs_value> | |
| </assignment> | |
| <assignment assignment_type="state" base_name="record_malloc" display_name="malloc::1::record_malloc" hidden="true" identifier="malloc::1::record_malloc" mode="C" step_nr="29" thread="0"> | |
| <location file="<builtin-library-malloc>" function="malloc" line="18" working-directory="/home/jakob/tmp"/> | |
| <type>__CPROVER_bool</type> | |
| <full_lhs>record_malloc</full_lhs> | |
| <full_lhs_value>FALSE</full_lhs_value> | |
| </assignment> | |
| <assignment assignment_type="state" base_name="record_malloc" display_name="malloc::1::record_malloc" hidden="true" identifier="malloc::1::record_malloc" mode="C" step_nr="30" thread="0"> | |
| <location file="<builtin-library-malloc>" function="malloc" line="18" working-directory="/home/jakob/tmp"/> | |
| <type>__CPROVER_bool</type> | |
| <full_lhs>record_malloc</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="31" thread="0"> | |
| <location file="<builtin-library-malloc>" function="malloc" line="19" working-directory="/home/jakob/tmp"/> | |
| <type>const void *</type> | |
| <full_lhs>__CPROVER_malloc_object</full_lhs> | |
| <full_lhs_value>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="32" thread="0"> | |
| <location file="<builtin-library-malloc>" function="malloc" line="20" working-directory="/home/jakob/tmp"/> | |
| <type>__CPROVER_size_t</type> | |
| <full_lhs>__CPROVER_malloc_size</full_lhs> | |
| <full_lhs_value>0ul</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="33" thread="0"> | |
| <location file="<builtin-library-malloc>" function="malloc" line="21" working-directory="/home/jakob/tmp"/> | |
| <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="record_may_leak" display_name="malloc::1::record_may_leak" hidden="true" identifier="malloc::1::record_may_leak" mode="C" step_nr="34" thread="0"> | |
| <location file="<builtin-library-malloc>" function="malloc" line="24" working-directory="/home/jakob/tmp"/> | |
| <type>__CPROVER_bool</type> | |
| <full_lhs>record_may_leak</full_lhs> | |
| <full_lhs_value>FALSE</full_lhs_value> | |
| </assignment> | |
| <assignment assignment_type="state" base_name="record_may_leak" display_name="malloc::1::record_may_leak" hidden="true" identifier="malloc::1::record_may_leak" mode="C" step_nr="35" thread="0"> | |
| <location file="<builtin-library-malloc>" function="malloc" line="24" working-directory="/home/jakob/tmp"/> | |
| <type>__CPROVER_bool</type> | |
| <full_lhs>record_may_leak</full_lhs> | |
| <full_lhs_value>FALSE</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="36" thread="0"> | |
| <location file="<builtin-library-malloc>" function="malloc" line="25" working-directory="/home/jakob/tmp"/> | |
| <type>const void *</type> | |
| <full_lhs>__CPROVER_memory_leak</full_lhs> | |
| <full_lhs_value>NULL</full_lhs_value> | |
| </assignment> | |
| <assignment assignment_type="state" base_name="malloc#return_value" display_name="malloc#return_value" hidden="true" identifier="malloc#return_value" mode="C" step_nr="37" thread="0"> | |
| <location file="<builtin-library-malloc>" function="malloc" line="27" working-directory="/home/jakob/tmp"/> | |
| <type>void *</type> | |
| <full_lhs>malloc#return_value</full_lhs> | |
| <full_lhs_value>(const void *)&dynamic_object1</full_lhs_value> | |
| </assignment> | |
| <function_return hidden="true" step_nr="38" thread="0"> | |
| <function display_name="malloc" identifier="malloc"> | |
| <location file="<builtin-library-malloc>" line="6" working-directory="/home/jakob/tmp"/> | |
| </function> | |
| <location file="<builtin-library-malloc>" function="malloc" line="28" working-directory="/home/jakob/tmp"/> | |
| </function_return> | |
| <assignment assignment_type="state" base_name="return_value_malloc" display_name="main::$tmp::return_value_malloc" hidden="true" identifier="main::$tmp::return_value_malloc" mode="C" step_nr="39" thread="0"> | |
| <location file="main.c" function="main" line="6" working-directory="/home/jakob/tmp"/> | |
| <type>void *</type> | |
| <full_lhs>return_value_malloc</full_lhs> | |
| <full_lhs_value>(const void *)&dynamic_object1</full_lhs_value> | |
| </assignment> | |
| <assignment assignment_type="state" base_name="ptr" display_name="main::1::ptr" hidden="false" identifier="main::1::ptr" mode="C" step_nr="40" thread="0"> | |
| <location file="main.c" function="main" line="6" working-directory="/home/jakob/tmp"/> | |
| <type>signed int *</type> | |
| <full_lhs>ptr</full_lhs> | |
| <full_lhs_value>&dynamic_object1</full_lhs_value> | |
| </assignment> | |
| <failure hidden="false" property="main.assertion.1" reason="assertion global > 0" step_nr="41" thread="0"> | |
| <location file="main.c" function="main" line="8" working-directory="/home/jakob/tmp"/> | |
| </failure> | |
| <failure hidden="false" property="main.assertion.2" reason="assertion *ptr > 0" step_nr="42" thread="0"> | |
| <location file="main.c" function="main" line="9" working-directory="/home/jakob/tmp"/> | |
| </failure> | |
| </goto_trace> | |
| </result> | |
| <message type="STATUS-MESSAGE"> | |
| <text>VERIFICATION FAILED</text> | |
| </message> | |
| <cprover-status>FAILURE</cprover-status> | |
| </cprover> |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment