- easier to instantiate
- locs can now be changed each time a block is opened (needed by Variadic)

cleanup: remove obsolete files

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

[kernel] Option -version prints a newline. Option -print-version does not.

Closes #1174 et #1176

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

[ptests] EXIT directives are also for EXEC/EXECNOW subtests

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

Fix WP terminates proof in absence of decreases

Closes #1141

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

[ivette] Removes unused script distrib.sh and generated file Makefile.distrib.

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

[Makefile] Removes some warning for non git repository

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

[Eva] Shows taint status of lvalues and expressions in the Inspector component of Ivette.

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

Distribution now use git archive (see dev/make-distrib.sh script).

Maxime Jacquemin authored 2 years ago and David Bühler committed 2 years ago

It's just code styling details.

In the taint domain:
- exports generic function [is_tainted] evaluating the taint of a memory zone
  in a given state. Removes function [is_tainted_property].
- returns Direct/Indirect/Untainted instead of Data/Control/None.

Implements [is_tainted_property] in the general request,
using [Results.is_tainted].

[descr] is used in the dropdown list of information kinds.
[title] is used as tooltip on the information.

[dev] remove local-export.sh and update scripts

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

[kernel] some fixes related to default spec

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

David Bühler authored 3 years ago and Patrick Baudin committed 2 years ago

With the automatic generation of `terminates` clauses, there is no empty
function contract. Instead, we detect function specification without any
assigns clause, which is unsound for the Eva analysis.