From f1219ac37e9d37a6aac502616f33c1277faf3ed4 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Fri, 30 Nov 2018 12:49:46 +0100
Subject: [PATCH] fixes AST integrity checking
---
src/kernel_services/ast_queries/filecheck.ml | 1 +
.../syntax/oracle/volatile_clause.res.oracle | 25 ++++++++++++++++++-
tests/syntax/volatile_clause.i | 19 ++++++++++++++
3 files changed, 44 insertions(+), 1 deletion(-)
diff --git a/src/kernel_services/ast_queries/filecheck.ml b/src/kernel_services/ast_queries/filecheck.ml
index c763a416001..1ff90088732 100644
--- a/src/kernel_services/ast_queries/filecheck.ml
+++ b/src/kernel_services/ast_queries/filecheck.ml
@@ -1253,6 +1253,7 @@ class check ?(is_normalized=true) what : Visitor.frama_c_visitor =
| None -> ()
| Some lv ->
let tlv = Cil.typeOfLval lv in
+ let tlv = Cil.type_remove_qualifier_attributes tlv in
if not (Cabs2cil.allow_return_collapse ~tlv ~tf:treturn) then
check_abort "in call %a, cannot implicitly cast from \
function return type %a to type of %a (%a)"
diff --git a/tests/syntax/oracle/volatile_clause.res.oracle b/tests/syntax/oracle/volatile_clause.res.oracle
index 3e1cc563b88..026eace2991 100644
--- a/tests/syntax/oracle/volatile_clause.res.oracle
+++ b/tests/syntax/oracle/volatile_clause.res.oracle
@@ -10,6 +10,11 @@
/* Generated by Frama-C */
typedef unsigned int volatile Vunsigned;
typedef int const Cint;
+enum __anonenum_Enum_1 {
+ e = -1
+};
+typedef enum __anonenum_Enum_1 Enum;
+typedef Enum const CEnum;
unsigned int g(Vunsigned *q);
unsigned int f(unsigned int volatile *q);
@@ -92,5 +97,23 @@ int wr_ci400(int const volatile *p, int const v);
/*@ volatile ci100 writes wr_ci100; */
/*@ volatile ci200 writes wr_ci200; */
/*@ volatile ci300 writes wr_ci300; */
-/*@ volatile ci400 writes wr_ci400; */
+/*@ volatile ci400 writes wr_ci400;
+*/
+Enum volatile e3;
+Enum wr_e3(Enum volatile *p, Enum const v);
+
+/*@ volatile e3 writes wr_e3;
+*/
+Enum fe(Enum a);
+
+void ge(void)
+{
+ e3 = fe(e3);
+ return;
+}
+
+CEnum volatile ce1;
+CEnum volatile ce2;
+CEnum volatile ce3;
+CEnum volatile ce4;
diff --git a/tests/syntax/volatile_clause.i b/tests/syntax/volatile_clause.i
index 7cd7df5c47f..140ca72f66f 100644
--- a/tests/syntax/volatile_clause.i
+++ b/tests/syntax/volatile_clause.i
@@ -59,3 +59,22 @@ int wr_ci400 (const int volatile *p, const int v) ;
//@ volatile ci200 writes wr_ci200;
//@ volatile ci300 writes wr_ci300;
//@ volatile ci400 writes wr_ci400;
+
+typedef enum { e=-1} Enum;
+volatile Enum e3;
+Enum wr_e3 (Enum volatile *p, const Enum v) ;
+
+//@ volatile e3 writes wr_e3;
+
+Enum fe(Enum a);
+void ge(void) {
+ e3 = fe(e3);
+}
+
+typedef const Enum CEnum ;
+volatile CEnum ce1, ce2, ce3, ce4;
+
+CEnum wr_ce1 (CEnum volatile *p, const Enum v) ;
+CEnum wr_ce2 (const Enum volatile *p, const Enum v) ;
+Enum wr_ce3 (CEnum volatile *p, const Enum v) ;
+Enum wr_ce4 (const Enum volatile *p, const Enum v) ;
--
GitLab