From 17856c7c69af9527326aa904fb32719f3fa65f86 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Mon, 26 Sep 2016 18:04:42 +0200
Subject: [PATCH] Register builtin functions
---
src/plugins/e-acsl/visit.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 135692ddfbd..5a820826ce8 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -295,7 +295,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
method !vglob_aux = function
| GVarDecl(vi, _) | GVar(vi, _, _)
| GFunDecl(_, vi, _) | GFun({ svar = vi }, _)
- when Misc.is_library_loc vi.vdecl ->
+ when Misc.is_library_loc vi.vdecl || Builtins.mem vi.vname ->
if generate then
Cil.JustCopyPost
(fun l ->
--
GitLab