Improve error message about bottoms

[shaoweilin]

trafficstars

I have the following simplified code

struct UU(u32);
const z : UU = UU(0u32);
fn f(_ : UU) {}
fn g() {
  let x = z;
  f(x);
  f(x);
}

which charon translates successfully without complaining. After running aeneas on the LLBC output, I get the message

[Error] There should be no bottoms in the value

It wasn't clear to me what "bottoms" mean in this context.

It would have been useful to know, from the error message, that bottoms are "Aeneas representations of values that are not accessible anymore (e.g., moved values)." (see here). For example, my code above "does not actually compile in Rust: the first call f(x) moves the value x, which is therefore not usable anymore for the second call."

There is another issue here of charon not complaining when there is an error in the code, but the issue here is only about improving the error message for bottoms.