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.
63 lines
1.3 KiB
63 lines
1.3 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.
|
||
|
|
*/
|
||
|
|
class Invariant {
|
||
|
|
|
||
|
|
// x is invariant
|
||
|
|
void x_is_invariant_ok(int size) {
|
||
|
|
int i = 0, x;
|
||
|
|
if (size > 10) {
|
||
|
|
x = 10;
|
||
|
|
} else {
|
||
|
|
x = 20;
|
||
|
|
}
|
||
|
|
while (i < size + x) {
|
||
|
|
i++;
|
||
|
|
}
|
||
|
|
}
|
||
|
|
|
||
|
|
// x shouldn't be invariant since it can have two different values
|
||
|
|
// depending on whether the inner conditional is executed or not
|
||
|
|
// Currently, we are getting T because of a problem in InferBo, see
|
||
|
|
// T32798161
|
||
|
|
void formal_not_invariant_FP(int size, int x) {
|
||
|
|
int i = 0;
|
||
|
|
while (i < size + x) {
|
||
|
|
if (x > i) {
|
||
|
|
x = 0;
|
||
|
|
}
|
||
|
|
i++;
|
||
|
|
}
|
||
|
|
}
|
||
|
|
|
||
|
|
// x shouldn't be invariant since it can have two different values
|
||
|
|
// depending on whether the inner conditional is executed or not
|
||
|
|
// Currently, we are getting T because of a problem in InferBo, see
|
||
|
|
// T32798161
|
||
|
|
void local_not_invariant_FP(int size) {
|
||
|
|
int i = 0;
|
||
|
|
int x = 5;
|
||
|
|
while (i < size + x) {
|
||
|
|
if (x > i) {
|
||
|
|
x = 0;
|
||
|
|
}
|
||
|
|
i++;
|
||
|
|
}
|
||
|
|
}
|
||
|
|
|
||
|
|
|
||
|
|
// m will be invariant
|
||
|
|
void do_while_invariant(int m, int k){
|
||
|
|
int i = 0;
|
||
|
|
do{
|
||
|
|
m = k;
|
||
|
|
i++;
|
||
|
|
}
|
||
|
|
while (i < m);
|
||
|
|
}
|
||
|
|
|
||
|
|
}
|