- now uses the right type for a boolean function

- these tests do not use anymore datacons, another error is thus triggered

- now, its a single constructor
- also adds a boolean logic constant

Also documents that the behavior of a%b depends on the behavior of a/b.

Only emits overflow alarms on [a/b] when [a] may be equal to [min_int] AND
[b] may be equal to [-1]. Also reduces the values of [a] and [b] when possible.

According to the C standard, section 6.5.5 §6:
"If the quotient a/b is representable, the expression (a/b)*b + a%b shall equal a;
otherwise, the behavior of both a/b and a%b is undefined."

Guillaume Combette authored 6 months ago and David Bühler committed 5 months ago

The performance impact is small but measurable (about 2% in run time
difference for polarssl and debie1 in open-source-case-studies). That's
the tradeoff for not having to worry about misusing Obj.

When an invalid status is emitted for the instance of a precondition at a
callsite, registers as "high priority" the instance as well as the precondition
itself.

- object_pointer end of structure
- dangling -> not object_pointer

also: add clarifying comment to the Labels module

Id_term.Map is no longer usable since Id_term no longer has a working
compare function.

At_data.Set is no longer usable because comparison is no longer defined
(see previous commit). Therefore we rely here on hash tables which do
not require comparison.

Make Pred_or_term depend on Misc.Term_id instead of Cil_datatype.Term.
This should have been the case all along, since Pred_or_term is used in
contexts where the physical identity of terms matter. They might be
typed differently depending on contexts (cast or no cast) and thus
require different translations.

Then we undefine the comparison function for both modules which depend
on Misc.Id_term, since there is no meaningful comparison for physical
equality.

The notion of equality of Id_term is physical equality. The comparison
as defined is not correct. If two terms are not physically equal but
structually equal the comparison returns 0. There is no meaningful way
to define a comparison w.r.t physical equality semantics, so we'll raise
an exception.

Not having any comparison implies that Map and Set cannot be used on
Id_term.t. Hashtbl is the only collection that still works. In the
subsequent commits the uses of Id_term.Map end Set will be changed to use
Id_term.Hashtbl instead.

Note that Datatype.undefined cannot be used here. In its current state
Datatypes.Make_with_collections requires comparison to be defined. In
the future we might tease out of Make_with_collections a functor
Make_with_hashtbl.

[kernel] functions.c:120: Failure:
  mkBinOp: unsupported operator for such operands 2L == __gen_e_acsl_at
  (type of e1: long, type of e2: __e_acsl_mpz_t)

This occurs notable for code using stdlib.h unless the flag
"-keep-unused-functions none" is given.

The reason for this is a memoisation issue. In the example there are two
occurrences of j, in two terms of the form \at(j, Old).
They are typed differently according to their context. However the
memoisation in Translate_ats does not take into account the typing.
More specifically it uses Analyses_datatype.At_data for memoising the
translations, which relies on structural equivalence of terms.