Skip to content

Commit ff2ddce

Browse files
author
Remi Delmas
committed
format fixes
1 parent c11c7c7 commit ff2ddce

File tree

3 files changed

+5
-1
lines changed
  • regression/contracts
    • invar_havoc_dynamic_array
    • invar_havoc_static_array
    • invar_havoc_static_multi-dim_array_partial_const_idx

3 files changed

+5
-1
lines changed

regression/contracts/invar_havoc_dynamic_array/main.c

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,10 @@ void main()
99
data[5] = 0;
1010

1111
for(unsigned i = 0; i < SIZE; i++)
12+
// clang-format off
1213
__CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(data))
1314
__CPROVER_loop_invariant(i <= SIZE)
15+
// clang-format on
1416
{
1517
data[i] = 1;
1618
}

regression/contracts/invar_havoc_static_array/main.c

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,10 @@ void main()
99
data[5] = 0;
1010

1111
for(unsigned i = 0; i < SIZE; i++)
12+
// clang-format off
1213
__CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(data))
1314
__CPROVER_loop_invariant(i <= SIZE)
15+
// clang-format on
1416
{
1517
data[i] = 1;
1618
}

regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ main.c
66
^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
77
^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
88
^\[main\.\d+\] .* Check that i is assignable: SUCCESS$
9-
^\[main\.\d+\] .* Check that data\[\(signed long int\)4\]\[\(signed long int\)i\]\[\(signed long int\)6\] is assignable: SUCCESS$
9+
^\[main\.\d+\] .* Check that data\[\(signed long (long )?int\)4\]\[\(signed long (long )?int\)i\]\[\(signed long (long )?int\)6\] is assignable: SUCCESS$
1010
^\[main\.assertion\.\d+\] .* assertion data\[1\]\[2\]\[3\] == 0: FAILURE$
1111
^\[main\.assertion\.\d+\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$
1212
^VERIFICATION FAILED$

0 commit comments

Comments
 (0)