update code and oracles according to Frama-C changes, in particular interpretation of \valid in presence of const