1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
CORE
main.c
--enforce-contract update _ --pointer-check --pointer-overflow-check --signed-overflow-check --unsigned-overflow-check --conversion-check
^\[update.assigns.\d+] line 73 Check that __CPROVER_object_whole\(\(.*\)state->digest.high_level.first.ctx->digest\) is valid when .*: SUCCESS
^\[update.assigns.\d+] line 74 Check that state->digest.high_level.first.ctx->flags is valid when .*: SUCCESS
^\[update.assigns.\d+] line 76 Check that __CPROVER_object_whole\(\(.*\)state->digest.high_level.second.ctx->digest\) is valid when .*: SUCCESS
^\[update.assigns.\d+] line 77 Check that state->digest.high_level.second.ctx->flags is valid when .*: SUCCESS
^\[is_high_level.assigns.\d+\] line 50 Check that latch is assignable: SUCCESS$
^\[is_high_level.assigns.\d+\] line 51 Check that once is assignable: SUCCESS$
^\[update.assigns.\d+\] line 84 Check that __CPROVER_POINTER_OBJECT\(\(void \*\)state->digest.high_level.first.ctx->digest\) is assignable: SUCCESS$
^\[update.assigns.\d+\] line 85 Check that state->digest.high_level.first.ctx->flags is assignable: SUCCESS$
^\[update.assigns.\d+\] line 90 Check that __CPROVER_POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: SUCCESS$
^\[update.assigns.\d+\] line 91 Check that state->digest.high_level.second.ctx->flags is assignable: SUCCESS$
^\[update.assigns.\d+\] line 95 Check that __CPROVER_POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: FAILURE$
^\[update.assigns.\d+\] line 96 Check that state->digest.high_level.second.ctx->flags is assignable: FAILURE$
^\[update.assigns.\d+\] line 100 Check that __CPROVER_POINTER_OBJECT\(\(void \*\)state->digest.high_level.first.ctx->digest\) is assignable: FAILURE$
^\[update.assigns.\d+\] line 101 Check that state->digest.high_level.first.ctx->flags is assignable: FAILURE$
^\[update.assigns.\d+\] line 104 Check that __CPROVER_POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: FAILURE$
^\[update.assigns.\d+\] line 105 Check that state->digest.high_level.second.ctx->flags is assignable: FAILURE$
^VERIFICATION FAILED$
^EXIT=10$
^SIGNAL=0$
--
--
Tests that conditional assignments to whole objects and lvalues are supported,
when conditions determine how to interpret a union type.
|
