CerCo : A cost annotating compiler for the C language.