From baf62e5df576b5bab5e88a01fe84bd7ad89b9d11 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 3 Oct 2023 14:26:28 +0200 Subject: [PATCH] `assert false` if we encounter a CReal without a string representation --- src/analyses/base.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index ea595ad96d..e83a352df3 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -761,7 +761,7 @@ struct (match str with Some x -> M.tracel "casto" "CInt (%s, %a, %s)\n" (Z.to_string num) d_ikind ikind x | None -> ()); Int (ID.cast_to ikind (IntDomain.of_const (num,ikind,str))) | Const (CReal (_,fkind, Some str)) when not (Cilfacade.isComplexFKind fkind) -> Float (FD.of_string fkind str) (* prefer parsing from string due to higher precision *) - | Const (CReal (num, fkind, None)) when not (Cilfacade.isComplexFKind fkind) -> Float (FD.of_const fkind num) + | Const (CReal (num, fkind, None)) when not (Cilfacade.isComplexFKind fkind) -> assert false (* Cil does nor create CReal without string representation *) (* String literals *) | Const (CStr (x,_)) -> Address (AD.of_string x) (* normal 8-bit strings, type: char* *) | Const (CWStr (xs,_) as c) -> (* wide character strings, type: wchar_t* *)