char * alphabet = "ABCDEFGHIJKLMNOPQRSTUVWXYZ";
int toUpper(char *userinput) {
for (int i=0; i < strlen(userinput); i++){
// We loose here the symbolic tracking, when using a symbolic index to access non symbolic data, alphabet
userinput[i] = alphabet[userinput[i] - 'a'];
char * userinput = malloc(10);
memcpy(userinput, "aaaaaaaaa", 10);
// Let's image aaaaaaaaa is the userinput that is symbolic
// After the execution of the function userinput is not symbolic anymore