From 8221a9a1eea87234d23d65d1227acf48bab5135b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?C=C3=A9cile=20RUET-CROS?= <cecile.ruet-cros@cea.fr>
Date: Fri, 7 Feb 2025 16:17:15 +0100
Subject: [PATCH] [kernel] issue #1474: + .mli doc + runt.t: -print
---
.../plugin_entry_points/kernel.mli | 11 ++++
tests/misc/machdep.t/run.t | 63 ++++++++++++++++---
2 files changed, 67 insertions(+), 7 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 4b3f27de4f..e8bf35fe4f 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/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
diff --git a/tests/misc/machdep.t/run.t b/tests/misc/machdep.t/run.t
index ccffb228b9..2177e6c4d0 100644
--- a/tests/misc/machdep.t/run.t
+++ b/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;
+ }
--
GitLab