[kernel] Ast_diff: fixes the check of goto targets by function.

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

[wp] display more info in TacClear/Unfold

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

AST diff

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

When a function has no correspondance in the new AST, its local and formal
variables are not added to the Varinfo table.

In the function [gvar_correspondance].

Instead of silently ignoring them and always returning `Same_body.

Virgile Prevosto authored 3 years ago and David Bühler committed 2 years ago

same issue as with compinfo

Virgile Prevosto authored 3 years ago and David Bühler committed 2 years ago

it turns out that not all global varinfos are stored in Globals.Vars...

Virgile Prevosto authored 3 years ago and David Bühler committed 2 years ago

same reason as for locals: latter formals can refer to former ones

Virgile Prevosto authored 3 years ago and David Bühler committed 2 years ago

a local can be referenced in the type of another one, hence we can't
compare them in the same environment and update said environment
afterwards.

Virgile Prevosto authored 3 years ago and David Bühler committed 2 years ago

actually, we visit the spec of a function at its first occurrence,
so that it is possible that some global logic definitions
that are used in the constract haven't been visited yet.

Virgile Prevosto authored 3 years ago and David Bühler committed 2 years ago

Specifically if a global declaration `x` occurs between a
function declaration `f` and the definition of `f` which uses `x`