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.
33 lines
671 B
33 lines
671 B
6 years ago
|
/*
|
||
6 years ago
|
* Copyright (c) Facebook, Inc. and its affiliates.
|
||
|
6 years ago
|
*
|
||
|
|
* This source code is licensed under the MIT license found in the
|
||
|
|
* LICENSE file in the root directory of this source tree.
|
||
|
|
*/
|
||
|
|
// Command: infer -g --biabduction-only
|
||
|
|
class T {
|
||
|
|
static int q;
|
||
|
|
|
||
|
|
static void f() {
|
||
|
|
if (q == 0) {
|
||
|
|
q = 1;
|
||
|
|
} else if (q == 1) {
|
||
|
|
while (true) ;
|
||
|
|
}
|
||
|
|
}
|
||
|
|
|
||
|
|
static void h() {
|
||
|
|
// Important to have 2 branches, and one of them is (q==1).
|
||
|
|
if (q == 1) {
|
||
|
|
} else if (q == 2) {
|
||
|
|
}
|
||
|
|
}
|
||
|
|
|
||
|
|
static void go() {
|
||
|
|
q = 0;
|
||
|
|
f();
|
||
|
|
h(); // warning disappears if the NOP function h() is called here
|
||
|
|
f(); // should warn of PRECONDITION_NOT_MET here
|
||
|
|
}
|
||
|
|
}
|