Incomplete : request API must also change

# Conflicts:
#	.Makefile.lint
#	src/kernel_services/ast_printing/description.ml
#	src/kernel_services/ast_printing/logic_print.ml
#	src/kernel_services/ast_printing/printer_tag.ml
#	src/kernel_services/ast_printing/printer_tag.mli
#	src/libraries/utils/rich_text.ml
#	src/plugins/gui/design.ml
#	src/plugins/gui/history.ml
#	src/plugins/gui/pretty_source.ml
#	src/plugins/gui/pretty_source.mli
#	src/plugins/gui/property_navigator.ml
#	src/plugins/occurrence/register_gui.ml
#	src/plugins/scope/dpds_gui.ml
#	src/plugins/security_slicing/register_gui.ml
#	src/plugins/slicing/register_gui.ml
#	src/plugins/value/gui_files/register_gui.ml
#	src/plugins/wp/GuiSource.ml

[WP] use no_wp (like no_eva) to skip proofs

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

Resolve "Comportement de Cil.changeTo pour les listes d'instructions"

Closes #583

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

[typing] Keep trace of all libc includes that contribute to a var definition

Closes #614

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

Fixes issue #614

Add missing entries in the Changelog

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

[Kernel] New assertion kind: Assert or Check.

Closes #227

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

[printer] ensures labels are not put on declarations

Closes #617

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

Fixes #617

Technically, the C standard distinguishes between declarations and statements,
and only the latter may have labels attached to them. Thus, printing a label
directly over a `Local_init` will result in ill-formed C code. In order to
avoid that, we add a dummy nop (aka `;`) in-between.

A first version was done in !1518, but failed to take into account
`UnspecifiedSequence` whose first element happens to be a `Local_init` 

[Makefile] avoid copying cmx if only bytecode is available

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

Thanks to Mehdi Dogguy for pointing the issue and suggesting the patch,
applied to the Debian Frama-C package.

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

Checks must never reduce the states of the analysis, nor lead to bottom.