The main file, relse, initializes the symbolic execution and executes instructions.
The sate of a symbolic path is defined in the module Relse_path.Path_state. This module mostly defines interfaces between other modules and symbolic state.
Symbolic states are defined in Relse_symbolic. It is a crucial part of RelSE that contains operations on the symbolic memory, the symbolic store, and the path constraint.
Relational expressions are defined in the file Rel_expr
The interface with the solver is defined in Relse_smt.Solver and translation of DBAs to Formulas is defined in Relse_smt.Translate.
Insecurity checks are handled in the module Relse_insecurity.
Finally, Relse_utils provides utility functions, Relse_options defines the input options of the RelSE, Relse_stats handles the metrics outputted by the RelSE, and Relse_stubs defines the function/instruction that are stubbed during RelSE.