From 296532e3b606e224d43eed2990c541b2b5115727 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 2 Jun 2021 17:38:45 +0200
Subject: [PATCH] [eacsl] Count E-ACSL builtins as Frama-C builtins
This modification will notably avoid translating E-ACSL builtin
contracts.
---
src/plugins/e-acsl/src/libraries/misc.ml | 3 +++
1 file changed, 3 insertions(+)
diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index 92d0e9bfef7..95e8177eaab 100644
--- a/src/plugins/e-acsl/src/libraries/misc.ml
+++ b/src/plugins/e-acsl/src/libraries/misc.ml
@@ -34,6 +34,9 @@ let is_fc_or_compiler_builtin vi =
&&
let prefix = String.sub vi.vname 0 prefix_length in
Datatype.String.equal prefix "__builtin_")
+ ||
+ (Options.Replace_libc_functions.get ()
+ && Functions.RTL.has_rtl_replacement vi.vname)
let is_fc_stdlib_generated vi =
Cil.hasAttribute "fc_stdlib_generated" vi.vattr
--
GitLab