Intented to replace calls to Db.Properties.Interp.loc_to_loc*, used by
the inout and from plugins.

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.

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.

The function relied on "List.map" which is not tail-rec. With enough
plevel, it provoked a stack overflow. I've simply fixed it by performing
the mapped computation inside the fold directly.

Uses a reference to a function provided by Eva to compute the dependency
of a term.

During the Eva analysis, the Inout and From plugins uses callbacks that gives
access to the computed cvalue states, and they need to evaluate some expressions
in these states.

[as_precise_loc] converts error cases in bottom or top precise_locs accordingly.

[as_location] converts error cases in bottom or top location accordingly.
Adds the value [loc_top] to Locations.

Needed by the From plugin.

The register.ml file should be removed with Db.Value in the near future.

Exports these functions in Eva.mli.

Used by the from plugin when option -from-verify-assigns is enabled.

This file will contain all functions used by the inout and from plugins to
interpret ACSL predicates and assigns clauses.
It is now in the legacy/ directory.