Adopt a code slicer

**Adopt a code slicer**
Aiming to improve the code exploration and avoiding states in the program unnecessary to prove a given property, you could adopt a code slicer.

Checking out some slicers:
- Frama-C: https://github.com/Frama-C/Frama-C-snapshot
- DG: https://github.com/mchalupa/dg
- GIRI: https://github.com/liuml07/giri
