Skip to content
Snippets Groups Projects
Commit ba72d64b authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

Merge branch 'bugfix/patrick/check-volatile-qualifier' into 'master'

fixes AST integrity checking

See merge request frama-c/frama-c!2092
parents d660df76 f1219ac3
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