From b869c2a01e74fc5c2c1364351b5f753fb55e6a1e Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 27 Apr 2021 10:55:13 +0200
Subject: [PATCH] [cabs2cil] fix minor typo
---
src/kernel_internals/typing/cabs2cil.ml | 2 +-
tests/spec/oracle/multidecl.res.oracle | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index c3a8e705137..4282f0e9f46 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 a5fb6eeefb5..2cdd55bf416 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;
*/
--
GitLab