In plugins pdg, scope and slicing, directly uses the Eva API instead of this
function.

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

The only remaining mention to <Db.From> is in <eva/register.ml>.
It looks like a circular dependency, but maybe we could tackle it later.

Valentin Perrelle authored 2 years ago and David Bühler committed 2 years ago

- use cardinal for integers, thus better hints for small set
- do not try to compute range when it's desperate

has not been used since years, depends on really old software

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

- stricter conversion of tuples (checks list size)
- stricter conversion of integers (checks that there is no fractional part)
- jCatch only catches JsonErrors
- more detailed error messages to debug the server interface
- jUnion works more often
- fixed several mistyping

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.