Certifying Delta-Oriented Programming: User Manual

Show the options of the executable "DeltaCert":

$ DeltaCert --help

Terminal output is:

DeltaCert 0.0.1

delta-cert [COMMAND] ... [OPTIONS]
  Create and Apply Certified Delta RPMs

Common flags:
  -w --workdir=DIR      Set working project directory
  -r --resolve          Resolve Undefined (U) symbols
  -? --help             Display help message
  -V --version          Print version information
     --numeric-version  Print just the version number
  -v --verbose          Loud verbosity
  -q --quiet            Quiet verbosity

delta-cert certify [OPTIONS]
  Create a certified deltarpm from two rpms

  -o --oldrpmdir=DIR    Old Autotools project directory
  -n --newrpmdir=DIR    New Autotools project directory
  -d --deltarpm=FILE    Delta RPM file

delta-cert apply [OPTIONS]
  Reconstruct an rpm from a deltarpm (safe operation)

  -d --deltarpm=FILE  
  -i --install          Install RPM after static checking

Run the PCC Agent in "certify" mode (code producer):
```
$ DeltaCert certify -n ecall_europe_with_static-1.0 
                       -o ecall_russia_with_static-1.0 
                       -d ecall_delta-1.0-1.i686.drpm
```
Description: create a delta-RPM using the "old" RPM located in directory "ecall_russia_with_static-1.0" and the "new" RPM located in "ecall_europe_with_static-1.0". The output delta-RPM is "ecall_delta-1.0-1.i686.drpm" and is stored inside the "./data" directory.

Run the PCC Agent in "apply" mode (code receiver):
```
 $ DeltaCert apply -r -d ecall_delta-1.0-1.i686.drpm 
```
Description: reconstructs a RPM from the delta-RPM provided with the -d option. The option -r is essential to tell the PCC Agent to resolve undefined symbols. The option -i installs the reconstructed RPM in the system.

Run the "Criterion" benchmarking tool:
```
 $ Profiler 
```

Run the Z3 SMT script:

Download file https://github.com/esmifro/CertifiedDOP/tree/master/z3/z3-script.txt
```
 $ z3 z3-script.txt 
```