Skip to content

Commit 5d3cffc

Browse files
ArenBabikianArenBabikian
committed
Fixes formatting
1 parent 280e85f commit 5d3cffc

File tree

10 files changed

+60
-50
lines changed

10 files changed

+60
-50
lines changed

‎regression/contracts/quantifiers-exists-ensures-01/main.c

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
1-
int f1(int *arr)
2-
__CPROVER_ensures(
3-
__CPROVER_exists {int i; (0 <= i && i < 10) && arr[i] == i}
4-
)
1+
int f1(int *arr) __CPROVER_ensures(__CPROVER_exists {
2+
int i;
3+
(0 <= i && i < 10) && arr[i] == i
4+
})
55
{
66
for(int i = 0; i < 10; i++)
77
{

‎regression/contracts/quantifiers-exists-ensures-02/main.c

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
1-
int f1(int *arr)
2-
__CPROVER_ensures(
3-
__CPROVER_exists {int i; (0 <= i && i < 10) && arr[i] != 0}
4-
)
1+
int f1(int *arr) __CPROVER_ensures(__CPROVER_exists {
2+
int i;
3+
(0 <= i && i < 10) && arr[i] != 0
4+
})
55
{
66
for(int i = 0; i < 10; i++)
77
{

‎regression/contracts/quantifiers-exists-requires-01/main.c

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,13 @@
1-
int f1(int *arr)
2-
__CPROVER_requires(
3-
__CPROVER_exists {int i; (0 <= i && i < 10) && arr[i] == 4}
4-
)
5-
__CPROVER_ensures(__CPROVER_return_value == 0)
1+
int f1(int *arr) __CPROVER_requires(__CPROVER_exists {
2+
int i;
3+
(0 <= i && i < 10) && arr[i] == 4
4+
}) __CPROVER_ensures(__CPROVER_return_value == 0)
65
{
76
return 0;
87
}
98

109
int main()
1110
{
12-
int arr[10] = {0,1,2,3,4,5,6,7,8,9};
11+
int arr[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9};
1312
f1(arr);
1413
}

‎regression/contracts/quantifiers-exists-requires-02/main.c

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,13 @@
1-
int f1(int *arr)
2-
__CPROVER_requires(
3-
__CPROVER_exists {int i; (0 <= i && i < 10) && arr[i] == 1}
4-
)
5-
__CPROVER_ensures(__CPROVER_return_value == 0)
1+
int f1(int *arr) __CPROVER_requires(__CPROVER_exists {
2+
int i;
3+
(0 <= i && i < 10) && arr[i] == 1
4+
}) __CPROVER_ensures(__CPROVER_return_value == 0)
65
{
76
return 0;
87
}
98

109
int main()
1110
{
12-
int arr[10] = {0,0,0,0,0,0,0,0,0,0};
11+
int arr[10] = {0, 0, 0, 0, 0, 0, 0, 0, 0, 0};
1312
f1(arr);
1413
}

‎regression/contracts/quantifiers-forall-ensures-01/main.c

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,9 @@
1-
int f1(int *arr)
2-
__CPROVER_ensures(
3-
__CPROVER_forall {int i; (0 <= i && i < 10) ==> arr[i] == 0}
4-
)
1+
// clang-format off
2+
int f1(int *arr) __CPROVER_ensures(__CPROVER_forall {
3+
int i;
4+
(0 <= i && i < 10) ==> arr[i] == 0
5+
})
6+
// clang-format on
57
{
68
for(int i = 0; i < 10; i++)
79
{

‎regression/contracts/quantifiers-forall-ensures-02/main.c

Lines changed: 10 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,16 @@
1-
int f1(int *arr)
2-
__CPROVER_ensures(
3-
__CPROVER_forall {int i; (0 <= i && i < 10) ==> arr[i] == i}
4-
)
1+
// clang-format off
2+
int f1(int *arr) __CPROVER_ensures(__CPROVER_forall {
3+
int i;
4+
(0 <= i && i < 10) ==> arr[i] == i
5+
})
6+
// clang-format on
57
{
68
for(int i = 0; i < 10; i++)
79
{
8-
if (i == 0) arr[i] = -1;
9-
else arr[i] = i;
10+
if(i == 0)
11+
arr[i] = -1;
12+
else
13+
arr[i] = i;
1014
}
1115

1216
return 0;

‎regression/contracts/quantifiers-forall-requires-01/main.c

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,15 @@
1-
int f1(int *arr)
2-
__CPROVER_requires(
3-
__CPROVER_forall {int i; (0 <= i && i < 10) ==> arr[i] == i}
4-
)
5-
__CPROVER_ensures(__CPROVER_return_value == 0)
1+
// clang-format off
2+
int f1(int *arr) __CPROVER_requires(__CPROVER_forall {
3+
int i;
4+
(0 <= i && i < 10) ==> arr[i] == i
5+
}) __CPROVER_ensures(__CPROVER_return_value == 0)
6+
// clang-format on
67
{
78
return 0;
89
}
910

1011
int main()
1112
{
12-
int arr[10] = {0,1,2,3,4,5,6,7,8,9};
13+
int arr[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9};
1314
f1(arr);
1415
}

‎regression/contracts/quantifiers-forall-requires-02/main.c

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,15 @@
1-
int f1(int *arr)
2-
__CPROVER_requires(
3-
__CPROVER_forall {int i; (0 <= i && i < 10) ==> arr[i] == i}
4-
)
5-
__CPROVER_ensures(__CPROVER_return_value == 0)
1+
// clang-format off
2+
int f1(int *arr) __CPROVER_requires(__CPROVER_forall {
3+
int i;
4+
(0 <= i && i < 10) ==> arr[i] == i
5+
}) __CPROVER_ensures(__CPROVER_return_value == 0)
6+
// clang-format on
67
{
78
return 0;
89
}
910

1011
int main()
1112
{
12-
int arr[10] = {-1,1,2,3,4,5,6,7,8,9};
13+
int arr[10] = {-1, 1, 2, 3, 4, 5, 6, 7, 8, 9};
1314
f1(arr);
1415
}

‎src/goto-instrument/code_contracts.cpp

Lines changed: 11 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -171,17 +171,18 @@ bool code_contractst::has_contract(const irep_idt fun_name)
171171
}
172172

173173
void code_contractst::add_quantified_variable(
174-
exprt expression, replace_symbolt &replace, irep_idt mode)
174+
exprt expression,
175+
replace_symbolt &replace,
176+
irep_idt mode)
175177
{
176178
//If the expression is a quantified expression, this function adds
177179
//the quantified variable to the symbol table and to the expression map
178180

179181
//TODO Currently only works if the contract contains only a single quantified formula
180182
// i.e. (1) the top-level element is a quantifier formula
181183
//and (2) there are no inner quantifier formulae
182-
if(expression.id()==ID_exists || expression.id()==ID_forall)
184+
if(expression.id() == ID_exists || expression.id() == ID_forall)
183185
{
184-
185186
//get quantified symbol
186187
exprt tuple = expression.operands().front();
187188
exprt quantified_variable = tuple.operands().front();
@@ -197,7 +198,8 @@ void code_contractst::add_quantified_variable(
197198
symbol_table);
198199

199200
// add created fresh symbol to expression map
200-
symbol_exprt q(quantified_symbol.get_identifier(), quantified_symbol.type());
201+
symbol_exprt q(
202+
quantified_symbol.get_identifier(), quantified_symbol.type());
201203
replace.insert(q, new_symbol.symbol_expr());
202204
}
203205
}
@@ -283,7 +285,7 @@ bool code_contractst::apply_function_contract(
283285
}
284286

285287
// Add quantified variables in contracts to the symbol map
286-
irep_idt mode = symbol_table.lookup_ref(function).mode;
288+
irep_idt mode = symbol_table.lookup_ref(function).mode;
287289
code_contractst::add_quantified_variable(ensures, replace, mode);
288290
code_contractst::add_quantified_variable(requires, replace, mode);
289291

@@ -839,8 +841,10 @@ void code_contractst::add_contract_check(
839841
}
840842

841843
// Add quantified variables in contracts to the symbol map
842-
code_contractst::add_quantified_variable(ensures, replace, function_symbol.mode);
843-
code_contractst::add_quantified_variable(requires, replace, function_symbol.mode);
844+
code_contractst::add_quantified_variable(
845+
ensures, replace, function_symbol.mode);
846+
code_contractst::add_quantified_variable(
847+
requires, replace, function_symbol.mode);
844848

845849
// assume(requires)
846850
if(requires.is_not_nil())

‎src/goto-instrument/code_contracts.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -169,7 +169,7 @@ class code_contractst
169169
//If the expression is a quantified expression, this function adds
170170
//the quantified variable to the symbol table and to the expression map
171171
void add_quantified_variable(
172-
exprt expression,
172+
exprt expression,
173173
replace_symbolt &replace,
174174
irep_idt mode);
175175
};

0 commit comments

Comments
 (0)