From dd574e421e0a95b6143244287392255cb23ce82f Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 26 Sep 2019 12:04:40 +0200
Subject: [PATCH] [Override Std] Do not add "restrict" in overrides
---
src/plugins/override_std/basic_blocks.ml | 1 -
src/plugins/override_std/basic_blocks.mli | 1 -
src/plugins/override_std/memcpy.ml | 4 ++--
src/plugins/override_std/memmove.ml | 4 ++--
4 files changed, 4 insertions(+), 6 deletions(-)
diff --git a/src/plugins/override_std/basic_blocks.ml b/src/plugins/override_std/basic_blocks.ml
index 2ea6dd4db1f..2eee115c55d 100644
--- a/src/plugins/override_std/basic_blocks.ml
+++ b/src/plugins/override_std/basic_blocks.ml
@@ -27,7 +27,6 @@ open Logic_const
let ptr_of t = TPtr(t, [])
let const_of t = Cil.typeAddAttributes [Attr("const", [])] t
-let restrict_of t = Cil.typeAddAttributes [Attr("restrict", [])] t
let size_t () =
Globals.Types.find_type Logic_typing.Typedef "size_t"
diff --git a/src/plugins/override_std/basic_blocks.mli b/src/plugins/override_std/basic_blocks.mli
index f0eb5ad242c..e2b0d5d0fff 100644
--- a/src/plugins/override_std/basic_blocks.mli
+++ b/src/plugins/override_std/basic_blocks.mli
@@ -24,7 +24,6 @@ open Cil_types
val ptr_of: typ -> typ
val const_of: typ -> typ
-val restrict_of: typ -> typ
val size_t: unit -> typ
diff --git a/src/plugins/override_std/memcpy.ml b/src/plugins/override_std/memcpy.ml
index f54cb0fd0a2..b0cbffaf38c 100644
--- a/src/plugins/override_std/memcpy.ml
+++ b/src/plugins/override_std/memcpy.ml
@@ -84,8 +84,8 @@ let generate_spec vi loc =
let generate_prototype t =
let name = function_name ^ "_" ^ (string_of_typ t) in
- let dt = ptr_of (restrict_of t) in
- let st = ptr_of (restrict_of (const_of t)) in
+ let dt = ptr_of t in
+ let st = ptr_of (const_of t) in
let params = [
("dest", dt, []) ;
("src", st, []) ;
diff --git a/src/plugins/override_std/memmove.ml b/src/plugins/override_std/memmove.ml
index ea35d100a61..f0ddef2df5c 100644
--- a/src/plugins/override_std/memmove.ml
+++ b/src/plugins/override_std/memmove.ml
@@ -80,8 +80,8 @@ let generate_spec vi loc =
let generate_prototype t =
let name = function_name ^ "_" ^ (string_of_typ t) in
- let dt = ptr_of (restrict_of t) in
- let st = ptr_of (restrict_of (const_of t)) in
+ let dt = ptr_of t in
+ let st = ptr_of (const_of t) in
let params = [
("dest", dt, []) ;
("src", st, []) ;
--
GitLab