Store float values in the flat memory model

[sallaigy]

When using the flat memory model, float values are not stored in the memory array. Attempt to retrieve floats results in an undefined value, leading to false-positives. We should add support for storing and loading floating-point values.

LLVM IR test case:

; This test failed due to unsupported memory writes for floats in the float memory model

; RUN: %bmc -bound 1 -skip-pipeline -memory=flat "%s" | FileCheck "%s"
; CHECK: Verification SUCCESSFUL

define i32 @main() {
bb:
  %b = alloca float, align 4
  store float 0.000000e+00, float* %b, align 4
  br i1 false, label %bb2, label %bb6

bb2:                                              ; preds = %bb
  br label %bb6

bb6:                                              ; preds = %bb2, %bb
  %tmp7 = load float, float* %b, align 4
  %tmp8 = fadd float %tmp7, -4.251000e+03
  %tmp9 = fcmp une float %tmp8, 0.000000e+00
  br i1 %tmp9, label %bb10, label %error

bb10:                                             ; preds = %bb6
  ret i32 0

error:                                            ; preds = %bb6
  call void @gazer.error_code(i16 2)
  unreachable
}

declare void @gazer.error_code(i16)