jrgse.github.io/Installation.html at master · yuffon/jrgse.github.io · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
<!DOCTYPE html>
<html lang="en-us">
  <head>
    <meta charset="UTF-8">
    <title></title>
    <meta name="description" content=""/>
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <meta name="theme-color" content="#157878">
    <link href='https://fonts.googleapis.com/css?family=Open+Sans:400,700' rel='stylesheet' type='text/css'>
    <link rel="stylesheet" href="/temporalTest/assets/css/style.css?v=e6385aa5d099879fe352412a0d0eca6a66f2d907">
  </head>
  <body>
    <section class="page-header">


    </section>

    <section class="main-content">
      <h1 id="manual">Manual for Installing RGSE</h1>
<p><font size="4">
RGSE can be installed as a Java project in Eclipse</font></font></p>
<hr />
<p><font size="4">To run <b>RGSE</b>, The Java IDE <b>Eclipse</b> needs to support the <b>PDE</b> (Plug-in Develop Environment).
We suppose that you have created a Java project named <b>AnalysisDriver</b></font></p>

<h2 id="Z3"><strong>(1). Install Z3 </strong></h2>

<p><font size="4">(a). If your operating system is <b>Ubuntu 12.04</b>,
you can just put <b>libz3.so</b> [<a href="https://github.com/jrgse/demo/blob/master/libz3.so" class="btn">Download Link</a>]
in the directory <b>"/usr/lib/"</b>; otherwise,
you need to install the <b>Z3</b> Theorem Prover [<a href="https://github.com/Z3Prover/z3" class="btn">Z3 Website</a>]
for your operating system. (b). Put <b>libz3java.dylib</b> [<a href="https://github.com/jrgse/demo/blob/master/libz3java.dylib" class="btn">Download Link</a>]
and <b>libz3java.so</b> [<a href="https://github.com/jrgse/demo/blob/master/libz3java.so" class="btn">Download Link</a>]
in the directory <b>"pathToAnalysisDriver/"</b>.</font></p>

<h2 id="Jar Files"><strong>(2). Import the Jar Files</strong></h2>

<p><font size="4">Create a folder named <b>lib</b> in the directory <b>"pathToAnalysisDriver/"</b>, and
put the auxiliary Jar files [<a href="https://github.com/jrgse/demo/tree/master/jar%20files" class="btn">Download Link</a>] in the <b>lib</b>.
Then, you should add all the Jar files to the <b>build path</b> of the <b>AnalysisDriver project</b>.</font></p>

<h2 id="JPF-nhandler"><strong>(3). Creat the File for JPF-nhandler</strong></h2>

<p><font size="4">Create a folder called <b>"onthefly"</b> in the directory <b>"pathToAnalysisDriver/"</b> (Note that such a folder is essential to run JPF-nhandler)</b>.</font></p>

<h2 id="WALA"><strong>(4). Import the WALA Project</strong></h2>

<p><font size="4">Download the <b>WALA</b> projects [<a href="https://github.com/jrgse/demo/tree/master/wala" class="btn">Download Link</a>],
and add it them the dependent projects of the <b>AnalysisDriver project</b>.
Note that you need to configure <b>WALA</b> according to your <b>JDK</b> installation,
i.e., change the value of <b>java_runtime_dir</b> in the file <b>com.ibm.wala.core/dat/wala.properties</b> to your own installed Java lib. </font></p>

<h2 id="Static Analysis"><strong>(5). Create the Files for Static Analysis</strong></h2>

<p><font size="4">Put the file <b>Include.txt</b> [<a href="https://github.com/jrgse/demo/blob/master/Include.txt" class="btn">Download Link</a>]
and the file <b>Exclusions.txt</b> [<a href="https://github.com/jrgse/demo/blob/master/Exclusions.txt" class="btn">Download Link</a>] in the directory <b>"pathToAnalysisDriver/src"</b>.
Note that you should change <b>"bin/moti"</b> in the file <b>Include.txt</b> to the location of your own package, e.g., <b>"bin/yourPackageName"</b>.</font></p>

<h2 id="WALA"><strong>(6). Import the Setting File of RGSE</strong></h2>

<p><font size="4">Download the configuration file of RGSE [<a href="https://github.com/jrgse/demo/blob/master/rgse.jpf" class="btn">Download Link</a>],
 and put it in the directory <b>"pathToAnalysisDriver/"</b>.</font></p>

<h2 id="WALA"><strong>(7). Write the Analysis Driver</strong></h2>
<p><font size="4">You can download the motivation example [<a href="https://github.com/jrgse/demo/blob/master/Example.java" class="btn">Download Link</a>]
and its analysis driver [<a href="https://github.com/jrgse/demo/blob/master/TestMotiExamplewithSlicing.java" class="btn">Download Link</a>] for reference.
Note that you should change the following arguments with respect to your program: <b>symMethod</b>, <b>symMethodSig</b>,
 <b>classname</b>, and <b>mainClassName</b> in the <b>main</b> function and <b>classpath</b> in the <b>createArgsMotiExample</b> function.
 In addition, the implementation of function <b>getForwardFSAAntlr</b> (FSM) and function <b>setProperty</b> (Java monitor) depends on the property to be verified.
It is worth noting that the <b>tutorials</b>
[<a href="https://jrgse.github.io/tutorial.html" class="btn">Link</a>] can also help you to write an analysis driver.</font></p>

<h2 id="WALA"><strong>(8). Run the Analysis Driver</strong></h2>

<p><font size="4">Build the <b>AnalysisDriver project</b>, and run it as a Java application.</font></p>

<hr />

<h2 id="contacts"><strong>Contacts</strong></h2>

<p> <font size="4">Please feel free to contact us if you have any problem.</font></p>

<ul>
  <li><code class="highlighter-rouge"><font color="#0000FF" size="4">hengbiaoyu@nudt.edu.cn</font></code></li>
</ul>

<ul>
  <li><code class="highlighter-rouge"><font color="#0000FF" size="4">yuffonzhang@163.com</font></code></li>
</ul>

<ul>
  <li><code class="highlighter-rouge"><font color="#0000FF" size="4">zbchen@nudt.edu.cn</font></code></li>
</ul>

  </body>
</html>