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

Disable lazy loading opaque return for symex driven loading

This commit is contained in:
thk123 2018-06-13 09:20:09 +01:00
parent 409d892d42
commit d7d5f63529
1 changed files with 2 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
jbmc/regression/jbmc/lazyloading_opaquereturn/test.desc
View File

@ -1,4 +1,4 @@
CORE CORE symex-driven-lazy-loading-expected-failure
TestClass.class TestClass.class
--function TestClass.testFunction --lazy-methods --verbosity 10 --function TestClass.testFunction --lazy-methods --verbosity 10
CI lazy methods: elaborate java::Foo\.cproverNondetInitialize:\(\)V CI lazy methods: elaborate java::Foo\.cproverNondetInitialize:\(\)V
@ -10,3 +10,4 @@ CI lazy methods: elaborate java::GenFiller\.cproverNondetInitialize:\(\)V
Testing that the return type of an opaque method is correctly elaborated. The Testing that the return type of an opaque method is correctly elaborated. The
cproverNondetInitialize should be loaded for all classes where an instance might cproverNondetInitialize should be loaded for all classes where an instance might
be seen. be seen.
This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods