diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 9c8a060a59c279d2b05291ced8c53795a570594c..fb91e86165755fdfcf0c4503b84707e95f82e9ca 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -1868,6 +1868,7 @@ any_identifier:
 ;
 
 identifier_or_typename: /* allowed as C field names */
+| is_acsl_typename  { $1 }
 | TYPENAME { $1 } /* followed by the same list than 'identifier' */
 | IDENTIFIER { $1 }
 /* token list used inside ascl clauses: */
@@ -1888,6 +1889,11 @@ identifier: /* part included into 'identifier_or_typename', but duplicated to av
 
 bounded_var:
 | identifier { $1 }
+| is_acsl_typename /* Since TYPENAME cannot be accepted by lexpr rule */
+    { raise
+	(Not_well_formed(loc (),
+			 "Type names are not allowed as binding variable"))
+    }
 | TYPENAME  /* Since TYPENAME cannot be accepted by lexpr rule */
     { raise
 	(Not_well_formed(loc (),
@@ -1981,9 +1987,9 @@ is_acsl_decl_or_code_annot:
 | AXIOMATIC { "axiomatic" }
 ;
 
-is_acsl_other:
-| INTEGER  { "integer" (* token that cannot be used in C fields *) }
-| REAL     { "real" (* token that cannot be used in C fields *) }
+is_acsl_typename:
+| INTEGER  { "integer" (* token that can be used in C fields *) }
+| REAL     { "real" (* token that can be used in C fields *) }
 ;
 
 is_ext_spec:
@@ -2006,7 +2012,6 @@ non_logic_keyword:
 | is_ext_spec    { $1 }
 | is_acsl_spec   { $1 }
 | is_acsl_decl_or_code_annot { $1 }
-| is_acsl_other  { $1 }
 ;
 
 bs_keyword:
diff --git a/tests/spec/logic_type.c b/tests/spec/logic_type.c
index 008bec88b3cfccc932e2acee9028e9b07b33aa4c..5d5a1dad16dd21284e6eb38f66acfacce785969f 100644
--- a/tests/spec/logic_type.c
+++ b/tests/spec/logic_type.c
@@ -34,3 +34,16 @@ void h(void) {
 //@ logic boolean boolean_from_integer(integer b) = (boolean) b;
 //@ logic boolean boolean_from_int(int b) = (boolean) b;
 //@ logic boolean boolean_from_Bool(_Bool b) = (boolean) b;
+
+typedef struct INTEGER { int integer; } Integer ;
+/*@ axiomatic B {
+  logic integer value{L}(Integer *p) = p->integer;
+} */
+
+typedef struct COMPLEX { double real,img; } Complex ;
+/*@ axiomatic CPX {
+  type complex = Complex;
+  logic double re{L}(complex *p) = p->real;
+  logic complex with_re(complex c, double re) = { c \with .real = re };
+} */
+
diff --git a/tests/spec/oracle/logic_type.res.oracle b/tests/spec/oracle/logic_type.res.oracle
index 081eb3dee31de2d529c20f55acb1b8deb838c251..8176522d721ec98d263732fc5917152355e3fe8e 100644
--- a/tests/spec/oracle/logic_type.res.oracle
+++ b/tests/spec/oracle/logic_type.res.oracle
@@ -21,6 +21,15 @@ struct __anonstruct_Point_1 {
    int y ;
 };
 typedef struct __anonstruct_Point_1 Point;
+struct INTEGER {
+   int integer ;
+};
+typedef struct INTEGER Integer;
+struct COMPLEX {
+   double real ;
+   double img ;
+};
+typedef struct COMPLEX Complex;
 /*@ type t;
  */
 /*@ logic t create(int x) ;
@@ -60,6 +69,21 @@ void h(void)
 /*@ logic 𝔹 boolean_from_int(int b) = b ≢ 0;
  */
 /*@ logic 𝔹 boolean_from_Bool(_Bool b) = b ≢ 0;
+ */
+/*@ axiomatic B {
+      logic ℤ value{L}(Integer *p) = p->integer;
+      
+      }
+ */
+/*@
+axiomatic CPX {
+  type complex = Complex;
+  
+  logic double re{L}(Complex *p) = p->real;
+  
+  logic complex with_re(complex c, double re) = {c \with .real = re};
+  
+  }
 
 */