Commit deb43c06 authored by Ike Mulder's avatar Ike Mulder
Browse files

Added part in on extending or changing Diaframe.

parent 3b69a4a0
Pipeline #64288 passed with stage
in 19 minutes and 25 seconds
......@@ -60,6 +60,17 @@ Use `python3 -m venv <your_environment_name>` to create a new virtual environmen
Run `pip install tabulate` to install [tabulate](, the table-generation package.
Next, run `python utils/` from the root of the project. See `python utils/ --help` for more info.
## Extending or changing Diaframe
If you wish to extend or change Diaframe, this section provides some information to get you started.
- Important definitions can be found in [solve_defs.v](./theories/solve_defs.v) and
[util_classes.v](./theories/util_classes.v). We recommend getting familiar with them before making large changes.
- The rules and corresponding tactics for running the proof automation can all be found in [theories/steps](./theories/steps). There is a file for each relevant goal shape. If you wish to add or change the applied rules, or improve the pure automation, this is the place.
- The rules and procedure for constructing hints recursively can be found in [theories/hint_search](./theories/hint_search). There are separate files for the recursive rules themselves, and the procedure using them. This is not the appropriate folder for adding new base hints!
- If you wish to add a new hint (library), this can be done in [theories/lib](./theories/lib). You can inspect the files in that folder for examples.
- If you wish to add support for a new language, or experiment with changing the support for heap_lang, look at [theories/heap_lang](./theories/heap_lang). This folder contains all files responsible for making Diaframe understand heap_lang verification goals.
- The infrastructure responsible for symbolic execution can be found in [theories/symb_exec](./theories/symb_exec). This is set up quite abstractly, and is capable of handling goals other that WP. Proper documentation of this part is still future work.
## Directory structure
All Coq files reside in (subdirectories of) the [theories](./theories) folder.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment