From 890b6e8039e3f48544ed8932dd9b0f2016f68c92 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 27 May 2015 17:58:01 +0200
Subject: [PATCH] search .h in E-ACSL memory model by default
---
src/plugins/e-acsl/doc/Changelog | 2 ++
src/plugins/e-acsl/main.ml | 7 +++++--
2 files changed, 7 insertions(+), 2 deletions(-)
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 56a3ada9386..a8ccb4ffa76 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,8 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
+- E-ACSL [2015/05/27] Search .h in the E-ACSL memory model by
+ default (easier to use declarations like __memory_size).
- E-ACSL [2015/05/27] Compatibility with new Frama-C Sodium option
-frama-c-stdlib.
-* E-ACSL [2015/04/28] Fix bug when using fopen.
diff --git a/src/plugins/e-acsl/main.ml b/src/plugins/e-acsl/main.ml
index f38b8a069da..431e16241cb 100644
--- a/src/plugins/e-acsl/main.ml
+++ b/src/plugins/e-acsl/main.ml
@@ -51,9 +51,12 @@ let extended_ast_project: extended_project ref = ref To_be_extended
let unmemoized_extend_ast () =
let extend () =
+ let share = Options.Share.dir ~error:true () in
Options.feedback ~level:3 "setting kernel options for E-ACSL.";
Kernel.CppExtraArgs.add
- (Pretty_utils.sfprintf " -DE_ACSL_MACHDEP=%s" (Kernel.Machdep.get ()));
+ (Pretty_utils.sfprintf " -DE_ACSL_MACHDEP=%s -I%s/memory_model"
+ (Kernel.Machdep.get ())
+ share);
Kernel.Keep_unused_specified_functions.off ();
let ppc, ppk = File.get_preprocessor_command () in
let register s =
@@ -61,7 +64,7 @@ let unmemoized_extend_ast () =
(File.NeedCPP
(s,
ppc
- ^ Pretty_utils.sfprintf " -I%s" (Options.Share.dir ~error:true ()),
+ ^ Pretty_utils.sfprintf " -I%s" share,
ppk))
in
List.iter register (Misc.library_files ())
--
GitLab