cbmc --bounds-check --pointer-check --memory-cleanup-check --div-by-zero-check --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check --conversion-check --undefined-shift-check --enum-range-check --pointer-primitive-check --external-sat-solver cadical isqrt_contracts.goto CBMC version 5.84.0 (cbmc-5.84.0) 64-bit arm64 macos Reading GOTO program from file isqrt_contracts.goto ** Results: function __CPROVER_contracts_car_create: SUCCESS function __CPROVER_contracts_car_set_contains: SUCCESS function __CPROVER_contracts_car_set_create: SUCCESS function __CPROVER_contracts_car_set_insert: SUCCESS function __CPROVER_contracts_car_set_remove: SUCCESS function __CPROVER_contracts_check_replace_ensures_was_freed_preconditions: SUCCESS function __CPROVER_contracts_is_freeable: SUCCESS function __CPROVER_contracts_is_fresh: SUCCESS function __CPROVER_contracts_link_allocated: SUCCESS function __CPROVER_contracts_obeys_contract: SUCCESS function __CPROVER_contracts_obj_set_add: SUCCESS function __CPROVER_contracts_obj_set_append: SUCCESS function __CPROVER_contracts_obj_set_contains: SUCCESS function __CPROVER_contracts_obj_set_contains_exact: SUCCESS function __CPROVER_contracts_obj_set_create_append: SUCCESS function __CPROVER_contracts_obj_set_create_indexed_by_object_id: SUCCESS function __CPROVER_contracts_obj_set_remove: SUCCESS function __CPROVER_contracts_pointer_in_range_dfcc: SUCCESS function __CPROVER_contracts_was_freed: SUCCESS function __CPROVER_contracts_write_set_add_allocated: SUCCESS function __CPROVER_contracts_write_set_check_array_copy: SUCCESS function __CPROVER_contracts_write_set_check_array_replace: SUCCESS function __CPROVER_contracts_write_set_check_array_set: SUCCESS function __CPROVER_contracts_write_set_check_assignment: SUCCESS function __CPROVER_contracts_write_set_check_deallocate: SUCCESS function __CPROVER_contracts_write_set_check_frees_clause_inclusion: SUCCESS function __CPROVER_contracts_write_set_deallocate_freeable: SUCCESS function __CPROVER_contracts_write_set_havoc_object_whole: SUCCESS function __CPROVER_contracts_write_set_havoc_slice: SUCCESS function __CPROVER_contracts_write_set_insert_object_from: SUCCESS function __CPROVER_contracts_write_set_record_deallocated: SUCCESS function malloc isqrt.c function isqrt [isqrt.no_alloc_dealloc_in_ensures.1] line 16 Check that ensures do not allocate or deallocate memory: SUCCESS [isqrt.no_alloc_dealloc_in_requires.1] line 16 Check that requires do not allocate or deallocate memory: SUCCESS [isqrt.no_recursive_call.1] line 16 No recursive call to function isqrt when checking contract isqrt: SUCCESS [isqrt.single_top_level_call.1] line 16 Only a single top-level call to function isqrt when checking contract isqrt: SUCCESS [isqrt.overflow.1] line 20 arithmetic overflow on signed * in __contract_return_value * __contract_return_value: SUCCESS [isqrt.postcondition.1] line 20 Check ensures clause of contract contract::isqrt for function isqrt: SUCCESS [isqrt.overflow.2] line 21 arithmetic overflow on signed + in (int64_t)__contract_return_value + (signed long int)1: SUCCESS [isqrt.overflow.3] line 21 arithmetic overflow on signed * in ((int64_t)__contract_return_value + (signed long int)1) * ((int64_t)__contract_return_value + (signed long int)1): SUCCESS [isqrt.assigns.1] line 24 Check that lower is assignable: SUCCESS [isqrt.assigns.2] line 25 Check that upper is assignable: SUCCESS [isqrt.loop_assigns.1] line 26 Check assigns clause inclusion for loop isqrt.0: SUCCESS [isqrt.loop_assigns.2] line 26 Check assigns clause inclusion for loop isqrt.0: SUCCESS [isqrt.loop_decreases.1] line 26 Check variant decreases after step for loop isqrt.0: SUCCESS [isqrt.loop_invariant_base.1] line 26 Check invariant before entry for loop isqrt.0: SUCCESS [isqrt.loop_invariant_base.2] line 26 Check invariant before entry for loop isqrt.0: SUCCESS [isqrt.loop_invariant_step.1] line 26 Check invariant after step for loop isqrt.0: SUCCESS [isqrt.loop_step_unwinding.1] line 26 Check step was unwound for loop isqrt.0: SUCCESS [isqrt.overflow.9] line 26 arithmetic overflow on signed + in lower + 1: SUCCESS [isqrt.overflow.15] line 26 arithmetic overflow on signed + in lower + 1: SUCCESS [isqrt.pointer_dereference.1] line 27 dereference failure: pointer NULL in *__havoc_target: SUCCESS [isqrt.pointer_dereference.2] line 27 dereference failure: pointer invalid in *__havoc_target: SUCCESS [isqrt.pointer_dereference.3] line 27 dereference failure: deallocated dynamic object in *__havoc_target: SUCCESS [isqrt.pointer_dereference.4] line 27 dereference failure: dead object in *__havoc_target: SUCCESS [isqrt.pointer_dereference.5] line 27 dereference failure: pointer outside object bounds in *__havoc_target: SUCCESS [isqrt.pointer_dereference.6] line 27 dereference failure: invalid integer address in *__havoc_target: SUCCESS [isqrt.pointer_dereference.7] line 27 dereference failure: pointer NULL in *__havoc_target$0: SUCCESS [isqrt.pointer_dereference.8] line 27 dereference failure: pointer invalid in *__havoc_target$0: SUCCESS [isqrt.pointer_dereference.9] line 27 dereference failure: deallocated dynamic object in *__havoc_target$0: SUCCESS [isqrt.pointer_dereference.10] line 27 dereference failure: dead object in *__havoc_target$0: SUCCESS [isqrt.pointer_dereference.11] line 27 dereference failure: pointer outside object bounds in *__havoc_target$0: SUCCESS [isqrt.pointer_dereference.12] line 27 dereference failure: invalid integer address in *__havoc_target$0: SUCCESS [isqrt.pointer_dereference.13] line 27 dereference failure: pointer NULL in *__havoc_target$1: SUCCESS [isqrt.pointer_dereference.14] line 27 dereference failure: pointer invalid in *__havoc_target$1: SUCCESS [isqrt.pointer_dereference.15] line 27 dereference failure: deallocated dynamic object in *__havoc_target$1: SUCCESS [isqrt.pointer_dereference.16] line 27 dereference failure: dead object in *__havoc_target$1: SUCCESS [isqrt.pointer_dereference.17] line 27 dereference failure: pointer outside object bounds in *__havoc_target$1: SUCCESS [isqrt.pointer_dereference.18] line 27 dereference failure: invalid integer address in *__havoc_target$1: SUCCESS [isqrt.overflow.4] line 30 arithmetic overflow on signed * in lower * lower: SUCCESS [isqrt.overflow.6] line 30 arithmetic overflow on signed * in lower * lower: SUCCESS [isqrt.overflow.12] line 30 arithmetic overflow on signed * in lower * lower: SUCCESS [isqrt.overflow.18] line 30 arithmetic overflow on signed * in lower * lower: SUCCESS [isqrt.overflow.5] line 32 arithmetic overflow on signed * in (int64_t)upper * (int64_t)upper: SUCCESS [isqrt.overflow.7] line 32 arithmetic overflow on signed * in (int64_t)upper * (int64_t)upper: SUCCESS [isqrt.overflow.13] line 32 arithmetic overflow on signed * in (int64_t)upper * (int64_t)upper: SUCCESS [isqrt.overflow.19] line 32 arithmetic overflow on signed * in (int64_t)upper * (int64_t)upper: SUCCESS [isqrt.overflow.8] line 33 arithmetic overflow on signed - in upper - lower: SUCCESS [isqrt.overflow.14] line 33 arithmetic overflow on signed - in upper - lower: SUCCESS [isqrt.overflow.20] line 33 arithmetic overflow on signed - in upper - lower: SUCCESS [isqrt.assigns.3] line 35 Check that middle is assignable: SUCCESS [isqrt.assigns.6] line 35 Check that middle is assignable: SUCCESS [isqrt.overflow.10] line 35 arithmetic overflow on signed + in lower + upper: SUCCESS [isqrt.overflow.16] line 35 arithmetic overflow on signed + in lower + upper: SUCCESS [isqrt.overflow.11] line 36 arithmetic overflow on signed * in middle * middle: SUCCESS [isqrt.overflow.17] line 36 arithmetic overflow on signed * in middle * middle: SUCCESS [isqrt.assigns.4] line 37 Check that upper is assignable: SUCCESS [isqrt.assigns.7] line 37 Check that upper is assignable: SUCCESS [isqrt.assigns.5] line 39 Check that lower is assignable: SUCCESS [isqrt.assigns.8] line 39 Check that lower is assignable: SUCCESS isqrt.c function isqrt_harness [isqrt_harness.assigns.1] line 47 Check that y is assignable: SUCCESS ** 0 of 1542 failed (1 iterations) VERIFICATION SUCCESSFUL