From c00197753e53e5b7fba61ac2964ea01ab44d7bb6 Mon Sep 17 00:00:00 2001 From: Valentin Perrelle <valentin.perrelle@cea.fr> Date: Mon, 18 Jul 2022 17:36:44 +0200 Subject: [PATCH] [Cil Builder] Add .@[] operator --- src/kernel_services/ast_building/cil_builder.ml | 1 + src/kernel_services/ast_building/cil_builder.mli | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/kernel_services/ast_building/cil_builder.ml b/src/kernel_services/ast_building/cil_builder.ml index bd68e4e9f10..9a3ee8044d0 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 30d69d5165f..c83207cd1d9 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 *) -- GitLab