From 971a34b35a47e28e9b9721fbc6a69d2309c901d5 Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Fri, 1 Jun 2018 11:16:03 +0100 Subject: [PATCH 1/2] Always load cprover-nondet-initialize --- jbmc/src/java_bytecode/ci_lazy_methods.cpp | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/jbmc/src/java_bytecode/ci_lazy_methods.cpp b/jbmc/src/java_bytecode/ci_lazy_methods.cpp index 413f8b3c709..667447bc983 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods.cpp +++ b/jbmc/src/java_bytecode/ci_lazy_methods.cpp @@ -248,6 +248,17 @@ bool ci_lazy_methodst::operator()( } } + // cproverNondetInitialize has to be force-loaded for mocks to return valid + // objects (objects which satisfy invariants specified in the + // cproverNondetInitialize method) + for(const auto &class_name : instantiated_classes) + { + const irep_idt cprover_validate = + id2string(class_name) + ".cproverNondetInitialize:()V"; + if(symbol_table.symbols.count(cprover_validate)) + methods_already_populated.insert(cprover_validate); + } + // Remove symbols for methods that were declared but never used: symbol_tablet keep_symbols; // Manually keep @inflight_exception, as it is unused at this stage From a673e5dbc132c734ca833b891505da803d2dc691 Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Mon, 4 Jun 2018 13:15:36 +0100 Subject: [PATCH 2/2] Add test verifying that the cproverNondetInitialize method is always loaded Test is disabled because of test-runner problems described in the following issue: https://github.com/diffblue/cbmc/pull/2267 --- .../ObjectWithNondetInitialize.class | Bin 0 -> 478 bytes .../ObjectWithNondetInitialize.java | 11 +++++++++++ .../Opaque.java | 7 +++++++ .../Test.class | Bin 0 -> 363 bytes .../Test.java | 5 +++++ .../test.desc | 11 +++++++++++ 6 files changed, 34 insertions(+) create mode 100644 jbmc/regression/jbmc/cprover-always-load-nondet-initialize/ObjectWithNondetInitialize.class create mode 100644 jbmc/regression/jbmc/cprover-always-load-nondet-initialize/ObjectWithNondetInitialize.java create mode 100644 jbmc/regression/jbmc/cprover-always-load-nondet-initialize/Opaque.java create mode 100644 jbmc/regression/jbmc/cprover-always-load-nondet-initialize/Test.class create mode 100644 jbmc/regression/jbmc/cprover-always-load-nondet-initialize/Test.java create mode 100644 jbmc/regression/jbmc/cprover-always-load-nondet-initialize/test.desc diff --git a/jbmc/regression/jbmc/cprover-always-load-nondet-initialize/ObjectWithNondetInitialize.class b/jbmc/regression/jbmc/cprover-always-load-nondet-initialize/ObjectWithNondetInitialize.class new file mode 100644 index 0000000000000000000000000000000000000000..ee136a7e1c393b33b0083846625ead65f8d5deae GIT binary patch literal 478 zcmZ`#OH0E*5dJog#>T|H)M`ca*!Ey9UIY=LAQZF;l?q;Dn=W;0nv^u@!C&Leix)vq zJop3rQQ~YYqJoE=nVtO}v-AG(`UYSZ8#YXo^Dt1cv5XZ9s}`yZxfu^qamB#eblI1o zOb!_IdZWi+w4#AvC>+aBbkcEO#OJ&pP^aoo;%Fw~P81GA(k71NfxM*`x0`VP=7dk? zNHdeq1WDiSMrrJeBdJ8TPWvO_Cl@lg{;RVy;xq1G0eJ^GSQgeCtfR(I`=7&5R4gyx z;n4enF;t>>=*@@qT4&kN^i4jUrehkxs9!dE*ruhJv?K;ixlyIlA#>{3RBcjbl+ETd z*drATixhKNQ>W;BL-$BRLCei2Xhru9mT?b5e}S%eTE?>}D|U&jT&hfH?xAv6LV@CM RN0NCU%uh!(Rxwj6eF6`8SW*B0 literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/cprover-always-load-nondet-initialize/ObjectWithNondetInitialize.java b/jbmc/regression/jbmc/cprover-always-load-nondet-initialize/ObjectWithNondetInitialize.java new file mode 100644 index 00000000000..e9660b876cb --- /dev/null +++ b/jbmc/regression/jbmc/cprover-always-load-nondet-initialize/ObjectWithNondetInitialize.java @@ -0,0 +1,11 @@ +import org.cprover.CProver; + +class ObjectWithNondetInitialize { + private int value_; + public void cproverNondetInitialize() { + CProver.assume(value_ == 13); + } + public int value() { + return value_; + } +} diff --git a/jbmc/regression/jbmc/cprover-always-load-nondet-initialize/Opaque.java b/jbmc/regression/jbmc/cprover-always-load-nondet-initialize/Opaque.java new file mode 100644 index 00000000000..616c1ff6bb2 --- /dev/null +++ b/jbmc/regression/jbmc/cprover-always-load-nondet-initialize/Opaque.java @@ -0,0 +1,7 @@ +import org.cprover.CProver; + +public class Opaque { + public ObjectWithNondetInitialize get() { + return new ObjectWithNondetInitialize(); + } +} diff --git a/jbmc/regression/jbmc/cprover-always-load-nondet-initialize/Test.class b/jbmc/regression/jbmc/cprover-always-load-nondet-initialize/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..a809eb786c47307c7cd0cee2d96442f100f60267 GIT binary patch literal 363 zcmZ`!Jxc>o5S+bFb6%43TO$fKA+a!xonj*hfshmi#qwRU#23yxjdv;hO*S?ODEI^X zQR2R{6Wn66H7$L(H?GiW6a+oS*a3)g=ViSuq>&l{QLcD9XuH%~gmMR3vinsGbTAv4dS7 zdm$RAN`SEuB4g|%DxGu&@svjw1db4^(wvyEUNzXRzc-927{-sC}874%BdNFl0%#@Z}Lf!YVGyCv)eoCVz1KQp$t JYr