int __VERIFIER_nondet_int(); extern void __VERIFIER_error() __attribute__((noreturn)); // method ids int m_isPowerOfTwo = 1; int m_IntMath = 2; int m_log10 = 3; int m_checkedSubtract = 4; int m_checkedMultiply = 5; int m_log2 = 6; int m_checkedAdd = 7; int m_mod_1 = 8; int m_mod_2 = 9; int m_factorial_1 = 10; int m_factorial_2 = 11; int main() { int q = 0; int method_id; // variables while (1) { // parameters int P1=__VERIFIER_nondet_int(); int P2=__VERIFIER_nondet_int(); int P3=__VERIFIER_nondet_int(); int P4=__VERIFIER_nondet_int(); int P5=__VERIFIER_nondet_int(); int P6=__VERIFIER_nondet_int(); int P7=__VERIFIER_nondet_int(); int P8=__VERIFIER_nondet_int(); int P9=__VERIFIER_nondet_int(); int P10=__VERIFIER_nondet_int(); int P11=__VERIFIER_nondet_int(); int P12=__VERIFIER_nondet_int(); int P13=__VERIFIER_nondet_int(); int P14=__VERIFIER_nondet_int(); int P15=__VERIFIER_nondet_int(); int P16=__VERIFIER_nondet_int(); int P17=__VERIFIER_nondet_int(); // states if (q == 0){ if(__VERIFIER_nondet_int()){ // assume guard if ( 1 ){ // record method id method_id = 2; // non-conformance condition if ( 0 ) { goto ERROR; } // state update q = 2; // post condition } continue; } continue; } if (q == 1){ if(__VERIFIER_nondet_int()){ // assume guard if ( 1 ){ // record method id method_id = 3; // non-conformance condition if ( 0 ) { goto ERROR; } // state update q = 1; // post condition break; } continue; } if(__VERIFIER_nondet_int()){ // assume guard if ( 1 ){ // record method id method_id = 6; // non-conformance condition if ( 0 ) { goto ERROR; } // state update q = 1; // post condition break; } continue; } if(__VERIFIER_nondet_int()){ // assume guard if ( !((P1 >= 0) && (P2 > 0)) ){ // record method id method_id = 9; // non-conformance condition if ( 0 ) { goto ERROR; } // state update q = 1; // post condition break; } continue; } if(__VERIFIER_nondet_int()){ // assume guard if ( (P1 < 0) ){ // record method id method_id = 10; // non-conformance condition if ( 0 ) { goto ERROR; } // state update q = 1; // post condition break; } continue; } continue; } if (q == 2){ if(__VERIFIER_nondet_int()){ // assume guard if ( 1&& ((((P1 & (P1 - 1)) == 0) && (P1 > 0)) || 0) ){ // record method id method_id = 1; // non-conformance condition if ( 0 ) { goto ERROR; } // state update q = 2; // post condition } continue; } if(__VERIFIER_nondet_int()){ // assume guard if ( 1&& ((((P1 & (P1 - 1)) == 0) && (P1 > 0)) || 0)&& ((((P1 & (P1 - 1)) != 0) && (P1 > 0)) || 0) ){ // record method id method_id = 1; // non-conformance condition if ( 0 ) { goto ERROR; } // state update q = 2; // post condition } continue; } if(__VERIFIER_nondet_int()){ // assume guard if ( 1&& ((((P1 & (P1 - 1)) == 0) && (P1 > 0)) || 0)&& ((((P1 & (P1 - 1)) != 0) && (P1 > 0)) || 0)&& ((((P1 & (P1 - 1)) == 0) && (P1 <= 0)) || 0) ){ // record method id method_id = 1; // non-conformance condition if ( 0 ) { goto ERROR; } // state update q = 2; // post condition } continue; } if(__VERIFIER_nondet_int()){ // assume guard if ( 1&& ((((P1 & (P1 - 1)) == 0) && (P1 > 0)) || 0)&& ((((P1 & (P1 - 1)) != 0) && (P1 > 0)) || 0)&& ((((P1 & (P1 - 1)) == 0) && (P1 <= 0)) || 0)&& ((((P1 & (P1 - 1)) != 0) && (P1 <= 0)) || 0) ){ // record method id method_id = 1; // non-conformance condition if ( 0 ) { goto ERROR; } // state update q = 2; // post condition } continue; } if(__VERIFIER_nondet_int()){ // assume guard if ( 1 ){ // record method id method_id = 3; // non-conformance condition if ( 0 ) { goto ERROR; } // state update q = 1; // post condition break; } continue; } if(__VERIFIER_nondet_int()){ // assume guard if ( 1 ){ // record method id method_id = 4; // non-conformance condition if ( 0 ) { goto ERROR; } // state update q = 2; // post condition } continue; } if(__VERIFIER_nondet_int()){ // assume guard if ( 1 ){ // record method id method_id = 5; // non-conformance condition if ( 0 ) { goto ERROR; } // state update q = 2; // post condition } continue; } if(__VERIFIER_nondet_int()){ // assume guard if ( 1 ){ // record method id method_id = 6; // non-conformance condition if ( 0 ) { goto ERROR; } // state update q = 1; // post condition break; } continue; } if(__VERIFIER_nondet_int()){ // assume guard if ( 1 ){ // record method id method_id = 7; // non-conformance condition if ( 0 ) { goto ERROR; } // state update q = 2; // post condition } continue; } if(__VERIFIER_nondet_int()){ // assume guard if ( ((P1 >= 0) && (P2 > 0)) ){ // record method id method_id = 8; // non-conformance condition if ( 0 ) { goto ERROR; } // state update q = 2; // post condition } continue; } if(__VERIFIER_nondet_int()){ // assume guard if ( !((P1 >= 0) && (P2 > 0)) ){ // record method id method_id = 9; // non-conformance condition if ( 0 ) { goto ERROR; } // state update q = 1; // post condition break; } continue; } if(__VERIFIER_nondet_int()){ // assume guard if ( (P1 < 0) ){ // record method id method_id = 10; // non-conformance condition if ( 0 ) { goto ERROR; } // state update q = 1; // post condition break; } continue; } if(__VERIFIER_nondet_int()){ // assume guard if ( !(P1 < 0)&& (((P17 < 13) && (P17 >= 0)) || 0) ){ // record method id method_id = 11; // non-conformance condition if ( 0 ) { goto ERROR; } // state update q = 2; // post condition } continue; } if(__VERIFIER_nondet_int()){ // assume guard if ( !(P1 < 0)&& (((P17 < 13) && (P17 >= 0)) || 0)&& (((P17 >= 13) && (P17 >= 0)) || 0) ){ // record method id method_id = 11; // non-conformance condition if ( 0 ) { goto ERROR; } // state update q = 2; // post condition } continue; } continue; } } // end while return 0; ERROR: __VERIFIER_error(); }