Re: [rvm-research] Jikes RVM and Java Runtime library
Erik Brangs <[email protected]>
| Newsgroups | gmane.comp.java.jikes.rvm.devel |
|---|---|
| Message-ID | <[email protected]> |
Hi, On 03.03.2014 18:59, Pascal Kesseli wrote: > We’re trying to extend our bounded model checker CBMC by a Java frontend. Obviously there are a lot of things to be considered before this can work, and one of those would be how to model native operations in the Java Runtime library. If you haven't done so already, you could try to take a look at Java Path Finder ( http://babelfish.arc.nasa.gov/trac/jpf ) to see how they deal with this issue. > An obvious choice would be to model them [native operations in the class library] using JNI and the JDK source code. [...] Does Jikes feature Java implementations of all these operations? In general, the Jikes RVM does not modify native methods in the class libraries. There are a few exceptions but most native operations stay native. Kind regards, Erik Brangs ------------------------------------------------------------------------------ Subversion Kills Productivity. Get off Subversion & Make the Move to Perforce. With Perforce, you get hassle-free workflows. Merge that actually works. Faster operations. Version large binaries. Built-in WAN optimization and the freedom to use Git, Perforce or both. Make the move to Perforce. http://pubads.g.doubleclick.net/gampad/clk?id=122218951&iu=/4140/ostg.clktrk