Virgile Prevosto authored 5 years ago and David Bühler committed 5 years ago

If a defined local is referenced to in the type of a declared one (e.g. in
a `sizeof` expression as part of an array length), the `Local_init` will put
its actual definition after the declaration (which occurs at the beginning of
the block, resulting in at least pretty-printing unparsable code. We generate
undeclared temp variables of the same type to overcome the issue, like in
bb30d0e4

Virgile Prevosto authored 5 years ago and David Bühler committed 5 years ago

they can appear before their `Local_init`, e.g. in a `SizeOfE` in the
size expression of a local array. Furthermore, we weren't really checking that
declared locals weren't used before the block in which they were supposed to
appear.

Virgile Prevosto authored 5 years ago and David Bühler committed 5 years ago

from a dependency point of view, this make more sense.

[Libc] add specs for chdir/chroot

See merge request frama-c/frama-c!2275

[wp] Improves simplifiers

See merge request frama-c/frama-c!2294

[configure] show version of found libraries

See merge request frama-c/frama-c!2293

Bugfix/issue549

See merge request frama-c/frama-c!2235

Resolve "[WP/QED] Incorrect transformations with binders"

Closes #654

See merge request frama-c/frama-c!2267