From f9eae093525ce462a615ea88df4e9f0bf1eaf3d2 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Sun, 2 Aug 2020 20:53:05 +0200
Subject: [PATCH] [CilBuilder] support more expressions - successors - whole
ranges - pointer arithmetic
---
src/kernel_services/ast_building/cil_builder.ml | 12 +++++++++++-
src/kernel_services/ast_building/cil_builder.mli | 4 ++++
2 files changed, 15 insertions(+), 1 deletion(-)
diff --git a/src/kernel_services/ast_building/cil_builder.ml b/src/kernel_services/ast_building/cil_builder.ml
index 8af8b529e61..836a84016ee 100644
--- a/src/kernel_services/ast_building/cil_builder.ml
+++ b/src/kernel_services/ast_building/cil_builder.ml
@@ -184,6 +184,8 @@ struct
let bwnot e = unop Cil_types.BNot e
let binop op e1 e2 = `exp (Binop (op, harden_exp e1, harden_exp e2))
let add e1 e2 = binop Cil_types.PlusA e1 e2
+ let succ e = add e1 one
+ let increment e i = add e1 (int i)
let sub e1 e2 = binop Cil_types.MinusA e1 e2
let mul e1 e2 = binop Cil_types.Mult e1 e2
let div e1 e2 = binop Cil_types.Div e1 e2
@@ -208,6 +210,8 @@ struct
let term t = `exp (CilTerm t)
let none = `none
let range e1 e2 = `exp (Range (harden_exp_opt e1, harden_exp_opt e2))
+ let whole = `exp (Range (None, None))
+ let whole_right = `exp (Range (Some (Const (Int 0)), None))
let init i = `init (CilInit i)
let compound t l = `init (CompoundInit (t, List.map harden_init l))
@@ -294,7 +298,13 @@ struct
| Binop (op,e1,e2) ->
let e1' = build_exp ~loc e1
and e2' = build_exp ~loc e2 in
- Cil.mkBinOp ~loc op e1' e2'
+ let op' = match op with (* Normalize operation *)
+ | PlusA when Cil.isPointerType e1' -> PlusPI
+ | MinusA when Cil.isPointerType e1' -> MinusPI
+ | PlusPI when not Cil.isPointerType e1' -> PlusA
+ | MinusPI when not Cil.isPointerType e1' -> MinusA
+ in
+ Cil.mkBinOp ~loc op' e1' e2'
let rec build_term_lval ~loc ~restyp = function
| CilLval _ -> raise CInLogic
diff --git a/src/kernel_services/ast_building/cil_builder.mli b/src/kernel_services/ast_building/cil_builder.mli
index af6de9843f9..f5c06677372 100644
--- a/src/kernel_services/ast_building/cil_builder.mli
+++ b/src/kernel_services/ast_building/cil_builder.mli
@@ -100,6 +100,8 @@ sig
val neg : [< exp] -> [> exp]
val lognot : [< exp] -> [> exp]
val bwnot : [< exp] -> [> exp]
+ val succ : [< exp] -> [> exp] (* e + 1 *)
+ val increment : [< exp] -> int -> [> exp] (* e + i *)
val binop : Cil_types.binop -> [< exp] -> [< exp] -> [> exp]
val add : [< exp] -> [< exp] -> [> exp]
val sub : [< exp] -> [< exp] -> [> exp]
@@ -126,6 +128,8 @@ sig
val term : Cil_types.term -> [> exp]
val none : [> `none]
val range : [< exp | `none] -> [< exp | `none] -> [> exp]
+ val whole : [> exp] (* Whole range, i.e. .. *)
+ val whole_right : [> exp] (* Whole range right side, i.e. 0.. *)
val init : Cil_types.init -> [> init]
val compound : Cil_types.typ -> init list -> [> init]
val values : (init,'values) typ -> 'values -> init
--
GitLab