User Manual
Contents
1. will be used when reporting execution history If not specified the history might be empty m lt methodname gt Name of a single method to be checked By de fault all methods from a class are checked c lt filename gt Path to a JPF configuration file All default JPF configuration parameters will be overriden with values from this file e Do not print the execution history when an error occurs by default the history is printed a Trace also the standard Java libraries when an er ror occurs by default the Java libraries are not traced d Print bytecode intructions in the execution his tory by default bytecode is not printed j Do not filter JUnit and UnitCheck code out of the execution history by default the filtering is on b lt dirname gt The base directory of UnitCheck You will hardly ever need this option it is set by wrapper scripts w Do not stop checking when an error occurs It is not recommended to use this option The typical command for running UnitCheck follows unitcheck p mydir myproject classes s mydir myproject src SE C4 4 OO TSSL CHAPTER 1 USER S MANUAL 1 2 ECLIPSE PLUGIN 1 2 Eclipse Plugin 1 2 1 Installation The plugin requires Eclipse IDE 3 4 or higher it was successfully tested with versions 3 4 1 and 3 5M6 The plugin cannot be used with the version 3 3 or lower because it requires API that is not available in these old versions2. Before you can start using the plugin it is necessary to properly install it to your Eclipse IDE In order to do so you have to access so called update site This can be done in two ways e either you use the UnitCheck plugin update site at http aiya ms mff c uni cz unitchecking plugin e or you use the local update site archive which you might e g build from the plugin sources In either case follow these steps 1 Open the Software Updates and Add ons dialog by selecting Help Software Up dates from the main menu 2 Choose the Available Software tab 3 Click Add Site to define the update site If you want to use the UnitCheck plugin update site enter the URL of the site in the Location box Click OK to confirm In case you have the local update site archive file named unitcheck eclipse plugin r where stands for the revision number choose Archive and in the displayed dialog select the file Click OK to confirm 4 Eclipse connects to the update site and offers you the features provided by the site Check the UnitCheck Eclipse Plugin feature and click Install 5 In order to use the plugin you have to agree with its license and continue by selecting Finish 6 After the plugin is installed acknowledge the Eclipse restart The plugin can be uninstalled using the same Software Updates and Add ons dialog select Help Software Updates from the main menu In the first Installed Software tab select U
3. UnitCheck task for checking sam ple tests Before the task can be used it must be properly defined in a build file as Exam ple L1 shows The task depends on a couple of JAR files located in its 1ib directory According to Ant guidelines this way of defining task s dependencies is more flexible than using Ant s global 1ib directory CHAPTER 1 USER S MANUAL 1 3 ANTTASK Example 1 1 UnitCheck task definition amp usage S Pani wsiesao er 0M 2 lt project name myproject default mytarget basedir gt lt property name unitcheck task dir oeas len W unmieecheck ant task clanter MEU lt path id unitcheckcp gt lt fileset dir unitcheck task dir includes jar gt lt path gt lt taskdef name unitcheck classname cz kebrt unitcheck ant UnitCheckTask classpathref unitcheckcp gt lt target name mytarget gt lt property name proj dir location project daisy gt lt unskecheeksbasscher US numa ne Cleese k cr lt vmclasspath gt lt pathelement path proj dir classes gt lt vmclasspath gt lt vmsourcepath path proj dir src proj dir testsrc gt lt jpfproperty key jpf listener value daisy jpf DaisyLockOrderProperty gt SPIproeperey key lseareh properciesl value gov nasa jpf jvm NoUncaughtExceptionsProperty gt lt test class daisy unittest CreatFileTest method testCreatFile gt lt test class daisy unittest CreatFileTest met
4. 0 racer d 4 cz kebrt test Racer Racer java 34 Thread sleep n iload_o 2l invokestatic java lang Thread sleep J V cz kebrt test Racer Racer java 34 Thread sleep n goto 5 N cz kebrt test Racer Racer java 37 return cz kebrt test Racer doSomething I V 4 gt Transitions in the grid are coloured differently those executed by the same thread are coloured with the same background colour When a transition is selected all other transitions that were executed by the same thread are highlighted in bold User can use either the keyboard arrows to move in the grid or arrow buttons in top upper corner of the view The arrows marked with T jump only between transitions executed by the same thread Three other view buttons allow to e show bytecode instructions along with the source code listing e trace standard Java libraries can be combined with the previous button e search the code listing 1 3 Ant Task For better integration of UnitCheck into existing projects the Ant task is also provided This task should always be preferred to command line program because it offers more convenient way of running JUnit under JPF After extracting unitcheck ant task rev zip the following structure will appear e lib contains taks s binary code as well its dependencies in the form of JAR files e srcand classes can be used for looking at example JUnit tests e examples contain Ant build files that use the
5. UnitCheck User s Manual Michal Kebrt Prague April 2009 Contents 1 User s manual 1 1 Command line Tool 1 2 Eclipse Plugin ss 4 9 u 624 1 2 1 Installation 1 2 3 Result of Checking 1 2 4 Inspecting Error Traces 1 3 Ant Task NO CON SO O1 01 Listings N zev pr ce Unit Checking for Java IDE Autor Michal Kebrt Katedra Katedra softwarov ho in en rstv Vedouc diplomov pr ce RNDr Ond ej er E mail vedouc ho ondrej sery dsrg mff cuni cz Abstrakt Kl ov slova unit testing model checking JUnit Java PathFinder Eclipse Title Unit Checking for Java IDE Author Michal Kebrt Department Department of Software Engineering Supervisor RNDr Ond ej er Supervisor s e mail address ondrej sery dsrg mff cuni cz Abstract Keywords unit testing model checking JUnit Java PathFinder Eclipse Chapter 1 User s manual 1 1 Command line Tool Executable programs can be found in the unitcheck bin directory unitcheck for Unix environments and TODO for Windows The following options are recognized the bold ones are required t lt classname gt JUnit test class to be checked fully qualified class name must be used p lt pathl gt lt path2 gt Colon separated list of classpath elements that will be used by JPF VM for checking a test class s lt pathl gt lt path2 gt Colon separated list of sourcepath elements that
6. hod testCreatLongFilename gt lt batchtest gt lt fileset dir proj dir gt lt include name xx xTest java gt lt fileset gt lt batchtest gt lt unitcheck gt lt target gt Project The unitcheck task has the following attributes and subelements the bold ones are reguired Attribute name Default Description basedir UnitCheck task s 1ib directory The same di rectory was used in the task definition 10 CHAPTER 1 USER S MANUAL 1 3 ANTTASK Attribute name Default Description vmclasspathref Reference to a classpath that will be used by JPF VM when checking The vmclasspath element can be used instead vmsourcepathref Reference to a sourcepath that will be used by JPF VM when reporting errors If not specified the execution history might be empty The v msourcepath element can be used instead conffile Path to a JPF configuration file All default JPF configuration parameters will be overri den with values from this file The jpfpro perty elements can be used instead printpath true Print the execution history path when an er ror occurs printbytecode false Print the bytecode intructions along with the execution history filterjunittrace true Filter the JUnit and UnitCheck code out of the execution history tracejre false Trace the standard Java libraries in the execu tion history Element na
7. java Wih gt Run Configurations ompare Wi b kebrt test1 wem a Replace With e Ifa test class is opened in the Java editor one may right click the source code and select Run As UnitCheck Only this single test class will be checked e The last way of running uses configurations that can be reached by selecting Run Run Configurations from the main menu In the dialog right the UnitCheck category and select New which creates a new run configuration The Main tab defines tests to be checked as Figure l 2 illustrates Either a single test class can be checked First a Java project must be selected using the Browse button and after clicking the Search button a list of all classes from the project containing at least one JUnit test will be displayed Only the selected class will be then checked Or all tests from selected project or package can be checked After clicking the Select button the tree of all projects and packages containing at least one JUnit test will be displayed JPF properties overriding default JPF properties can be specified in the textbox Each one is written in a single row in the form of lt prop_name gt lt prop_value gt An example of a propery is jpf listener for defining custom JPF listeners used when checking You will hardly ever need to change anything in the standard Eclipse run tabs Classpath Source and Common Classpath and sourcepath are based on the particular Java project
8. me Description vmclasspath Classpath that will be used by JPF VM when checking All standard Ant constructs for creatings path like structures can be used within the element The vmclasspathref attribute can be used instead vmsourcepath Sourcepath that will be used by JPF VM when reporting er rors If not specified the execution history might be empty All standard Ant constructs for creatings path like structures can be used within the element The vmsourcepathref at tribute can be used instead jpfproperty Allows to override default JPF configuration parameters Each property has the key and value attributes test Defines a JUnit test to be checked Each test must have a test class assigned The method attribute allows to specify only a single test method otherwise all test methods within the class will be checked batchtest More tests to be checked can be specified using this element All standard Ant constructs for defining filesets can be used within the element Only the java and class files will be taken into account 2 Remember that the classpath containing the test and its dependencies must be configured using vmclasspath or vmclasspathref 11
9. meticException division by zero 1 2 4 Inspecting Error Traces This section applies only for situations where a test finished with an error In such case the Path view can be used for detecting reasons that led to the error In general the view displays the execution history provided by JPF but in more convenient way than the command line program The execution history or path in other words is split into a set of transitions which are listed in the left part of the view in a grid The right part shows detailed information about the selected transition Each transition is a result of so called choice in JPF the choice usually produces more transitions as JPF backtracks to the choice point again and again Therefore the user can see the following data about each transition e Number of the thread that executed the transition e Type of the choice e g selection from a set of threads to be executed Additional information about the choice e g which thread was selected e Instruction that caused a choice to be created i e the choice point Number of the choice in the choice point in the form of choice_number choice_total CHAPTER 1 USER S MANUAL 1 3 ANTTASK Figure 1 4 Path view V Path amp El Console eo P Es AD 0 2 Thread 1 Choice Type gov nasa jpf jvm choice ThreadChoiceFromSet 3 Choice No 2 2 Choice Info gov nasa jpf jvm choice ThreadChoicefromSet main gt Thread 0 Choice Insn int c 42
10. nitCheck Eclipse Plugin item and click the Uninstall button After you confirm that you agree with uninstallation the plugin will be removed from your Eclipse IDE The plugin consists of two views that can be shown by opening the Window Show View Other dialog and selecting the views in the UnitCheck category You can place the views on your favourite locations in the Eclipse IDE Both views will be described in next sections Applies only to Eclipse 3 4 the plugin management is a little bit different in Eclipse 3 5 CHAPTER 1 USER S MANUAL 1 2 ECLIPSE PLUGIN 1 2 2 Running There are a couple of ways how to run UnitCheck on a selected JUnit test or a set of tests e One can right click a single test directory or a whole project in the Package Ex plorer and select Run As UnitCheck as Figure 1 1 shows The UnitCheck run op tion is displayed only for items that contain at least one JUnit test All test classes within selected element will then be checked Figure 1 1 Running UnitCheck from Package Explorer l Package Explorer 23 A D Racerjava E Sly package cz kebrt test gt 3 daisy import org junit Test gt elib 7 ublic class Racer implements Runnable publ l Ra l ts Runnable v tests v Bsrc int d 42 v cz kebrt test ag public void run gt DD dl ki lm C n nt hs nal O a LA 1 N Deadlock java New gt b D Lock java b N Simple java Dany A gt Team gt z 3 gt D Simplel
11. or The second part of the view contains more information about checking results of a selected test method In case an error was detected by UnitChecker three buttons for showing detailed information are displayed The first button called Show Exception is enabled only for errors that were caused by an uncaught exception it is disabled for violations of JPF properties After clicking the button the exception stracktrace is printed in the Path view which will be described in the next section in more details The Show Path and Show Snapshot buttons allow to read the complete execution history leading to the error and the state of all threads at the moment the error occured A short of summary of the error can be found in the textbox below the buttons The right upper corner of the view contains a couple of buttons for manipulating with the tree of test classes The buttons allow to expand and collapse all tree items e stop checking CHAPTER 1 USER S MANUAL 1 2 ECLIPSE PLUGIN e rerun the previous checking e show only test methods that finished with an error Figure 1 3 Check Summary view H Package Expl W Check Summ amp gt O IE v E cz kebrt test Racer b Ei cz kebrt test Lock J FF FF Er cz kebrt test Simple1 J 4 cz kebrt test Simple E hello rs verify Check count 3 Error count 1 Status Finished Show Exception M Show Path Show Snapshot java lang Arith
12. s settings and are passed to JPF VM If the configuration is ok the Run button starts checking of selected test classes CHAPTER 1 USER S MANUAL 1 2 ECLIPSE PLUGIN Figure 1 2 Running UnitCheck from Run Configurations e Run Configurations Create manage and run configurations BEK E x i K Name DirCreatTest1 type filter text Main gt Classpath amp Source Common Eclipse Application Fl Java Applet Check single test Project daisy Browse I Java Application b Ju JUnit Test class daisy unittest DirCreatTest1 Ju JUnit Plug in Test OSGi Framework O Check all tests from selected project or package v W UnitCheck W cz kebrt test v W Racer Select JPF properties jpf listener daisy jpf DaisyDirCreatProperty Apply Revert Filter matched 11 of 11 iter Run Close 1 2 3 Result of Checking After the checking is started the Console view will contain the same output as the equivalent launch of the command line UnitCheck program The Check Summary view incrementally displays classes that were checked in the current run The view is split into two parts as Figure 1 3 shows The first one contains the tree of all classes that were checked Each class comprises of a list of test methods with icons indicating whether the checking of the particular method finished success fully or not Double clicking any item in the tree opens its source code in the Java edit
Download Pdf Manuals
Related Search