[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 Sep 27, 2022 and David Bühler committed Sep 30, 2022

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 Sep 15, 2021 and Patrick Baudin committed Sep 29, 2022

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.

[Install] frama-c-test.sh

Closes #1154

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

Remove functions from `Extlib`

Closes #1091

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

[e acsl] restore libc test suite

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