Skip to content

Commit 8082795

Browse files
Add test checking that string content is declared before being allocated
1 parent 280c45b commit 8082795

File tree

3 files changed

+18
-0
lines changed

3 files changed

+18
-0
lines changed
Binary file not shown.
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
test.class
3+
--refine-strings --show-goto-functions
4+
// Enable multi-line checking
5+
activate-multi-line-match
6+
EXIT=0
7+
SIGNAL=0
8+
char \([*]malloc_site.[0-9]*\)\[INFINITY\(\)\];\n\s*//.*\n\s*malloc_site.[0-9]*\s*=\s*MALLOC\(char \[INFINITY\(\)\], 2ull? \* INFINITY\(\)\);\n\s*//.*\n\s*cprover_string_array.[0-9]*\s*=\s*malloc_site.\d*;
9+
--
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
public class test
2+
{
3+
public static void check()
4+
{
5+
String s = new String("foo");
6+
String t = new String("bar");
7+
String u = s.concat(t);
8+
}
9+
}

0 commit comments

Comments
 (0)