replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Update regression tests 

Not-null annotation check properties which are added to the beginning of
the method's goto inherit the source_locationt of the method. Because
previously the location had missing information (missing method name),
the property name looked like this:
[not-null-annotation-check.1]

Now the name looks like this:
[java::Main.bar:(Ljava/lang/Integer;ZLjava/lang/Object;[Ljava/lang/String;)Ljava/lang/Integer;.not-null-annotation-check.1]
This commit is contained in:
svorenova 2019-07-11 16:08:26 +01:00
parent e240abb783
commit bffa37f9f7
3 changed files with 6 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
jbmc/regression/jbmc/parameter-annotation-not-null/test_array.desc
View File

@ -4,7 +4,7 @@ Main.class
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
\[not-null-annotation-check\.1\] line \d+ Not null annotation check: FAILURE
\[not-null-annotation-check\.2\] line \d+ Not null annotation check: SUCCESS
\[java::Main\.bar:\(Ljava/lang/Integer;ZLjava/lang/Object;\[Ljava/lang/String;\)Ljava/lang/Integer;\.not-null-annotation-check\.1\] line \d+ Not null annotation check: FAILURE
\[java::Main\.bar:\(Ljava/lang/Integer;ZLjava/lang/Object;\[Ljava/lang/String;\)Ljava/lang/Integer;\.not-null-annotation-check\.2\] line \d+ Not null annotation check: SUCCESS
--
^warning: ignoring

4
jbmc/regression/jbmc/parameter-annotation-not-null/test_object.desc
View File

@ -4,7 +4,7 @@ Main.class
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
\[not-null-annotation-check\.1\] line \d+ Not null annotation check: SUCCESS
\[not-null-annotation-check\.2\] line \d+ Not null annotation check: FAILURE
\[java::Main\.foo:\(Ljava/lang/Integer;ZLjava/lang/Object;\[Ljava/lang/String;\)Ljava/lang/Integer;\.not-null-annotation-check\.1\] line \d+ Not null annotation check: SUCCESS
\[java::Main\.foo:\(Ljava/lang/Integer;ZLjava/lang/Object;\[Ljava/lang/String;\)Ljava/lang/Integer;\.not-null-annotation-check\.2\] line \d+ Not null annotation check: FAILURE
--
^warning: ignoring

4
jbmc/regression/jbmc/parameter-annotation-not-null/test_success.desc
View File

@ -4,7 +4,7 @@ Main.class
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
\[not-null-annotation-check\.1\] line \d+ Not null annotation check: SUCCESS
\[not-null-annotation-check\.2\] line \d+ Not null annotation check: SUCCESS
\[java::Main\.foo:\(Ljava/lang/Integer;ZLjava/lang/Object;\[Ljava/lang/String;\)Ljava/lang/Integer;\.not-null-annotation-check\.1\] line \d+ Not null annotation check: SUCCESS
\[java::Main\.foo:\(Ljava/lang/Integer;ZLjava/lang/Object;\[Ljava/lang/String;\)Ljava/lang/Integer;\.not-null-annotation-check\.2\] line \d+ Not null annotation check: SUCCESS
--
^warning: ignoring