Valentin Perrelle authored 3 years ago and Virgile Prevosto committed 3 years ago

- The optional argument is gone, allowing much shorter usage in
  printf-like functions

Fixes a crash when the location of an \assigns clause cannot be computed.

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

We have the same behavior as in the previous GUI. We are going to
discuss about potential improvements.

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

We have a request that returns all the lvalues pointed by a pointer.

- Always fold on the location bases.
- For a given base, reduce if the number of integer offsets is smaller than
  the plevel or the ilevel.

Only the functions whose body is analyzed are counted as covered by the
analysis. The functions reached by the analysis but for which a builtin or the
specification is used are not considered analyzed anymore.

Summary: computes statistics only for analyzed function. Returns [None] for
other functions.

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

- Whole program statistics are aggregated from function by function
  statistics
- Also ordered the alarms output by count by category, except for
  the Other category

And makes these options visible.

Called from the iterator; removes [call_return_policy] from iterator.ml.
In partition.ml, renames [recombine] to [combine].

The fix is correct, but it significantly changes the behavior of the history
partitioning on some case studies.
Keep it for later, in order to fully understand the consequences.

[Datatype.Option] defines a different order than [Stdlib.Option.compare].

Type ['state partition] is a map from partition keys to states.
Such maps are converted into lists to be propagated through statements.
Changes in [Key.compare] impact the list order.
The list order impacts the heuristics used to remove redundant states before
propagating them (see Partitioning_index): redundant states may be propagated
or not depending of the list order.
This impacts the number of states propagated at some statements, and thus the
consumed slevel, and the precision of the analysis afterwards.

This commit reverts the change in the comparison of keys only to minimize
changes in the behavior of the analysis partitioning.

'Indeterminate' alarms are alarms about uninitialized memory, escaping pointers
and special floating-point values (infinite and NaN).

These alarms are emitted for functions specified by -eva-warn-copy-indeterminate
option, which is @all by default. These alarms can be disabled for some function
by -eva-warn-copy-indeterminate=-f, in which case they are also disabled for
the argument expressions of calls to [f].

However:
- the @all default value did not include functions without definition
  (for which a specification or a builtin is used).
- 'indeterminate' alarms were emitted anyway for the arguments of calls to
  functions without definition, except for builtins.
So no indeterminate alarms were emitted for the argument expressions of calls
to builtins (unless their definitions were included).

This commit fixes this behavior:
the @all default of -eva-warn-copy-indeterminate option include all functions
and special case for functions without definition or builtins are removed.

It still avoids to emit surch alarms on Eva directives such as Frama_C_show_each.