Propagate Float literal changes from Charon

AeneasVerif · Sep 6, 2024 · 40aa2c2 · 40aa2c2
1 parent e31b9a6
commit 40aa2c2
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
@@ -75,9 +75,9 @@ let extract_literal (span : Meta.span) (fmt : F.formatter) (is_pattern : bool)
           in
           F.pp_print_string fmt c;
           if inside then F.pp_print_string fmt ")")
-  | VStr _ | VByteStr _ ->
+  | VFloat _ | VStr _ | VByteStr _ ->
       craise __FILE__ __LINE__ span
-        "String and byte string literals are unsupported"
+        "Float, string and byte string literals are unsupported"
 
 (** Format a unary operation
 

diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
@@ -92,9 +92,9 @@ let compute_literal_type (cv : literal) : literal_type =
   | VScalar sv -> TInteger sv.int_ty
   | VBool _ -> TBool
   | VChar _ -> TChar
-  | VStr _ | VByteStr _ ->
+  | VFloat _ | VStr _ | VByteStr _ ->
       craise_opt_span __FILE__ __LINE__ None
-        "String and byte string literals are unsupported"
+        "Float, string and byte string literals are unsupported"
 
 let var_get_id (v : var) : VarId.id = v.id