All the previously described operations and properties have been implemented in a compiler written in C which analyzes a C code to generate the RSRSG associated with each sentence of the code. As we said, the symbolic execution of each sentence over an RSRSG is going to generate a modified RSRSG as we have presented in Fig. 2. We can see that the new is just the set resulting from the union of all compatible 's that were obtained after the abstract interpretation of the sentence over all the graphs belonging to . Remember that the division, pruning, and compress operations are instanced during the abstract interpretation of each sentence.