If needed, this will be done later via machdeps and not preprocessor macros

This reverts commit 1e6f9135.

It also changes pthread_t to match the usual definition on a glibc + Linux.

Prints the number of statements at which a garbled mix from a given origin
has been read and propagated, instead of the total number of times such a
garbled mix has been read/propagated.
This is more stable and depends less on states partitioning.

On assigns clause on struct, the message could be emitted even if no garbled
mix had been created, as the offsetmap for the struct was read as one cvalue,
which could be very imprecise.
Instead, this commit iters on the offsetmap and warn for each imprecise garbled
mix in the offsetmap, if any.

These warnings are emitted when a garbled mix is written through an
assignment or an assigns clause.
This commit:
- rephrases the warnings to be clearer and less verbose.
- emits the warning only for garbled mix created at the current statement,
  according to their origin. Do not emit warnings for each propagation of
  previous garbled mixes.
- emits the warning when assigning garbled mix to the formal parameters
  of a function from the arguments of a call.

Origins no longer have a lattice structure.
A unique id is associated to each created origin. When multiple origins can
be associated to a value, we keep the oldest origin (according to their ids).

The C standard explicitly states that these functions 'convert the initial
portion of the string pointed to by nptr ...'; therefore they do expect
_strings_ (NUL-terminated) as inputs.

Thanks to Mark Dascher for the fix.

In all files, all occurrences of "[eva] done for function" have been replaced
by "[eva] Done for function".

On some loops allocating memory, the size of the allocated base can be
increased at each iteration without widening, thus preventing the convergence
of the analysis.
In lmap, when the widening has no effect, we widen the size of such allocated
bases to avoid such issues.

Virgile Prevosto authored 2 years ago and Andre Maroneze committed 1 year ago

adds a test for avr_8 and avr_16. Turns out that embedded micro-controlers
have libc that are not exactly standard compliant