RE: [Javapathfinder-user] Verify.ignoreIf does not work

[Willem V. <wv...@em...>]

The implementation in the Verify class is empty, since that is just used
as a trap for the model checker to react to - if you look in the
JPF_gov_nasa_jpf_jvm_Verify.java file in the same directory (i.e. the
native peer of the Verify class that actually gets executed) you'll see
the true body of the ignoreIf method. If you still don't believe me that
it really prunes the state space put an assert false right after a
ignoreif true and see if it ever gets triggered :-)
 
 
 
--
Willem C. Visser                 Automated Software Engineering Group
RIACS/NASA Ames Research Center            wv...@em...
M/S 269-2                                     http://ase.arc.nasa.gov
Moffett Field, CA 94035                (650)604-3515 fax 4036  rm 235
-----Original Message-----
From: jav...@li...
[mailto:jav...@li...] On Behalf Of
zuo jihong
Sent: Sunday, December 18, 2005 10:19 PM
To: Jav...@li...
Subject: [Javapathfinder-user] Verify.ignoreIf does not work
 
Hi, I encounter a problem when instrumenting code with Verify. The code
is to simulate a user action. For example, 
       Address item = pickAddress();
       if (item != null) {
              Verify.ignoreIf(item.isEqual(Address.Remailer));
              forwMsg.setForwardItem(item);
       }
 
According to the doc on the web, Verify.ignoreIf can prune state search.
"If the provided expression evaluates to true, JPF does not continue to
execute the current path, and backtracks to the previous
non-deterministic choice point."
However, it is not the fact. As I traced into the execution I found that
Verify.ignoreIf() is only an empty function. Nothing happens when the
expression evaluates to true. Then, how can I implement search pruning
and backtracking in my code?
 
J.H. Zuo