Project

General

Profile

Download (582 Bytes)

Bug #9132 » slice.c

Slice generated using crude_slicer - Asia ., 07/19/2018 10:16 AM

 
/* Generated by Frama-C */

# 1 "/home/u1364447/Desktop/Bug_Reporting/Ternary_Readonly/test.c"
extern void __VERIFIER_error(void);


# 2
extern int nondet(void);


# 3 "/home/u1364447/Desktop/Bug_Reporting/Ternary_Readonly/test.c"
int main(void)
{
int __retres;
int m1;
int m2;
int b;
int const tmp;
# 6
m1 = nondet();
# 7
m2 = nondet();
# 8
if (m1 < m2)
# 8
tmp = m1; else
# 8
tmp = m2;
# 8
b = tmp;
# 9
if (b == 0)
# 11
__VERIFIER_error();
# 13
return __retres;
}


(1-1/3)