Skip to content

Commit 5cfa413

Browse files
Adding test to check that data field of strings are set in json
1 parent f4fa778 commit 5cfa413

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,10 @@
1+
CORE
2+
test.class
3+
--refine-strings --function test.check --json-ui --trace --string-max-length 100 --cover location
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
\"data\".*\"tmp_object_factory\$6.*\"
7+
--
8+
This checks that tmp_object_factory$6 gets affected to the data field
9+
of some strings, which was not the case in previous versions of cbmc,
10+
as it was just ignored by the json output.
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
public class test
2+
{
3+
public static int check(String s)
4+
{
5+
int i=Integer.parseInt(s);
6+
return i;
7+
}
8+
}

0 commit comments

Comments
 (0)