diff --git a/src/kernel_services/ast_building/cil_builder.ml b/src/kernel_services/ast_building/cil_builder.ml index bd68e4e9f103884dfda6827bc98f901cb8aa0ab7..9a3ee8044d0e720940d45d47cd079b9ab0f1c7cf 100644 --- a/src/kernel_services/ast_building/cil_builder.ml +++ b/src/kernel_services/ast_building/cil_builder.ml @@ -396,6 +396,7 @@ struct let (<<), (>>) = shiftl, shiftr let (<), (>), (<=), (>=), (==), (!=) = lt, gt, le, ge, eq, ne let (--) = range + let (.@[]) = index (* Convert *) diff --git a/src/kernel_services/ast_building/cil_builder.mli b/src/kernel_services/ast_building/cil_builder.mli index 30d69d5165fb1d372b9cff7fb8058e675ede1a20..c83207cd1d9587dfff780c343b868d1bbc2e96a9 100644 --- a/src/kernel_services/ast_building/cil_builder.mli +++ b/src/kernel_services/ast_building/cil_builder.mli @@ -177,7 +177,6 @@ sig val compound : Cil_types.typ -> init list -> [> init] val values : (init,'values) typ -> 'values -> init - (* Redefined operators *) val (+) : [< exp] -> [< exp] -> [> exp] @@ -194,6 +193,7 @@ sig val (==) : [< exp] -> [< exp] -> [> exp] val (!=) : [< exp] -> [< exp] -> [> exp] val (--) : [< exp] -> [< exp] -> [> exp] + val (.@[]) : [< lval] -> [< exp] -> [> exp] (* C index operator [] *) (* Export CIL objects from built expressions *)