diff --git a/src/plugins/override_std/basic_blocks.ml b/src/plugins/override_std/basic_blocks.ml index 2ea6dd4db1f1e6099fa0bf534a95cd4bb81779fb..2eee115c55d2604611b9c8455ad2bc5bee58cadb 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 f0eb5ad242c38a761353656c47312036196f57fc..e2b0d5d0fffd7e52ec4dc36ca9509c5550f7642e 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 f54cb0fd0a222f5f9bd45c25f52dcd0f12cc224d..b0cbffaf38c74e873669859e7e499615c92e8b07 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 ea35d100a61c9dd49ffaf21058ca0f54a6168ca3..f0ddef2df5cd42469a75d2e7256b1e14096fb4ee 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, []) ;