Updated the readme to be more friendly towards new devs and Windows users. #71
Conversation
Updated readme to be more friendly to new devs and Windows users.
There was a problem hiding this comment.
Thanks, @phillipbruce1! I had some comments; also because now we have the chance to improve the documentation even further. I made some general comments as well (not really concerning your changes), but it would be great if you can spend maybe 30min to make the README even nicer :-)
I documented my setup process for GSoC'2022 here: https://sudsy-spear-592.notion.site/Symbolic-PathFinder-Setup-47fe784d81614f98b4525f260618fa35. Maybe you find it useful to improve the README.
I think we can remove the "README" file and only keep the "README.md", what do you think?
|
|
||
| Create a new Eclipse workspace in the `spf-files` directory, then import `jpf-core` and `jpf-symbc` into the workspace as Java projects. To do this in Eclipse, go to `File > Import > General > Existing Projects into Workspace` and hit next. Select `spf-files` as the root directory, then select both projects to import and hit finish. |
There was a problem hiding this comment.
I think this is not necessary. One also can use an existing workspace afak, so maybe we can just remove that part of the sentence? Or say create new one or use an existing one...
There was a problem hiding this comment.
this comment is meant to address the first part of the line
Create a new Eclipse workspace ...
|
|
||
| Next we need to tell Eclipse where to find the Java 8 JDK. Go to `Window > Preferences > Java > Installed JREs`. If you do not already have a Java 8 compliant JDK, then you will need to download one. Once you do, go to "Add...", select "Standard VM", then select "Directory..." next to "JRE home" and browse to find the `jre` directory for the desired JDK (i.e. `/path/to/jdk/.../jre`). Once selected, hit "Finish" and "Apply and Close". | ||
|
|
||
| Lastly, we need to point Eclipse to the necessary dependencies. Go to `Run > Run Configurations...`. Under the "Java Application" dropdown, there should be several run configurations. Select `run-JPF-symbc` and go to the Environment tab along the top. There should be two variables: `LD_LIBRARY_PATH` for Mac and Linux, and `PATH` for Windows. Change each to point to `jpf-symbc/lib` (i.e. `/path/to/.../jpf-symbc/lib`). Windows users should use `\\` as described above. |
There was a problem hiding this comment.
for macOS it is "DYLD_LIBRARY_PATH"
| spf-files/ | ||
| | jpf-core/ | ||
| | jpf-symbc/ | ||
| ``` | ||
|
|
There was a problem hiding this comment.
I think it would be worthwhile to mention that the user should first attempt to build the jpf-core and jpf-symbc locally before moving on to Eclipse. This way they can already detect errors that are not due to any Eclipse configuration, e.g., the java8 setup etc. In general, it would also be good to add the expected output so that users can check and see which warnings might be expected.
|
|
||
| Then please download jpf-core from here: | ||
| https://github.com/yannicnoller/jpf-core/tree/0f2f2901cd0ae9833145c38fee57be03da90a64f | ||
| ### Configuring Eclipse |
There was a problem hiding this comment.
It would be helpful to also have some screenshots.
|
|
||
| ### Building and Running |
There was a problem hiding this comment.
It would be helpful to also show an example, and the expected output.
| and user-defined data structures. | ||
|
|
||
| SPF now has a "symcrete" mode that executes paths | ||
| SPF now has a "symcrete" mode that executes paths | ||
| triggered by concrete inputs and collects constraints along the paths | ||
|
|
||
| A paper describing Symbolic PathFinder appeared at ISSTA'08: |
There was a problem hiding this comment.
Can we change the format of this reference?
Combining Unit-level Symbolic Execution and System-level Concrete Execution for Testing NASA Software
Corina S. Pǎsǎreanu, Peter C. Mehlitz, David H. Bushnell, Karen Gundy-Burlet, Michael Lowry, Suzette Person, and Mark Pape. In Proceedings of the 2008 International Symposium on Software Testing and Analysis (ISSTA '08). https://doi.org/10.1145/1390630.1390635
@inproceedings{spf,
author = {P{\u{a}}s{\u{a}}reanu, Corina S. and Mehlitz, Peter C. and Bushnell, David H. and Gundy-Burlet, Karen and Lowry, Michael and Person, Suzette and Pape, Mark},
title = {Combining Unit-Level Symbolic Execution and System-Level Concrete Execution for Testing Nasa Software},
year = {2008},
isbn = {9781605580500},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/1390630.1390635},
doi = {10.1145/1390630.1390635},
booktitle = {Proceedings of the 2008 International Symposium on Software Testing and Analysis},
pages = {15–26},
numpages = {12},
keywords = {software model checking, symbolic execution, unit testing, system testing},
location = {Seattle, WA, USA},
series = {ISSTA '08}
}
No description provided.