[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.

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

Asserts are both evaluated and used as hypotheses afterwards.
Checks are only evaluated, but are not used as hypotheses: they must not affect
the analyses.

[kernel] fix initialization of built-ins in a visitor-created project

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

[WP/TIP] Adds a splitter to tactic palette

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

[Kernel] Fix: rejects more gotos that bypass the initialization of a VLA.

Closes #499

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

[Libc] add several specs

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

[Makefile] add check for incompatible ocp-indent version

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

Makes frama-c compile with the lablgtk3 beta4 package

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

Actually `create_from_visitor` was correct, but its sibling
`init_project_from_visitor` wasn't if not called from `create_from_visitor` and
is (erroneously?) exported in `file.mli`

[WP/test] adding a test initializing multidimentianal arrays

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