Skip to content
Snippets Groups Projects
Commit f1219ac3 authored by Patrick Baudin's avatar Patrick Baudin
Browse files

fixes AST integrity checking

parent d660df76
No related branches found
No related tags found
No related merge requests found
...@@ -1253,6 +1253,7 @@ class check ?(is_normalized=true) what : Visitor.frama_c_visitor = ...@@ -1253,6 +1253,7 @@ class check ?(is_normalized=true) what : Visitor.frama_c_visitor =
| None -> () | None -> ()
| Some lv -> | Some lv ->
let tlv = Cil.typeOfLval lv in 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 if not (Cabs2cil.allow_return_collapse ~tlv ~tf:treturn) then
check_abort "in call %a, cannot implicitly cast from \ check_abort "in call %a, cannot implicitly cast from \
function return type %a to type of %a (%a)" function return type %a to type of %a (%a)"
......
...@@ -10,6 +10,11 @@ ...@@ -10,6 +10,11 @@
/* Generated by Frama-C */ /* Generated by Frama-C */
typedef unsigned int volatile Vunsigned; typedef unsigned int volatile Vunsigned;
typedef int const Cint; 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 g(Vunsigned *q);
unsigned int f(unsigned int volatile *q); unsigned int f(unsigned int volatile *q);
...@@ -92,5 +97,23 @@ int wr_ci400(int const volatile *p, int const v); ...@@ -92,5 +97,23 @@ int wr_ci400(int const volatile *p, int const v);
/*@ volatile ci100 writes wr_ci100; */ /*@ volatile ci100 writes wr_ci100; */
/*@ volatile ci200 writes wr_ci200; */ /*@ volatile ci200 writes wr_ci200; */
/*@ volatile ci300 writes wr_ci300; */ /*@ 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;
...@@ -59,3 +59,22 @@ int wr_ci400 (const int volatile *p, const int v) ; ...@@ -59,3 +59,22 @@ int wr_ci400 (const int volatile *p, const int v) ;
//@ volatile ci200 writes wr_ci200; //@ volatile ci200 writes wr_ci200;
//@ volatile ci300 writes wr_ci300; //@ volatile ci300 writes wr_ci300;
//@ volatile ci400 writes wr_ci400; //@ 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) ;
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment