|
1 | | -/* Copyright 2020, TU Dortmund, Malte Mues ([email protected]) |
2 | | -This testcase is derived from the following File in the Juliet Benchmark found at: |
3 | | -https://samate.nist.gov/SARD/testsuite.php in Version 1.3 |
4 | | -Modifications are licenced under CC0 licence. |
5 | | -
|
6 | | -The original file is: |
7 | | -Filename: CWE369_Divide_by_Zero__float_connect_tcp_divide_01.java |
8 | | -Label Definition File: CWE369_Divide_by_Zero__float.label.xml |
9 | | -Template File: sources-sinks-01.tmpl.java |
10 | | -
|
11 | | -It is renamed to Main.java according to SV-Comp rules. |
12 | | -*/ |
13 | | - |
14 | | -/* |
15 | | - * @description |
16 | | - * CWE: 369 Divide by zero |
17 | | - * BadSource: connect_tcp Read data using an outbound tcp connection |
18 | | - * GoodSource: A hardcoded non-zero number (two) |
19 | | - * Sinks: divide |
20 | | - * GoodSink: Check for zero before dividing |
21 | | - * BadSink : Dividing by a value that may be zero |
22 | | - * Flow Variant: 01 Baseline |
23 | | - * |
24 | | - * */ |
25 | | - |
26 | | -import java.io.IOException; |
27 | | -import java.io.InputStreamReader; |
28 | | -import java.net.Socket; |
29 | | -import testcasesupport.*; |
30 | | - |
31 | | -public class Main { |
32 | | - public void bad() throws Throwable { |
33 | | - float data; |
34 | | - |
35 | | - data = -1.0f; /* Initialize data */ |
36 | | - |
37 | | - /* Read data using an outbound tcp connection */ |
38 | | - { |
39 | | - Socket socket = null; |
40 | | - BufferedReader readerBuffered = null; |
41 | | - InputStreamReader readerInputStream = null; |
42 | | - |
43 | | - try { |
44 | | - /* Read data using an outbound tcp connection */ |
45 | | - socket = new Socket("host.example.org", 39544); |
46 | | - |
47 | | - /* read input from socket */ |
48 | | - |
49 | | - readerInputStream = new InputStreamReader(socket.getInputStream(), "UTF-8"); |
50 | | - readerBuffered = new BufferedReader(readerInputStream); |
51 | | - |
52 | | - /* POTENTIAL FLAW: Read data using an outbound tcp connection */ |
53 | | - String stringNumber = readerBuffered.readLine(); |
54 | | - if (stringNumber != null) // avoid NPD incidental warnings |
55 | | - { |
56 | | - try { |
57 | | - data = Float.parseFloat(stringNumber.trim()); |
58 | | - } catch (NumberFormatException exceptNumberFormat) { |
59 | | - IO.writeLine("Number format exception parsing data from string"); |
60 | | - } |
61 | | - } |
62 | | - } catch (IOException exceptIO) { |
63 | | - IO.writeLine("Error with stream reading"); |
64 | | - } finally { |
65 | | - /* clean up stream reading objects */ |
66 | | - try { |
67 | | - if (readerBuffered != null) { |
68 | | - readerBuffered.close(); |
69 | | - } |
70 | | - } catch (IOException exceptIO) { |
71 | | - IO.writeLine("Error closing BufferedReader"); |
72 | | - } |
73 | | - |
74 | | - try { |
75 | | - if (readerInputStream != null) { |
76 | | - readerInputStream.close(); |
77 | | - } |
78 | | - } catch (IOException exceptIO) { |
79 | | - IO.writeLine("Error closing InputStreamReader"); |
80 | | - } |
81 | | - |
82 | | - /* clean up socket objects */ |
83 | | - try { |
84 | | - if (socket != null) { |
85 | | - socket.close(); |
86 | | - } |
87 | | - } catch (IOException exceptIO) { |
88 | | - IO.writeLine("Error closing Socket"); |
89 | | - } |
90 | | - } |
91 | | - } |
92 | | - |
93 | | - /* POTENTIAL FLAW: Possibly divide by zero */ |
94 | | - int result = (int) (100.0 / data); |
95 | | - if (1 < data || data <= 0) { |
96 | | - assert result < 100; |
97 | | - } |
98 | | - |
99 | | - IO.writeLine(result); |
100 | | - } |
101 | | - |
102 | | - public void good() throws Throwable { |
103 | | - goodG2B(); |
104 | | - goodB2G(); |
105 | | - } |
106 | | - |
107 | | - /* goodG2B() - use goodsource and badsink */ |
108 | | - private void goodG2B() throws Throwable { |
109 | | - float data; |
110 | | - |
111 | | - /* FIX: Use a hardcoded number that won't a divide by zero */ |
112 | | - data = 2.0f; |
113 | | - |
114 | | - /* POTENTIAL FLAW: Possibly divide by zero */ |
115 | | - int result = (int) (100.0 / data); |
116 | | - IO.writeLine(result); |
117 | | - } |
118 | | - |
119 | | - /* goodB2G() - use badsource and goodsink */ |
120 | | - private void goodB2G() throws Throwable { |
121 | | - float data; |
122 | | - |
123 | | - data = -1.0f; /* Initialize data */ |
124 | | - |
125 | | - /* Read data using an outbound tcp connection */ |
126 | | - { |
127 | | - Socket socket = null; |
128 | | - BufferedReader readerBuffered = null; |
129 | | - InputStreamReader readerInputStream = null; |
130 | | - |
131 | | - try { |
132 | | - /* Read data using an outbound tcp connection */ |
133 | | - socket = new Socket("host.example.org", 39544); |
134 | | - |
135 | | - /* read input from socket */ |
136 | | - |
137 | | - readerInputStream = new InputStreamReader(socket.getInputStream(), "UTF-8"); |
138 | | - readerBuffered = new BufferedReader(readerInputStream); |
139 | | - |
140 | | - /* POTENTIAL FLAW: Read data using an outbound tcp connection */ |
141 | | - String stringNumber = readerBuffered.readLine(); |
142 | | - if (stringNumber != null) // avoid NPD incidental warnings |
143 | | - { |
144 | | - try { |
145 | | - data = Float.parseFloat(stringNumber.trim()); |
146 | | - } catch (NumberFormatException exceptNumberFormat) { |
147 | | - IO.writeLine("Number format exception parsing data from string"); |
148 | | - } |
149 | | - } |
150 | | - } catch (IOException exceptIO) { |
151 | | - IO.writeLine("Error with stream reading"); |
152 | | - } finally { |
153 | | - /* clean up stream reading objects */ |
154 | | - try { |
155 | | - if (readerBuffered != null) { |
156 | | - readerBuffered.close(); |
157 | | - } |
158 | | - } catch (IOException exceptIO) { |
159 | | - IO.writeLine("Error closing BufferedReader"); |
160 | | - } |
161 | | - |
162 | | - try { |
163 | | - if (readerInputStream != null) { |
164 | | - readerInputStream.close(); |
165 | | - } |
166 | | - } catch (IOException exceptIO) { |
167 | | - IO.writeLine("Error closing InputStreamReader"); |
168 | | - } |
169 | | - |
170 | | - /* clean up socket objects */ |
171 | | - try { |
172 | | - if (socket != null) { |
173 | | - socket.close(); |
174 | | - } |
175 | | - } catch (IOException exceptIO) { |
176 | | - IO.writeLine("Error closing Socket"); |
177 | | - } |
178 | | - } |
179 | | - } |
180 | | - |
181 | | - /* FIX: Check for value of or near zero before dividing */ |
182 | | - if (Math.abs(data) > 0.000001) { |
183 | | - int result = (int) (100.0 / data); |
184 | | - IO.writeLine(result); |
185 | | - } else { |
186 | | - IO.writeLine("This would result in a divide by zero"); |
187 | | - } |
188 | | - } |
189 | | - |
190 | | - /* Below is the main(). It is only used when building this testcase on |
191 | | - * its own for testing or for building a binary to use in testing binary |
192 | | - * analysis tools. It is not used when compiling all the testcases as one |
193 | | - * application, which is how source code analysis tools are tested. |
194 | | - */ |
195 | | - public static void main(String[] args) throws Throwable { |
196 | | - Main m = new Main(); |
197 | | - m.bad(); |
198 | | - } |
199 | | -} |
| 1 | +/* Copyright 2020, TU Dortmund, Malte Mues ([email protected]) |
| 2 | +This testcase is derived from the following File in the Juliet Benchmark found at: |
| 3 | +https://samate.nist.gov/SARD/testsuite.php in Version 1.3 |
| 4 | +Modifications are licenced under CC0 licence. |
| 5 | +
|
| 6 | +The original file is: |
| 7 | +Filename: CWE369_Divide_by_Zero__float_connect_tcp_divide_01.java |
| 8 | +Label Definition File: CWE369_Divide_by_Zero__float.label.xml |
| 9 | +Template File: sources-sinks-01.tmpl.java |
| 10 | +
|
| 11 | +It is renamed to Main.java according to SV-Comp rules. |
| 12 | +*/ |
| 13 | + |
| 14 | +/* |
| 15 | + * @description |
| 16 | + * CWE: 369 Divide by zero |
| 17 | + * BadSource: connect_tcp Read data using an outbound tcp connection |
| 18 | + * GoodSource: A hardcoded non-zero number (two) |
| 19 | + * Sinks: divide |
| 20 | + * GoodSink: Check for zero before dividing |
| 21 | + * BadSink : Dividing by a value that may be zero |
| 22 | + * Flow Variant: 01 Baseline |
| 23 | + * |
| 24 | + * */ |
| 25 | + |
| 26 | +import java.io.IOException; |
| 27 | +import java.io.InputStreamReader; |
| 28 | +import java.net.Socket; |
| 29 | +import testcasesupport.*; |
| 30 | + |
| 31 | +public class Main { |
| 32 | + public void bad() throws Throwable { |
| 33 | + float data; |
| 34 | + |
| 35 | + data = -1.0f; /* Initialize data */ |
| 36 | + |
| 37 | + /* Read data using an outbound tcp connection */ |
| 38 | + { |
| 39 | + Socket socket = null; |
| 40 | + BufferedReader readerBuffered = null; |
| 41 | + InputStreamReader readerInputStream = null; |
| 42 | + |
| 43 | + try { |
| 44 | + /* Read data using an outbound tcp connection */ |
| 45 | + socket = new Socket("host.example.org", 39544); |
| 46 | + |
| 47 | + /* read input from socket */ |
| 48 | + |
| 49 | + readerInputStream = new InputStreamReader(socket.getInputStream(), "UTF-8"); |
| 50 | + readerBuffered = new BufferedReader(readerInputStream); |
| 51 | + |
| 52 | + /* POTENTIAL FLAW: Read data using an outbound tcp connection */ |
| 53 | + String stringNumber = readerBuffered.readLine(); |
| 54 | + if (stringNumber != null) // avoid NPD incidental warnings |
| 55 | + { |
| 56 | + try { |
| 57 | + data = Float.parseFloat(stringNumber.trim()); |
| 58 | + } catch (NumberFormatException exceptNumberFormat) { |
| 59 | + IO.writeLine("Number format exception parsing data from string"); |
| 60 | + } |
| 61 | + } |
| 62 | + } catch (IOException exceptIO) { |
| 63 | + IO.writeLine("Error with stream reading"); |
| 64 | + } finally { |
| 65 | + /* clean up stream reading objects */ |
| 66 | + try { |
| 67 | + if (readerBuffered != null) { |
| 68 | + readerBuffered.close(); |
| 69 | + } |
| 70 | + } catch (IOException exceptIO) { |
| 71 | + IO.writeLine("Error closing BufferedReader"); |
| 72 | + } |
| 73 | + |
| 74 | + try { |
| 75 | + if (readerInputStream != null) { |
| 76 | + readerInputStream.close(); |
| 77 | + } |
| 78 | + } catch (IOException exceptIO) { |
| 79 | + IO.writeLine("Error closing InputStreamReader"); |
| 80 | + } |
| 81 | + |
| 82 | + /* clean up socket objects */ |
| 83 | + try { |
| 84 | + if (socket != null) { |
| 85 | + socket.close(); |
| 86 | + } |
| 87 | + } catch (IOException exceptIO) { |
| 88 | + IO.writeLine("Error closing Socket"); |
| 89 | + } |
| 90 | + } |
| 91 | + } |
| 92 | + |
| 93 | + /* POTENTIAL FLAW: Possibly divide by zero */ |
| 94 | + int result = (int) (100.0 / data); |
| 95 | + if (1 < data || data <= 0) { |
| 96 | + assert result < 100; |
| 97 | + } |
| 98 | + |
| 99 | + IO.writeLine(result); |
| 100 | + } |
| 101 | + |
| 102 | + public void good() throws Throwable { |
| 103 | + goodG2B(); |
| 104 | + goodB2G(); |
| 105 | + } |
| 106 | + |
| 107 | + /* goodG2B() - use goodsource and badsink */ |
| 108 | + private void goodG2B() throws Throwable { |
| 109 | + float data; |
| 110 | + |
| 111 | + /* FIX: Use a hardcoded number that won't a divide by zero */ |
| 112 | + data = 2.0f; |
| 113 | + |
| 114 | + /* POTENTIAL FLAW: Possibly divide by zero */ |
| 115 | + int result = (int) (100.0 / data); |
| 116 | + IO.writeLine(result); |
| 117 | + } |
| 118 | + |
| 119 | + /* goodB2G() - use badsource and goodsink */ |
| 120 | + private void goodB2G() throws Throwable { |
| 121 | + float data; |
| 122 | + |
| 123 | + data = -1.0f; /* Initialize data */ |
| 124 | + |
| 125 | + /* Read data using an outbound tcp connection */ |
| 126 | + { |
| 127 | + Socket socket = null; |
| 128 | + BufferedReader readerBuffered = null; |
| 129 | + InputStreamReader readerInputStream = null; |
| 130 | + |
| 131 | + try { |
| 132 | + /* Read data using an outbound tcp connection */ |
| 133 | + socket = new Socket("host.example.org", 39544); |
| 134 | + |
| 135 | + /* read input from socket */ |
| 136 | + |
| 137 | + readerInputStream = new InputStreamReader(socket.getInputStream(), "UTF-8"); |
| 138 | + readerBuffered = new BufferedReader(readerInputStream); |
| 139 | + |
| 140 | + /* POTENTIAL FLAW: Read data using an outbound tcp connection */ |
| 141 | + String stringNumber = readerBuffered.readLine(); |
| 142 | + if (stringNumber != null) // avoid NPD incidental warnings |
| 143 | + { |
| 144 | + try { |
| 145 | + data = Float.parseFloat(stringNumber.trim()); |
| 146 | + } catch (NumberFormatException exceptNumberFormat) { |
| 147 | + IO.writeLine("Number format exception parsing data from string"); |
| 148 | + } |
| 149 | + } |
| 150 | + } catch (IOException exceptIO) { |
| 151 | + IO.writeLine("Error with stream reading"); |
| 152 | + } finally { |
| 153 | + /* clean up stream reading objects */ |
| 154 | + try { |
| 155 | + if (readerBuffered != null) { |
| 156 | + readerBuffered.close(); |
| 157 | + } |
| 158 | + } catch (IOException exceptIO) { |
| 159 | + IO.writeLine("Error closing BufferedReader"); |
| 160 | + } |
| 161 | + |
| 162 | + try { |
| 163 | + if (readerInputStream != null) { |
| 164 | + readerInputStream.close(); |
| 165 | + } |
| 166 | + } catch (IOException exceptIO) { |
| 167 | + IO.writeLine("Error closing InputStreamReader"); |
| 168 | + } |
| 169 | + |
| 170 | + /* clean up socket objects */ |
| 171 | + try { |
| 172 | + if (socket != null) { |
| 173 | + socket.close(); |
| 174 | + } |
| 175 | + } catch (IOException exceptIO) { |
| 176 | + IO.writeLine("Error closing Socket"); |
| 177 | + } |
| 178 | + } |
| 179 | + } |
| 180 | + |
| 181 | + /* FIX: Check for value of or near zero before dividing */ |
| 182 | + if (Math.abs(data) > 0.000001) { |
| 183 | + int result = (int) (100.0 / data); |
| 184 | + IO.writeLine(result); |
| 185 | + } else { |
| 186 | + IO.writeLine("This would result in a divide by zero"); |
| 187 | + } |
| 188 | + } |
| 189 | + |
| 190 | + /* Below is the main(). It is only used when building this testcase on |
| 191 | + * its own for testing or for building a binary to use in testing binary |
| 192 | + * analysis tools. It is not used when compiling all the testcases as one |
| 193 | + * application, which is how source code analysis tools are tested. |
| 194 | + */ |
| 195 | + public static void main(String[] args) throws Throwable { |
| 196 | + Main m = new Main(); |
| 197 | + m.bad(); |
| 198 | + } |
| 199 | +} |
0 commit comments