Only differences comes from using float builtins in expr-to-term

[Eva] New alarms for the creation of invalid pointers

Closes #812 and #625

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

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

so that Eva won't raise an alarm on them.

Avoid warning about missing proto during typechecking.
Also changes a warning into an error, and improves the error message.

According to the kernel option -warn-invalid-pointer.

In order to avoid an undefined behavior in the C code generated for this macro
(conversion from an absolute integer to a pointer).

When -absolute-valid-range is enabled, the Null base has a Known validity,
but a pointer can always points to Null+{0}.

Complies with the kernel option -warn-invalid-pointers.

[typing] Do not inline inner block if previous statement is a code annotation applying to its whole next statement

Closes #836

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

New option for pointer downcast alarms

Closes #777

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

New smart constructor for TCastE in logic_const.

[Instantiate] Fix different failures

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