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`

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

also working oracle for AST diff test

- always remove FC's internal attribute everywhere before deciding whether
  a cast is needed.
- ACSL and C decisions to cast are similar
- only unroll type for checking equality. If a cast is needed, keep
  typedef (if any) as target

attributes that are completely internal to Frama-C and do not have any impact
on the semantics of the underlying value should not lead to a cast node.

The issue was introduced in 8fa891ec. Apparently
`Mergecil.union` has some interesting side effects even if one of the
field list is empty 🤔

original definitions took advantage of the non-compliant behavior
wrt decimal integer litteral

Logic preprocessing should not need extra args, since they were already
supplied to the preprocessor during the first pass. Passing them again might
lead to warnings about symbol redefinitions.

Note: trying to compile the initializer with gcc/CompCert likely results in
'no space left on device'. Clang 12 reports an unexpected warning
("initializer overrides prior initialization of this subobject"), and some
tests indicate it actually replaces index 72057594037927936 with 0, which would
explain why it compiles. Removing a digit from the index, for instance, results
in a similar issue as GCC/CompCert (except that Clang starts consuming all RAM
instead of simply disk space).