[kernel] issue #1474: + .mli doc + runt.t: -print

src/kernel_services/plugin_entry_points/kernel.mli

@@ -472,8 +472,19 @@ module UnfoldingForce: Parameter_sig.Bool
     called for well preparing the AST. *)
 module Machdep: sig
   include Parameter_sig.String
+
+  (** [get_dir] returns the directory containing default machdeps.
+      @since Frama-C+dev *)
   val get_dir : unit -> LoadState.t
+
+  (** [get_default_file] return the file with the name format of machdep from
+      the default machdep directory.
+      @since Frama-C+dev *)
   val get_default_file : string -> LoadState.t
+
+  (** [is_default] decides if the parameter refers to a default machdep or a
+      user file.
+      @since Frama-C+dev *)
   val is_default : string -> bool
 end
 

tests/misc/machdep.t/run.t

@@ -22,10 +22,11 @@
     __retres = 8388607 - 1;
     return __retres;
   }
-  
-  
 
-Note: we can't use only -D below, as the __fc_machdep.h define takes precedence.With -U, our cmdline definition is used in the code
+
+
+
+Note: we can't use only -D below, as the __fc_machdep.h define takes precedence. With -U, our cmdline definition is used in the code
   $ frama-c -no-autoload-plugins -check custom_machdep.c -cpp-extra-args="-UCUSTOM_MACHDEP -DCUSTOM_MACHDEP=42" -machdep custom_machdep.yaml -print
   [kernel] Parsing custom_machdep.c (with preprocessing)
   /* Generated by Frama-C */
@@ -50,11 +51,59 @@ Note: we can't use only -D below, as the __fc_machdep.h define takes precedence.
     __retres = 8388607 - 42;
     return __retres;
   }
-  
-  
+
+
+
 
 We want to ensure that `-load` works independently of in which directory the
 corresponding `-save` was performed
-  $ frama-c -no-autoload-plugins -check -machdep custom_machdep.yaml custom_machdep.c -save custom_machdep.sav
+  $ frama-c -no-autoload-plugins -check -machdep custom_machdep.yaml custom_machdep.c -save custom_machdep.sav -print
   [kernel] Parsing custom_machdep.c (with preprocessing)
-  $ mkdir -p subdir && (cd subdir && frama-c -no-autoload-plugins -load ../custom_machdep.sav)
+  /* Generated by Frama-C */
+  #include "ctype.h"
+  #include "errno.h"
+  #include "inttypes.h"
+  #include "locale.h"
+  #include "math.h"
+  #include "signal.h"
+  #include "stdarg.h"
+  #include "stddef.h"
+  #include "stdint.h"
+  #include "stdio.h"
+  #include "stdlib.h"
+  #include "string.h"
+  #include "strings.h"
+  #include "time.h"
+  #include "wchar.h"
+  int main(void)
+  {
+    int __retres;
+    __retres = 8388607 - 1;
+    return __retres;
+  }
+
+
+
+  $ mkdir -p subdir && (cd subdir && frama-c -no-autoload-plugins -load ../custom_machdep.sav -print)
+  /* Generated by Frama-C */
+  #include "ctype.h"
+  #include "errno.h"
+  #include "inttypes.h"
+  #include "locale.h"
+  #include "math.h"
+  #include "signal.h"
+  #include "stdarg.h"
+  #include "stddef.h"
+  #include "stdint.h"
+  #include "stdio.h"
+  #include "stdlib.h"
+  #include "string.h"
+  #include "strings.h"
+  #include "time.h"
+  #include "wchar.h"
+  int main(void)
+  {
+    int __retres;
+    __retres = 8388607 - 1;
+    return __retres;
+  }