Splits on ACSL predicates do not try to split and reduce states in which the
predicate is already satisfied or refuted.

A split has failed if the reduced state is equal to the entry state _and_
the predicate evaluates to Unknown.
If the predicate evaluates to True/False in the entry state, then the state
cannot be reduced: the reduced state is then equal to the entry state), but
this is not a failure: the split holds.

GCC states that the 'aligned' attribute applied to typedefs can lower the
default type alignment (unlike with structs).

- Extend checking to more than just left-values.
- Add function in Cil to check only for frama_c_init_obj attribute (as formals
  should not be annotated with frama_c_mutable one).