File: bts709.c

package info (click to toggle)
frama-c 20140301%2Bneon%2Bdfsg-3
  • links: PTS, VCS
  • area: main
  • in suites: jessie, jessie-kfreebsd
  • size: 19,548 kB
  • ctags: 28,183
  • sloc: ml: 181,252; ansic: 13,776; makefile: 2,452; sh: 1,085; lisp: 178
file content (57 lines) | stat: -rw-r--r-- 897 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
/* run.config
   OPT: -check -slice-pragma func -no-unicode -journal-disable -then-on 'Slicing export' -print
 */

int inputsOf_testcase_func ();
int inp1, var1,var2;

void func(  void  )  
{ 
	if ( 1 == inp1 )  
	{ 
		// Block-1
		var1 =  1 ;
		var2 =  1 ;
	} 
	else  
 	{ 
		if (  2== inp1  )  
		{
			// Block-2
			 var1 = 2 ;
			 var2 = 2 ;
		} 
		else  
 		{ 
			// Block-3
			if (  3== inp1  )  
			{ 
				var1 =  3;
				var2 =  3  ;
			} 
		} 
	} 

	//@slice pragma stmt;
	 65 != var2 ? assert ( 5 != var1):1;
} 


int main( ) { 


	int _noOfIter_ = 0;
	for (_noOfIter_=0; _noOfIter_ < 1; _noOfIter_++ ) {
		inputsOf_testcase_func ( );
		func ();
	}
}

int inputsOf_testcase_func ()
{
	int nondet_int ( );
	inp1 = nondet_int ( );
	var1 = nondet_int ( );		// This required line is getting knocked off
	var2 = nondet_int ( );		// This required line is getting knocked off
        return 0;
}