Ensure we are building the right machine model from a session

[adpaco]

In particular, should char be signed? What should the rounding mode be?

[adpaco]

The actual concern here is that we are hardcoding values in machine_model_from_session (in src/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs. We definitely want to get these values from the session instead of doing that.

[zhassan-aws]

Check if the target architecture agrees with the hardcoded values. If not, throw an error.