diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog index 56a3ada93861cf3188b5294b9e66e15f25362459..a8ccb4ffa76dedab4fcdfb60debd80d7c79a945e 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 f38b8a069da46b1bf5ce0977b3d1e2795ebd67f4..431e16241cb011094701540041e9d7b42fee54cc 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 ())