@@ -2085,12 +2085,15 @@ let mkCilint (ik:ikind) (i:int64) : cilint =
20852085
20862086
20872087(* Construct an integer constant with possible truncation *)
2088- let kintegerCilint (k : ikind ) (i : cilint ) : exp =
2088+ let kintegerCilintString (k : ikind ) (i : cilint ) ( s :string option ) : exp =
20892089 let i', truncated = truncateCilint k i in
20902090 if truncated = BitTruncation && ! warnTruncate then
20912091 ignore (warnOpt " Truncating integer %s to %s"
20922092 (string_of_cilint i) (string_of_cilint i'));
2093- Const (CInt (i', k, None ))
2093+ Const (CInt (i', k, s))
2094+
2095+ let kintegerCilint (k : ikind ) (i : cilint ) : exp =
2096+ kintegerCilintString k i None
20942097
20952098(* Construct an integer constant with possible truncation *)
20962099let kinteger64 (k : ikind ) (i : int64 ) : exp =
@@ -2749,7 +2752,7 @@ let parseInt (str: string) : exp =
27492752 let res =
27502753 let rec loop = function
27512754 | k ::rest ->
2752- if fitsInInt k i then kintegerCilint k i
2755+ if fitsInInt k i then kintegerCilintString k i ( Some str)
27532756 else loop rest
27542757 | [] -> E. s (E. unimp " Cannot represent the integer %s\n " (string_of_cilint i))
27552758 in
@@ -6010,8 +6013,7 @@ let mkCastT ~(e: exp) ~(oldt: typ) ~(newt: typ) =
60106013 TInt (IBool, [] ), Const (CInt(i , _ , _ )) ->
60116014 let v = if compare i zero_cilint = 0 then zero_cilint else one_cilint in
60126015 Const (CInt (v, IBool , None ))
6013- | TInt (newik , [] ), Const (CInt(_ , _ , Some s )) -> kintegerCilint newik (Cilint. cilint_of_string s)
6014- | TInt (newik , [] ), Const (CInt(i , _ , None)) -> kintegerCilint newik i
6016+ | TInt (newik , [] ), Const (CInt(i , _ , _ )) -> kintegerCilint newik i
60156017 | _ -> CastE (newt,e)
60166018 end
60176019
0 commit comments