Skip to content
Snippets Groups Projects
Commit 890b6e80 authored by Julien Signoles's avatar Julien Signoles
Browse files

search .h in E-ACSL memory model by default

parent 40d1cbce
No related branches found
No related tags found
No related merge requests found
...@@ -15,6 +15,8 @@ ...@@ -15,6 +15,8 @@
# E-ACSL: the Whole E-ACSL plug-in # 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 - E-ACSL [2015/05/27] Compatibility with new Frama-C Sodium option
-frama-c-stdlib. -frama-c-stdlib.
-* E-ACSL [2015/04/28] Fix bug when using fopen. -* E-ACSL [2015/04/28] Fix bug when using fopen.
......
...@@ -51,9 +51,12 @@ let extended_ast_project: extended_project ref = ref To_be_extended ...@@ -51,9 +51,12 @@ let extended_ast_project: extended_project ref = ref To_be_extended
let unmemoized_extend_ast () = let unmemoized_extend_ast () =
let extend () = let extend () =
let share = Options.Share.dir ~error:true () in
Options.feedback ~level:3 "setting kernel options for E-ACSL."; Options.feedback ~level:3 "setting kernel options for E-ACSL.";
Kernel.CppExtraArgs.add 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 (); Kernel.Keep_unused_specified_functions.off ();
let ppc, ppk = File.get_preprocessor_command () in let ppc, ppk = File.get_preprocessor_command () in
let register s = let register s =
...@@ -61,7 +64,7 @@ let unmemoized_extend_ast () = ...@@ -61,7 +64,7 @@ let unmemoized_extend_ast () =
(File.NeedCPP (File.NeedCPP
(s, (s,
ppc ppc
^ Pretty_utils.sfprintf " -I%s" (Options.Share.dir ~error:true ()), ^ Pretty_utils.sfprintf " -I%s" share,
ppk)) ppk))
in in
List.iter register (Misc.library_files ()) List.iter register (Misc.library_files ())
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment