No need to reset the current location after the analysis of a function or
after calling a visitor, as the new API ensures that this is the case.

- since we rename builtin labels, let us just try to find a label that does not need renaming

Allan Blanchard authored 1 year ago and Virgile Prevosto committed 11 months ago

- guarantee that pp code has the same semantics in such a case

This has no impact as the join of origins now chooses the oldest known origin,
but it could be better if we ever change the implementation of the origin join.

Do not add a unique id into the origin datatype, as this interacts badly with
hashconsing.
Instead, binds each origin to a unique id in the global table used to record
garbled mix history.

David Bühler authored 1 year ago and Andre Maroneze committed 1 year ago

This test contained sure undefined behaviors that would lead to bottom when
reducing values on ACSL predicates valid_string and valid_read_string.

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.

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

Also, give a better localization of unfinished `/@ ... @/`
annotations in ghost code.