You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
55 lines
1.2 KiB
55 lines
1.2 KiB
6 years ago
|
/*
|
||
|
|
* Copyright (c) 2018-present, Facebook, Inc.
|
||
|
|
*
|
||
|
|
* This source code is licensed under the MIT license found in the
|
||
|
|
* LICENSE file in the root directory of this source tree.
|
||
|
|
*/
|
||
|
|
|
||
|
|
int check_sorted_arr_good_FP(int a[], int length) {
|
||
|
|
for (int i = 1; i < length; i++) {
|
||
|
|
if (a[i] < a[i - 1]) { // should not report CONDITION_ALWAYS_FALSE
|
||
|
|
return 0;
|
||
|
|
}
|
||
|
|
}
|
||
|
|
return 1;
|
||
|
|
}
|
||
|
|
|
||
|
|
int check_sorted_arr10_good_FP(int a[10], int length) {
|
||
|
|
for (int i = 1; i < length; i++) {
|
||
|
|
if (a[i] < a[i - 1]) { // should not report CONDITION_ALWAYS_FALSE
|
||
|
|
return 0;
|
||
|
|
}
|
||
|
|
}
|
||
|
|
return 1;
|
||
|
|
}
|
||
|
|
|
||
|
|
int check_sorted_ptr_good_FP(int* a, int length) {
|
||
|
|
for (int i = 1; i < length; i++) {
|
||
|
|
if (a[i] < a[i - 1]) { // should not report CONDITION_ALWAYS_FALSE
|
||
|
|
return 0;
|
||
|
|
}
|
||
|
|
}
|
||
|
|
return 1;
|
||
|
|
}
|
||
|
|
|
||
|
|
int array_min_index_from_one_FP(int* a, int length) {
|
||
|
|
int index_min = 1;
|
||
|
|
for (int i = 2; i < length; i++) {
|
||
|
|
if (a[i] < a[index_min]) { // should not report CONDITION_ALWAYS_FALSE
|
||
|
|
index_min = i;
|
||
|
|
} else {
|
||
|
|
index_min = i;
|
||
|
|
}
|
||
|
|
}
|
||
|
|
return index_min;
|
||
|
|
}
|
||
|
|
|
||
|
|
/*
|
||
|
|
We need a either a narrowing or a relational domain to prove that
|
||
|
|
index_min < length
|
||
|
|
*/
|
||
|
|
void call_array_min_index_from_one_good_FP() {
|
||
|
|
int a[2];
|
||
|
|
a[array_min_index_from_one_FP(a, 2) - 1] = 0;
|
||
|
|
}
|