diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index c3a8e705137c062ef5eecc69a34f5eb13eb21ad6..4282f0e9f46d53aee4dc7b2f52b9773606f1a9bc 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -3918,7 +3918,7 @@ let optConstFoldBinOp loc machdep bop e1 e2 t = let integral_cast ty t = raise (Failure - (Format.asprintf "term %a has type %a, but %a is expected." + (Format.asprintf "term %a has type %a, but %a is expected" Cil_printer.pp_term t Cil_printer.pp_logic_type Linteger Cil_printer.pp_typ ty)) (* Exception raised by the instance of Logic_typing local to this module. diff --git a/tests/spec/oracle/multidecl.res.oracle b/tests/spec/oracle/multidecl.res.oracle index a5fb6eeefb56207a044d13d06706e462055d1704..2cdd55bf4160aadab08344b280f454d3c185004a 100644 --- a/tests/spec/oracle/multidecl.res.oracle +++ b/tests/spec/oracle/multidecl.res.oracle @@ -1,6 +1,6 @@ [kernel] Parsing tests/spec/multidecl.c (with preprocessing) [kernel:annot-error] tests/spec/multidecl.c:9: Warning: - term x has type ℤ, but int is expected.. Ignoring global annotation + term x has type ℤ, but int is expected. Ignoring global annotation /* Generated by Frama-C */ /*@ predicate p0(ℤ x) = x ≡ 0; */