[#334708] [test-only] FAILED (try 8) cbmc.git=5.95.1-alt1

[Girar awaiter (vt)]

https://git.altlinux.org/tasks/334708/logs/events.8.1.log

subtask  name  aarch64   armh  i586  ppc64le  x86_64
  #1000  cbmc     8:35  14:19  6:36     6:47  failed

2023-Nov-25 17:12:03 :: test-only task #334708 for sisyphus resumed by vt:
#100 removed
#200 removed
#300 removed
#400 removed
#500 removed
#600 removed
#700 removed
#1000 build 5.95.1-alt1 from /people/vt/packages/cbmc.git fetched at 2023-Nov-25 17:12:01
2023-Nov-25 17:12:05 :: [ppc64le] #1000 cbmc.git 5.95.1-alt1: build start
2023-Nov-25 17:12:05 :: [i586] #1000 cbmc.git 5.95.1-alt1: build start
2023-Nov-25 17:12:05 :: [aarch64] #1000 cbmc.git 5.95.1-alt1: build start
2023-Nov-25 17:12:05 :: [x86_64] #1000 cbmc.git 5.95.1-alt1: build start
2023-Nov-25 17:12:05 :: [armh] #1000 cbmc.git 5.95.1-alt1: build start
[x86_64] <builtin-library-__CPROVER_contracts_library> function __CPROVER_contracts_car_set_insert
[x86_64] [__CPROVER_contracts_car_set_insert.assertion.1] line 162 ptr NULL or writable up to size: ERROR
[x86_64] [__CPROVER_contracts_car_set_insert.assertion.4] line 162 ptr NULL or writable up to size: SUCCESS
[x86_64] [__CPROVER_contracts_car_set_insert.assertion.7] line 162 ptr NULL or writable up to size: SUCCESS
[x86_64] [__CPROVER_contracts_car_set_insert.assertion.2] line 165 CAR size is less than __CPROVER_max_malloc_size: ERROR
[x86_64] [__CPROVER_contracts_car_set_insert.assertion.5] line 165 CAR size is less than __CPROVER_max_malloc_size: SUCCESS
[x86_64] [__CPROVER_contracts_car_set_insert.assertion.8] line 165 CAR size is less than __CPROVER_max_malloc_size: SUCCESS
[x86_64] [__CPROVER_contracts_car_set_insert.assertion.3] line 169 no offset bits overflow on CAR upper bound computation: ERROR
[x86_64] [__CPROVER_contracts_car_set_insert.assertion.6] line 169 no offset bits overflow on CAR upper bound computation: SUCCESS
[x86_64] --
[x86_64] <builtin-library-__CPROVER_contracts_library> function __CPROVER_contracts_write_set_check_assignment
[x86_64] [__CPROVER_contracts_write_set_check_assignment.assertion.1] line 776 ptr NULL or writable up to size: ERROR
[x86_64] [__CPROVER_contracts_write_set_check_assignment.assertion.2] line 793 CAR size is less than __CPROVER_max_malloc_size: ERROR
[x86_64] [__CPROVER_contracts_write_set_check_assignment.assertion.3] line 799 no offset bits overflow on CAR upper bound computation: ERROR
[x86_64] [__CPROVER_contracts_write_set_check_assignment.unwind.1] line 808 unwinding assertion loop 0: SUCCESS
[x86_64] --
[x86_64] <builtin-library-__CPROVER_contracts_library> function __CPROVER_contracts_write_set_havoc_slice
[x86_64] [__CPROVER_contracts_write_set_havoc_slice.assertion.1] line 1422 assertion havoc_slice W_OK(car.lb, car.size): ERROR
[x86_64] <builtin-library-malloc> function malloc
[x86_64] --
[x86_64] [foo.assigns.2] line 5 Check that return_value___CPROVER_is_fresh$0 is assignable: SUCCESS
[x86_64] [foo.postcondition.1] line 7 Check ensures clause of contract contract::foo for function foo: ERROR
[x86_64] [foo.assigns.3] line 13 Check that i is assignable: SUCCESS
[x86_64] [foo.assigns.5] line 13 Check that i is assignable: ERROR
[x86_64] [foo.assigns.7] line 13 Check that i is assignable: ERROR
[x86_64] [foo.loop_assigns.1] line 13 Check assigns clause inclusion for loop foo.0: SUCCESS
2023-Nov-25 17:17:46 :: [x86_64] cbmc.git 5.95.1-alt1: remote: build failed
2023-Nov-25 17:17:46 :: [x86_64] #1000 cbmc.git 5.95.1-alt1: build FAILED
2023-Nov-25 17:17:46 :: [x86_64] requesting cancellation of task processing
2023-Nov-25 17:18:41 :: [i586] #1000 cbmc.git 5.95.1-alt1: build OK
2023-Nov-25 17:18:52 :: [ppc64le] #1000 cbmc.git 5.95.1-alt1: build OK
2023-Nov-25 17:20:40 :: [aarch64] #1000 cbmc.git 5.95.1-alt1: build OK
2023-Nov-25 17:26:24 :: [armh] #1000 cbmc.git 5.95.1-alt1: build OK
2023-Nov-25 17:17:46 :: [x86_64] build FAILED
2023-Nov-25 17:26:24 :: task #334708 for sisyphus FAILED