@@ -18,19 +18,21 @@ interfaces of objects, avoiding reflection.
1818
1919### Getting started
2020
21+ - See the documentation in ` scripts ` for initial setup scripts.
2122- Install Gauge from [ here] ( https://getgauge.io/get-started.html ) .
22- - Install the required Gauge plugins :
23+ - Install the required Gauge plugin :
2324 ```
2425 gauge install java
26+ ```
27+ - To generate HTML reports locally, you might also want to run
28+ ```
2529 gauge install html-report
2630```
31+ This plugin generally works well on single spec files but is unreliable and
32+ may freeze randomly when used on the whole test suite.
2733- Navigate to the ` model ` subdirectory (` cd model ` ).
2834- Run ` mvn package ` from the ` model ` directory to build a new copy of the
2935 ` models.jar ` , which will be placed in ` model/target ` .
30- - Run ` get-original-jdk.sh ` to download a copy of the real jdk classes.
31- - Use ` add-new-file.sh ` to copy a java class from the 'real' directory to our
32- directory of models. For example, to copy the jdk implementation of
33- java.lang.Long, run ` add-new-file.sh java/lang/Long.java ` .
3436- Create a branch using the scheme ` yourname/classname ` . where ` classname ` is
3537 the class for which you're creating a model.
3638- Commit the file you just copied.
@@ -61,13 +63,34 @@ interfaces of objects, avoiding reflection.
6163 ```
6264 return CProver.nondetInt();
6365```
64- Methods that are not currently modelled should include the line
66+ To generate a non-deterministic object of type ` T ` , use
67+ ` CProver.nondetWithNull(T) ` or ` CProver.nondetWithoutNull(T) ` , providing an
68+ instance of that class. Giving a non-null argument ensures the class ` T `
69+ gets loaded.
70+ - Methods that are not currently modelled should include the line
6571 ```
6672 CProver.notModelled();
6773```
6874 in the method body. Deeptest will discard any tests that depend on any such
69- method.
70- - More information about CProver's assume functionality can be found in [ the
75+ method. If a method which is not modelled returns an object, the return
76+ statement should be:
77+ ```
78+ return CProver.nondetWithNullForNotModelled();
79+ ```
80+ or
81+ ```
82+ return CProver.nondetWithoutNullForNotModelled();
83+ ```
84+ - Methods that are mocked and return an object of a class that is not modelled
85+ should also use the return statements:
86+ ```
87+ return CProver.nondetWithNullForNotModelled();
88+ ```
89+ or
90+ ```
91+ return CProver.nondetWithoutNullForNotModelled();
92+ ```
93+ - More information about CProver's assume functionality can be found in [ the
7194 manual] ( http://www.cprover.org/cprover-manual/modeling-assertions.shtml ) .
7295- CBMC is smart about strings. Most of the ` java.lang.String ` methods are
7396 intercepted and handled natively by CBMC. Therefore, it should be fine to
@@ -138,16 +161,9 @@ non-deterministic.
138161
139162### Running Tests
140163
141- To test models with test-gen, you'll need an up-to-date copy of the
142- test-generator binary. If you're developing models-library from the test-gen
143- submodule, you can ` cd model/modelTests ` and run ` setup.sh "build" ` to symlink
144- ` test-generator ` and ` models.jar ` into the ` under_test ` directory.
145- ` setup.sh "build" ` will link ` test-generator ` from the outer test-gen repo, and
146- ` models.jar ` from the ` target ` directory, so it's important that these files
147- are in the expected locations, and have been built against the current branch
148- of the models repo. The argument to ` setup.sh ` is the directory passed to cmake
149- when building ` test-generator ` , so if you ran ` cmake -H. -B$DIR ` , you should
150- run ` setup.sh $DIR ` .
164+ Before using the Gauge TestRunner, you need to set up the
165+ ` modelTests/under_test ` folder using the ` setup-under-test-dir.sh ` script. For
166+ detailed instructions, see ` scripts/README.md ` .
151167
152168Once you've set up the tests, you can run them using Gauge through Maven. Run
153169the following command from the modelTests directory. It will get all the
@@ -219,9 +235,14 @@ verify that they pass, or throw an error.
219235
220236#### Gauge spec files
221237
222- You will probably want to supply test specifications alongside any new models.
238+ You should supply test specifications alongside any new models.
223239First, you should probably familiarise yourself with how Gauge works, using the
224240official documentation [ here] ( https://docs.getgauge.io/using.html ) .
241+
242+ Gauge specs can be automatically generated for a given set of tests using the
243+ ` generate-specs.sh ` script in ` scripts/modelling-utils ` . See the ` scripts `
244+ readme for more information.
245+
225246Generally, test specifications will look like this:
226247
227248```
@@ -366,12 +387,6 @@ The important points:
366387 - End with ` ; `
367388 - Use ` / ` instead of ` . ` to separate class paths
368389
369- ### Misc
370-
371- ` create-small-rt-jar.sh ` can be used to create a jar file which contains the
372- original jdk classes, rather than models, but does not contain any jdk clasess
373- for which models don't exist. This might be useful in A-B testing.
374-
375390#### Model Stats
376391
377392The overall progress of the library modelling effort can be tracked using
0 commit comments