diff --git a/README.md b/README.md index 703cd83c..746b24b1 100644 --- a/README.md +++ b/README.md @@ -6,7 +6,8 @@ SELO encodes verification conditions(VCs) in SLHV and such VC will be fed to [Z3 ## Building -SELO shares the same building method with ESBMC, one can refer to ESBMC for detailed information. +SELO shares the same building method with ESBMC, one can refer to [BUILDING](./docs/ESBMC_BUILDING.md) of ESBMC for detailed information. + For convenience, we give some scripts and commands to compile the target. ### Using script(recommended) @@ -96,7 +97,8 @@ We also provide a simple script `x.py`. We can easily to run SELO on a single fi ```sh ./x.py --run ./benchmark/tests/case_1.c ``` -Output of SELO will be stored in `./output/t.log`. More details can be found by `./x.py --help` +Output of SELO will be stored in `./output/t.log`. More details can be found by `./x.py --help`. + +## Open source and License -### TODO -Adjust the script later. \ No newline at end of file +SELO is open-source software mainly distributed under the Apache License 2.0. It is based on ESBMC. Most of codes of ESBMC is preserved. However, please take a look at the COPYING file to explain who owns what and under what terms it is distributed. The files BUILDING, CITATION, CREDITS and COPYING are preserved in `docs`. Thanks for the contributions of the authors of ESBMC. \ No newline at end of file