diff --git a/.gitattributes b/.gitattributes
index b3719b153153ef6c8df56800211e77ef275a4bd2..bd77d27bee119e87970d217945848a046d5c378b 100644
--- a/.gitattributes
+++ b/.gitattributes
@@ -393,5 +393,5 @@ README* header_spec=.ignore
/share/emacs/frama-c-*.el header_spec=CEA_LGPL
/share/_frama-c header_spec=CEA_LGPL
-/src/kernel_internals/runtime/fc_config.ml.in header_spec=CEA_LGPL
+/src/kernel_internals/runtime/system_config.ml.in header_spec=CEA_LGPL
/src/libraries/stdlib/transitioning.ml.in header_spec=CEA_LGPL
diff --git a/configurator.ml b/configurator.ml
index 5e4c11ec982fdb654024e607b565b737a77097e0..87bb3e182bb859d7587594362268c4949d44fd28 100644
--- a/configurator.ml
+++ b/configurator.ml
@@ -234,6 +234,27 @@ module Fc_version = struct
"s|@MINOR_VERSION@|%s|" version.minor
end
+module OS = struct
+ type t = Windows | MacOS | OtherUnix
+
+ let get configurator =
+ match C.ocaml_config_var_exn configurator "os_type" with
+ | "Win32" -> Windows
+ | _ ->
+ match C.ocaml_config_var_exn configurator "system" with
+ | "macosx" -> MacOS
+ | _ -> OtherUnix
+
+ let pp_sed fmt t =
+ let module_dirs = match t with
+ | Windows -> "Win_dirs"
+ | MacOS -> "Macos_dirs"
+ | OtherUnix -> "Unix_dirs"
+ in
+ Format.fprintf fmt
+ "s|@FRAMAC_TARGET_SYSTEM_CONFIG_INCLUDE@|%s|" module_dirs
+end
+
let python_available configurator =
let result = C.Process.run configurator "python3" ["--version"] in
if result.exit_code <> 0 then false
@@ -256,9 +277,11 @@ let python_available configurator =
let configure configurator =
let version = Fc_version.get configurator in
let cpp = Cpp.get configurator in
+ let os = OS.get configurator in
let config_sed = open_out "config.sed" in
let fmt = Format.formatter_of_out_channel config_sed in
- Format.fprintf fmt "%a\n%a\n" Fc_version.pp_sed version Cpp.pp_sed cpp ;
+ Format.fprintf fmt "%a\n%a\n%a\n"
+ Fc_version.pp_sed version Cpp.pp_sed cpp OS.pp_sed os ;
close_out config_sed ;
let python = open_out "python-3.7-available" in
Printf.fprintf python "%b" (python_available configurator) ;
diff --git a/doc/userman/user-changes.tex b/doc/userman/user-changes.tex
index 63070311232e05e20a6e0ff093d52a6f2ec581ea..b308690922f1154fc8a5764082fd762654768e66 100644
--- a/doc/userman/user-changes.tex
+++ b/doc/userman/user-changes.tex
@@ -5,6 +5,8 @@ release. First we list changes of the last release.
\section*{Frama-C+dev}
\begin{itemize}
+\item \textbf{Environment variables:} detail variables and options dedicated to
+ user directories.
\item \textbf{Normalizing the Source Code:} extend and replace options
\texttt{-keep-unused-specified-functions} and
\texttt{-remove-unused-specified-functions} with
diff --git a/doc/userman/user-start.tex b/doc/userman/user-start.tex
index b0dec84251182d21f6b5f1a905bc9674f7942957..1f08acf17c439ae572c61c84f2a0fbbfe3839f04 100644
--- a/doc/userman/user-start.tex
+++ b/doc/userman/user-start.tex
@@ -466,7 +466,7 @@ integer numbers:
Different environment variables may be set to customize \FramaC.
-\subsection{Variable \texttt{FRAMAC\_SESSION}}\label{sec:var-session}
+\subsection{\texttt{FRAMAC\_SESSION}}\label{sec:var-session}
\FramaC may have to generate files depending on the project under analysis
during a session in order to reuse them later in other sessions.
@@ -481,22 +481,58 @@ Each \FramaC plug-in may have its own session directory (default is
a plug-in's session directory by using the option \texttt{-<plug-in
shortname>-session}.
-\subsection{Variable \texttt{FRAMAC\_CONFIG}}\label{sec:var-config}
+\subsection{User directories}\label{sec:var-user-dirs}
-\FramaC may have to generate configuration files during a session in order to
-reuse them later in other sessions.
+\FramaC provides facilities for sharing information between sessions using
+XDG-like directories for cache, config and state data. The default location of
+these directories is system-dependent.
-By default, these files are generated or searched in a subdirectory
-\texttt{frama-c} (or \texttt{.frama-c}) of the system's default configuration
-directory ({\it e.g.}
-\texttt{\%USERPROFILE\%} on Windows or \texttt{\$HOME/.config}
-on Linux). You can also set the environment variable \textttdef{FRAMAC\_CONFIG}
-or the option \optiondef{-}{config} to change this path.
+\begin{itemize}
+ \item macOS
+ \begin{itemize}
+ \item cache: \lstinline{~/Library/Caches/frama-c}
+ \item config: \lstinline{~/Application Support/frama-c/config}
+ \item state: \lstinline{~/Application Support/frama-c/state}
+ \end{itemize}
+ \item Unix (non macOS)
+ \begin{itemize}
+ \item cache: \lstinline{~/.cache/frama-c}
+ \item config: \lstinline{~/.config/frama-c}
+ \item state: \lstinline{ ~/.local/state/frama-c}
+ \end{itemize}
+ \item Windows
+ \begin{itemize}
+ \item cache: \lstinline{%TEMP%/frama-c}
+ \item config: \lstinline{%LOCALAPPDATA%/frama-c/config}
+ \item state: \lstinline{%LOCALAPPDATA%/frama-c/state}
+ \end{itemize}
+\end{itemize}
+
+There are three ways to customize these locations for \FramaC:
+\begin{itemize}
+ \item Frama-C options: \lstinline{-cache} / \lstinline{-config} / \lstinline{-state}
+ \item Frama-C variables: \lstinline{FRAMAC_CACHE} / \lstinline{FRAMAC_CONFIG} / \lstinline{FRAMAC_STATE}
+ \item XDG variables: \lstinline{XDG_CACHE} / \lstinline{XDG_CONFIG} / \lstinline{XDG_STATE_HOME}
+ (in each case, a \lstinline{frama-c} subdirectory is created inside it)
+\end{itemize}
+
+If several are used at the same time for the same directory, the order of
+priority is: \\
+\centerline{\FramaC command-line options > \FramaC variables > XDG variables.}
+
+Each \FramaC plug-in may have its own user directories if required; they are
+put in a subdirectory \lstinline{<plug-in shortname>}. Furthermore, they may
+provide options and variables to override it (where \lstinline{<plug-in>} is
+the plug-in's shortname):
+\begin{itemize}
+\item \lstinline{-<plug-in>-cache} / \lstinline{-<plug-in>-config} /
+ \lstinline{-<plug-in>-state}
+\item \lstinline{FRAMAC_<PLUG-IN>_CACHE} / \lstinline{FRAMAC_<PLUG-IN>_CONFIG} /
+ \lstinline{FRAMAC_<PLUG-IN>_STATE}
+\end{itemize}
-Each \FramaC plug-in may have its own configuration directory if required (on
-Linux, default is \texttt{\$HOME/.config/frama-c/<plug-in shortname>}). It is
-also possible to change a plug-in's config directory by using the option
-\texttt{-<plug-in shortname>-config}.
+Again, command-line options override environment variables. Furthermore,
+plug-in-specific settings have the priority over kernel settings.
\section{Exit Status}
diff --git a/ivette/src/frama-c/kernel/api/parameters/index.ts b/ivette/src/frama-c/kernel/api/parameters/index.ts
index 2e843d1dc628d18d613fa3b7de9f9a12a50d8fcd..f42b08cf6cd7c4df096be969b4b1ff93861bacd4 100644
--- a/ivette/src/frama-c/kernel/api/parameters/index.ts
+++ b/ivette/src/frama-c/kernel/api/parameters/index.ts
@@ -38,6 +38,42 @@ import * as Server from 'frama-c/server';
import * as State from 'frama-c/states';
+/** Signal for state [`session`](#session) */
+export const signalSession: Server.Signal = {
+ name: 'kernel.parameters.signalSession',
+};
+
+const getSession_internal: Server.GetRequest<null,string> = {
+ kind: Server.RqKind.GET,
+ name: 'kernel.parameters.getSession',
+ input: Json.jNull,
+ output: Json.jString,
+ fallback: '',
+ signals: [],
+};
+/** Getter for state [`session`](#session) */
+export const getSession: Server.GetRequest<null,string>= getSession_internal;
+
+const setSession_internal: Server.SetRequest<string,null> = {
+ kind: Server.RqKind.SET,
+ name: 'kernel.parameters.setSession',
+ input: Json.jString,
+ output: Json.jNull,
+ fallback: null,
+ signals: [],
+};
+/** Setter for state [`session`](#session) */
+export const setSession: Server.SetRequest<string,null>= setSession_internal;
+
+const session_internal: State.State<string> = {
+ name: 'kernel.parameters.session',
+ signal: signalSession,
+ getter: getSession,
+ setter: setSession,
+};
+/** State of parameter -session */
+export const session: State.State<string> = session_internal;
+
/** Signal for state [`astDiff`](#astdiff) */
export const signalAstDiff: Server.Signal = {
name: 'kernel.parameters.signalAstDiff',
@@ -1046,6 +1082,114 @@ const kernelLog_internal: State.State<string> = {
/** State of parameter -kernel-log */
export const kernelLog: State.State<string> = kernelLog_internal;
+/** Signal for state [`state`](#state) */
+export const signalState: Server.Signal = {
+ name: 'kernel.parameters.signalState',
+};
+
+const getState_internal: Server.GetRequest<null,string> = {
+ kind: Server.RqKind.GET,
+ name: 'kernel.parameters.getState',
+ input: Json.jNull,
+ output: Json.jString,
+ fallback: '',
+ signals: [],
+};
+/** Getter for state [`state`](#state) */
+export const getState: Server.GetRequest<null,string>= getState_internal;
+
+const setState_internal: Server.SetRequest<string,null> = {
+ kind: Server.RqKind.SET,
+ name: 'kernel.parameters.setState',
+ input: Json.jString,
+ output: Json.jNull,
+ fallback: null,
+ signals: [],
+};
+/** Setter for state [`state`](#state) */
+export const setState: Server.SetRequest<string,null>= setState_internal;
+
+const state_internal: State.State<string> = {
+ name: 'kernel.parameters.state',
+ signal: signalState,
+ getter: getState,
+ setter: setState,
+};
+/** State of parameter -state */
+export const state: State.State<string> = state_internal;
+
+/** Signal for state [`config`](#config) */
+export const signalConfig: Server.Signal = {
+ name: 'kernel.parameters.signalConfig',
+};
+
+const getConfig_internal: Server.GetRequest<null,string> = {
+ kind: Server.RqKind.GET,
+ name: 'kernel.parameters.getConfig',
+ input: Json.jNull,
+ output: Json.jString,
+ fallback: '',
+ signals: [],
+};
+/** Getter for state [`config`](#config) */
+export const getConfig: Server.GetRequest<null,string>= getConfig_internal;
+
+const setConfig_internal: Server.SetRequest<string,null> = {
+ kind: Server.RqKind.SET,
+ name: 'kernel.parameters.setConfig',
+ input: Json.jString,
+ output: Json.jNull,
+ fallback: null,
+ signals: [],
+};
+/** Setter for state [`config`](#config) */
+export const setConfig: Server.SetRequest<string,null>= setConfig_internal;
+
+const config_internal: State.State<string> = {
+ name: 'kernel.parameters.config',
+ signal: signalConfig,
+ getter: getConfig,
+ setter: setConfig,
+};
+/** State of parameter -config */
+export const config: State.State<string> = config_internal;
+
+/** Signal for state [`cache`](#cache) */
+export const signalCache: Server.Signal = {
+ name: 'kernel.parameters.signalCache',
+};
+
+const getCache_internal: Server.GetRequest<null,string> = {
+ kind: Server.RqKind.GET,
+ name: 'kernel.parameters.getCache',
+ input: Json.jNull,
+ output: Json.jString,
+ fallback: '',
+ signals: [],
+};
+/** Getter for state [`cache`](#cache) */
+export const getCache: Server.GetRequest<null,string>= getCache_internal;
+
+const setCache_internal: Server.SetRequest<string,null> = {
+ kind: Server.RqKind.SET,
+ name: 'kernel.parameters.setCache',
+ input: Json.jString,
+ output: Json.jNull,
+ fallback: null,
+ signals: [],
+};
+/** Setter for state [`cache`](#cache) */
+export const setCache: Server.SetRequest<string,null>= setCache_internal;
+
+const cache_internal: State.State<string> = {
+ name: 'kernel.parameters.cache',
+ signal: signalCache,
+ getter: getCache,
+ setter: setCache,
+};
+/** State of parameter -cache */
+export const cache: State.State<string> = cache_internal;
+
/** Signal for state [`save`](#save) */
export const signalSave: Server.Signal = {
name: 'kernel.parameters.signalSave',
diff --git a/man/frama-c.1 b/man/frama-c.1
index fa12da7239932e0498a03fefaf777bf329ef3dce..27e9941f2597e2be1899c63954d2307bf2e10d68 100644
--- a/man/frama-c.1
+++ b/man/frama-c.1
@@ -1,14 +1,14 @@
-.\" Automatically generated by Pandoc 3.1.8
+.\" Automatically generated by Pandoc 3.2.1
.\"
-.TH "FRAMA-C" "1" "" "2024-04-24" ""
+.TH "FRAMA\-C" "1" "" "2024\-07\-23" ""
.\"------------------------------------------------------------------------
-.\"
-.\" This file is part of Frama-C documentation
-.\"
-.\" Copyright (C) 2007-2024
-.\" CEA (Commissariat à l'énergie atomique et aux énergies
-.\" alternatives)
-.\"
+.\"
+.\" This file is part of Frama-C documentation
+.\"
+.\" Copyright (C) 2007-2024
+.\" CEA (Commissariat à l'énergie atomique et aux énergies
+.\" alternatives)
+.\"
.\" you can redistribute it and/or modify it under the terms of the
.\" CC-BY-SA 4.0 license
@@ -17,178 +17,183 @@
.\" using pandoc 2.0 or newer. To modify this file, edit the Markdown file,
.\" run `dune build @check-man` and then `dune promote`.
.SH NAME
-frama-c - a static analyzer for C programs
+frama\-c \- a static analyzer for C programs
.PP
-frama-c-gui - the graphical interface of frama-c
+frama\-c\-gui \- the graphical interface of frama\-c
.SH SYNOPSIS
-\f[B]frama-c\f[R] [ \f[I]options\f[R] ] \f[I]files\f[R]
+\f[B]frama\-c\f[R] [ \f[I]options\f[R] ] \f[I]files\f[R]
.SH DESCRIPTION
-\f[B]frama-c\f[R] is a suite of tools dedicated to the analysis of
-source code written in C.
-It gathers several analysis techniques in a single collaborative
-framework.
-This framework can be extended by additional plugins placed in the
-\f[B]$FRAMAC_PLUGIN\f[R] directory.
+\f[B]frama\-c\f[R] is a suite of tools dedicated to the analysis of
+source code written in C. It gathers several analysis techniques in a
+single collaborative framework.
+This framework can be extended by additional plugins.
The command
.RS
.PP
-frama-c --plugins
+frama\-c \-\-plugins
.RE
.PP
will provide the full list of the plugins that are currently installed.
.PP
-\f[B]frama-c-gui\f[R] is the graphical user interface of
-\f[B]frama-c\f[R].
-It features the same options as the command-line version.
+\f[B]frama\-c\-gui\f[R] is the graphical user interface of
+\f[B]frama\-c\f[R].
+It features the same options as the command\-line version.
.PP
-\f[B]ivette\f[R] is a new, Electron-based graphical user interface for
-\f[B]frama-c\f[R].
-It also features the same options as the command-line version.
+\f[B]ivette\f[R] is a new, Electron\-based graphical user interface for
+\f[B]frama\-c\f[R].
+It also features the same options as the command\-line version.
.PP
-By default, Frama-C recognizes \f[I].c\f[R] files as C files needing
+By default, Frama\-C recognizes \f[I].c\f[R] files as C files needing
preprocessing and \f[I].i\f[R] files as C files having been already
preprocessed.
Some plugins may extend the list of recognized files.
-Preprocessing can be customized through the \f[B]-cpp-command\f[R] and
-\f[B]-cpp-extra-args\f[R] options.
+Preprocessing can be customized through the \f[B]\-cpp\-command\f[R] and
+\f[B]\-cpp\-extra\-args\f[R] options.
.SH OPTIONS
.SS Syntax
Options taking an additional parameter can also be written under the
form
.RS
.PP
--\f[I]option\f[R]=\f[I]param\f[R]
+\-\f[I]option\f[R]=\f[I]param\f[R]
.RE
.PP
-This form is mandatory when \f[I]param\f[R] starts with a dash (`-').
+This form is mandatory when \f[I]param\f[R] starts with a dash (`\-').
.PP
Most options that take no parameter have a corresponding
.RS
.PP
--no-\f[I]option\f[R]
+\-no\-\f[I]option\f[R]
.RE
.PP
option which has the opposite effect.
.SS Help options
.TP
--help
+\-help
gives a short usage notice.
.TP
--kernel-help
-prints the list of options recognized by Frama-C\[cq]s kernel
+\-kernel\-help
+prints the list of options recognized by Frama\-C\[cq]s kernel
.TP
--explain
+\-explain
prints a help message for each other option given on the command line
.TP
--verbose \f[I]n\f[R]
+\-verbose \f[I]n\f[R]
sets verbosity level.
Defaults to 1.
Setting it to 0 will output less progress messages.
-This level can also be set on a per-\f[I]plugin\f[R] basis, with option
--\f[I]plugin\f[R]-\f[B]verbose\f[R] \f[I]n\f[R].
+This level can also be set on a per\-\f[I]plugin\f[R] basis, with option
+\-\f[I]plugin\f[R]\-\f[B]verbose\f[R] \f[I]n\f[R].
Verbosity level of the kernel can be controlled with option
-\f[B]-kernel-verbose\f[R] \f[I]n\f[R].
+\f[B]\-kernel\-verbose\f[R] \f[I]n\f[R].
.TP
--debug \f[I]n\f[R]
+\-debug \f[I]n\f[R]
sets debugging level.
Defaults to 0, meaning no debugging messages.
-This option has the same per-plugin (and kernel) specializations as
-\f[B]-verbose\f[R].
+This option has the same per\-plugin (and kernel) specializations as
+\f[B]\-verbose\f[R].
.TP
--quiet
+\-quiet
sets verbosity and debugging level to 0.
-.SS Options controlling Frama-C\[cq]s kernel
+.SS Options controlling Frama\-C\[cq]s kernel
.TP
--absolute-valid-range \f[I]min-max\f[R]
-considers that all numerical addresses in the range \f[I]min-max\f[R]
+\-absolute\-valid\-range \f[I]min\-max\f[R]
+considers that all numerical addresses in the range \f[I]min\-max\f[R]
are valid.
Bounds are parsed as OCaml integer constants.
By default, all numerical addresses are considered invalid.
.TP
--add-symbolic-path \f[I]p1:n1[,p2:n2[\&...,pn:nn]]\f[R]
+\-add\-symbolic\-path \f[I]p1:n1[,p2:n2[\&...,pn:nn]]\f[R]
replaces each path \f[I]pi\f[R] with the name \f[I]ni\f[R] when
displaying file locations in messages.
.TP
-[-no]-aggressive-merging
+[\-no]\-aggressive\-merging
merges function definitions modulo renaming.
Defaults to no.
.TP
-[-no]-allow-duplication
+[\-no]\-allow\-duplication
allows duplication of small blocks during normalization of tests and
loops.
Otherwise, normalization uses labels and gotos.
-Bigger blocks and blocks with non-trivial control flow are never
+Bigger blocks and blocks with non\-trivial control flow are never
duplicated.
Defaults to yes.
.TP
-[-no]-annot
+[\-no]\-annot
reads ACSL annotations.
This is the default.
Annotations are preprocessed by default.
-Use -no-pp-annot if you don\[cq]t want to expand macros in annotations.
+Use \-no\-pp\-annot if you don\[cq]t want to expand macros in
+annotations.
.TP
-[-no]-ast-diff
+[\-no]\-ast\-diff
computes AST differences between a loaded session (loaded with
-\f[B]-load\f[R]) and the current sources.
-These can then be used by plug-ins supporting incremental analyses.
+\f[B]\-load\f[R]) and the current sources.
+These can then be used by plug\-ins supporting incremental analyses.
.TP
--autocomplete \f[I]p1,\&...,pn\f[R]
+\-autocomplete \f[I]p1,\&...,pn\f[R]
lists the options of plugins \f[I]p1,\&...,pn\f[R] in a format suitable
for autocompletion scripts.
.TP
--big-ints-hex \f[I]max\f[R]
+\-big\-ints\-hex \f[I]max\f[R]
integers larger than \f[I]max\f[R] are displayed in hexadecimal (by
default, all integers are displayed in decimal).
.TP
--check
+\-check
performs integrity checks on the internal AST (for developers only).
.TP
-[-no]-asm-contracts
+[\-no]\-asm\-contracts
generates contracts for assembly code written according to gcc\[cq]s
extended syntax.
Defaults to yes.
.TP
-[-no]-asm-contracts-auto-validate
+[\-no]\-asm\-contracts\-auto\-validate
automatically marks contracts generated from asm as valid.
Defaults to no.
.TP
-[-no]-collapse-call-cast
+\-cache \f[I]dir\f[R]
+overrides default Frama\-C cache directory
+.TP
+[\-no]\-collapse\-call\-cast
allows implicit cast between the value returned by a function and the
lvalue it is assigned to.
Otherwise, a temporary variable is used and the cast is made explicit.
Defaults to yes.
.TP
-[-no]-constfold
+\-config \f[I]dir\f[R]
+overrides default Frama\-C configuration directory
+.TP
+[\-no]\-constfold
folds all syntactically constant expressions in the code before
analyses.
Defaults to no.
.TP
--const-readonly
+\-const\-readonly
variables with const qualifier must be actually constant.
Defaults to yes.
-The opposite option is \f[B]-unsafe-writable\f[R].
+The opposite option is \f[B]\-unsafe\-writable\f[R].
.TP
--cpp-command \f[I]cmd\f[R]
+\-cpp\-command \f[I]cmd\f[R]
uses \f[I]cmd\f[R] as the command to preprocess C files.
Defaults to the \f[B]CPP\f[R] environment variable or to
.RS
.PP
-gcc -C -E -I.
+gcc \-C \-E \-I.
.RE
.PP
if it is not set.
If unset, the command is built as follows:
.RS
.PP
-CPP -o
+CPP \-o
.RE
.PP
\f[I]%1\f[R] and \f[I]%2\f[R] can be used into the \f[B]CPP\f[R] string
to mark the position of \f[I]\f[R] and \f[I]\f[R] respectively.
Note that this option is often better replaced by
-\f[B]-cpp-extra-args\f[R].
+\f[B]\-cpp\-extra\-args\f[R].
.TP
--cpp-extra-args \f[I]args\f[R]
+\-cpp\-extra\-args \f[I]args\f[R]
gives additional arguments to the preprocessor.
Preprocessing annotations is done in two separate preprocessing stages.
The first one is a normal pass on the C code which retains macro
@@ -197,87 +202,88 @@ These are then used in the second pass during which annotations are
preprocessed.
\f[I]args\f[R] are used only for the first pass, so that arguments that
should not be used twice (such as additional include directives or macro
-definitions) must thus go there instead of \f[B]-cpp-command\f[R].
+definitions) must thus go there instead of \f[B]\-cpp\-command\f[R].
.TP
--cpp-extra-args-per-file \f[I]file1:args1,\&...,filen:argsn\f[R]
-like \f[B]-cpp-extra-args\f[R], but the arguments only apply to the
+\-cpp\-extra\-args\-per\-file \f[I]file1:args1,\&...,filen:argsn\f[R]
+like \f[B]\-cpp\-extra\-args\f[R], but the arguments only apply to the
specified files.
.TP
-[-no]-cpp-frama-c-compliant
-indicates that the chosen preprocessor complies to some Frama-C
+[\-no]\-cpp\-frama\-c\-compliant
+indicates that the chosen preprocessor complies to some Frama\-C
requirements, such as accepting the same set of options as GNU cpp, and
-accepting architecture-specific options such as -m32/-m64.
+accepting architecture\-specific options such as \-m32/\-m64.
Default values depend on the installed preprocessor at configure time.
-See also \f[B]-pp-annot\f[R].
+See also \f[B]\-pp\-annot\f[R].
.TP
-[-no]-autoload-plugins
+[\-no]\-autoload\-plugins
when on, load all the dynamic plugins found in the search path (see
-\f[B]-print-plugin-path\f[R] for more information on the default search
-path).
-Otherwise, only plugins requested by \f[B]-load-plugin\f[R] will be
+\f[B]\-print\-plugin\-path\f[R] for more information on the default
+search path).
+Otherwise, only plugins requested by \f[B]\-load\-plugin\f[R] will be
loaded.
Defaults to on.
.TP
--enums \f[I]repr\f[R]
+\-enums \f[I]repr\f[R]
choose the way the representation of enumerated types is determined.
-\f[B]frama-c -enums help\f[R] gives the list of available options.
-Default is \f[B]gcc-enums\f[R].
+\f[B]frama\-c \-enums help\f[R] gives the list of available options.
+Default is \f[B]gcc\-enums\f[R].
.TP
--float-digits \f[I]n\f[R]
-when outputting floating-point numbers, display \f[I]n\f[R] digits.
+\-float\-digits \f[I]n\f[R]
+when outputting floating\-point numbers, display \f[I]n\f[R] digits.
Defaults to 12.
.TP
--float-flush-to-zero
+\-float\-flush\-to\-zero
floating point operations flush to zero.
.TP
--float-hex
+\-float\-hex
display floats as hexadecimal.
.TP
--float-normal
+\-float\-normal
display floats with the standard OCaml routine.
.TP
--float-relative
+\-float\-relative
display float intervals as [ \f[I]lower_bound\f[R]++\f[I]width\f[R] ].
.TP
-[-no]-frama-c-stdlib
-adds \f[B]-I$FRAMAC_SHARE/libc\f[R] to the options given to the cpp
+[\-no]\-frama\-c\-stdlib
+adds \f[B]\-I$FRAMAC_SHARE/libc\f[R] to the options given to the cpp
command.
-If \f[B]-cpp-frama-c-compliant\f[R] is not false, also adds
-\f[B]-nostdinc\f[R] to prevent an inconsistent mix of system and Frama-C
-header files.
+If \f[B]\-cpp\-frama\-c\-compliant\f[R] is not false, also adds
+\f[B]\-nostdinc\f[R] to prevent an inconsistent mix of system and
+Frama\-C header files.
Defaults to yes.
.TP
--initialized-padding-locals
+\-initialized\-padding\-locals
implicit initialization of locals sets padding bits to 0.
If false, padding bits are left uninitialized.
Defaults to yes.
.TP
--inline-calls \f[I]f1,\&...,fn\f[R]
+\-inline\-calls \f[I]f1,\&...,fn\f[R]
syntactically inlines calls to functions \f[I]f1,\&...,fn\f[R].
Use \f[B]\[at]inline\f[R] to select all functions with attribute
\f[I]inline\f[R].
Recursive functions are inlined only at the first level.
Calls via function pointers are not inlined.
.TP
--json-compilation-database \f[I]path\f[R]
-use \f[I]path\f[R] as a JSON compilation database (see
-<https://clang.llvm.org/docs/JSONCompilationDatabase.html> for more
-information): each file preprocessed by Frama-C will include
-corresponding \f[B]-I\f[R] and \f[B]-D\f[R] flags according to the
+\-json\-compilation\-database \f[I]path\f[R]
+use \f[I]path\f[R] as a JSON compilation database (see \c
+.UR https://clang.llvm.org/docs/JSONCompilationDatabase.html
+.UE \c
+\ for more information): each file preprocessed by Frama\-C will include
+corresponding \f[B]\-I\f[R] and \f[B]\-D\f[R] flags according to the
specifications in \f[I]path\f[R].
If \f[I]path\f[R] is a directory, use
\f[B]<path>/compile_commands.json\f[R].
Disabled by default.
.TP
-[-no]-keep-comments
-tries to preserve comments when pretty-printing the source code.
+[\-no]\-keep\-comments
+tries to preserve comments when pretty\-printing the source code.
Defaults to no.
.TP
-[-no]-keep-switch
-when \f[B]-simplify-cfg\f[R] is set, keeps switch statements.
+[\-no]\-keep\-switch
+when \f[B]\-simplify\-cfg\f[R] is set, keeps switch statements.
Defaults to no.
.TP
--keep-unused-functions \f[I]criterion\f[R]
+\-keep\-unused\-functions \f[I]criterion\f[R]
keeps or removes function prototypes for functions that have no body and
are not used.
\f[I]criterion\f[R] is one of: \f[B]none\f[R], \f[B]specified\f[R],
@@ -286,285 +292,288 @@ value) keeps function prototypes that have an ACSL specification.
\f[B]all\f[R] and \f[B]all_debug\f[R] are identical except for compiler
builtins, which are only included with \f[B]all_debug\f[R].
.TP
--keep-unused-types
-see \f[B]-remove-unused-types\f[R].
+\-keep\-unused\-types
+see \f[B]\-remove\-unused\-types\f[R].
.TP
--kernel-log \f[I]kind:file\f[R]
-copies log messages from the Frama-C\[cq]s kernel to file.
+\-kernel\-log \f[I]kind:file\f[R]
+copies log messages from the Frama\-C\[cq]s kernel to file.
\f[I]kind\f[R] specifies which kinds of messages to be copied
(e.g.\ \f[B]w\f[R] for warnings, \f[B]e\f[R] for errors, etc.).
-See \f[B]-kernel-help\f[R] for more details.
-Can also be set on a per-plugin basis, with option
--\f[I]<plugin>\f[R]-\f[B]log\f[R].
+See \f[B]\-kernel\-help\f[R] for more details.
+Can also be set on a per\-plugin basis, with option
+\-\f[I]<plugin>\f[R]\-\f[B]log\f[R].
.TP
--kernel-msg-key \f[I]k1,\&...,kn\f[R]
+\-kernel\-msg\-key \f[I]k1,\&...,kn\f[R]
controls the emission of messages based on categories.
-Use \f[B]-kernel-msg-key help\f[R] to get a list of available
-categories, and \f[B]-kernel-msg-key=\[lq]*\[rq]\f[R] to control all
+Use \f[B]\-kernel\-msg\-key help\f[R] to get a list of available
+categories, and \f[B]\-kernel\-msg\-key=\[lq]*\[rq]\f[R] to control all
categories.
-To disable a category, add a \f[B]-\f[R] before its name; to enable a
+To disable a category, add a \f[B]\-\f[R] before its name; to enable a
category, simply add its name, with an optional \f[B]+\f[R] before it.
-For instance, \f[B]-kernel-msg-key=-k1,k2\f[R] will disable messages
+For instance, \f[B]\-kernel\-msg\-key=\-k1,k2\f[R] will disable messages
from category \f[B]k1\f[R] and enable those from category \f[B]k2\f[R].
-Can also be set on a per-plugin basis, with option
--\f[I]<plugin>\f[R]-\f[B]msg-key\f[R].
+Can also be set on a per\-plugin basis, with option
+\-\f[I]<plugin>\f[R]\-\f[B]msg\-key\f[R].
Note that each plugin has its own set of categories.
.TP
--kernel-warn-key \f[I]k1=a1,\&...,kn=an\f[R]
+\-kernel\-warn\-key \f[I]k1=a1,\&...,kn=an\f[R]
controls the emission of warnings based on categories: for each warning
category \f[I]k\f[R], associate action \f[I]a\f[R].
-Use \f[B]-kernel-warn-key help\f[R] to get a list of available warning
-categories and their currently associated actions.
+Use \f[B]\-kernel\-warn\-key help\f[R] to get a list of available
+warning categories and their currently associated actions.
The following actions can be set per category: \f[B]active\f[R] (warn),
\f[B]feedback\f[R], \f[B]error\f[R], \f[B]abort\f[R], \f[B]once\f[R],
-\f[B]feedback-once\f[R], \f[B]err-once\f[R].
+\f[B]feedback\-once\f[R], \f[B]err\-once\f[R].
Omitting the action is equivalent to setting it to \f[B]active\f[R].
-Warning categories can also be set on a per-plugin basis, with option
--\f[I]<plugin>\f[R]\f[B]-warn-key\f[R].
+Warning categories can also be set on a per\-plugin basis, with option
+\-\f[I]<plugin>\f[R]\f[B]\-warn\-key\f[R].
.TP
-[-no]-lib-entry
+[\-no]\-lib\-entry
indicates that the entry point is called during program execution.
This implies in particular that global variables cannot be assumed to
have their initial values.
-The default is \f[B]-no-lib-entry\f[R]: the entry point is also the
+The default is \f[B]\-no\-lib\-entry\f[R]: the entry point is also the
starting point of the program and globals have their initial value.
.TP
--load \f[I]file\f[R]
+\-load \f[I]file\f[R]
loads the (previously saved) state contained in \f[I]file\f[R].
.TP
--load-library \f[I]library_1,\&...,library_n\f[R]
+\-load\-library \f[I]library_1,\&...,library_n\f[R]
dynamically load libraries.
Loading order is preserved.
Libraries are loaded between plugins and modules.
.TP
--load-module \f[I]SPEC_1,\&...,SPEC_n\f[R]
+\-load\-module \f[I]SPEC_1,\&...,SPEC_n\f[R]
dynamically load modules.
-Each can be an object file, with or without extension, or a Findlib
+Each can be an object file, with or without extension, or a Findlib
package.
Loading order is preserved, but after plugins and libraries.
.TP
--load-plugin \f[I]plugin_1,\&...,plugin_n\f[R]
+\-load\-plugin \f[I]plugin_1,\&...,plugin_n\f[R]
dynamically load plugins.
Loading order is preserved.
Plugins are loaded before libraries and modules.
.TP
--machdep \f[I]machine\f[R]
-uses \f[I]machine\f[R] as the current machine-dependent configuration
+\-machdep \f[I]machine\f[R]
+uses \f[I]machine\f[R] as the current machine\-dependent configuration
(size of the various integer types, endiandness, \&...).
The list of currently supported machines is available through option
-\f[I]-machdep help\f[R].
+\f[I]\-machdep help\f[R].
Default is \f[B]x86_64\f[R].
.TP
--main \f[I]f\f[R]
+\-main \f[I]f\f[R]
sets \f[I]f\f[R] as the entry point of the analysis.
Defaults to \f[B]main\f[R].
By default, it is considered as the starting point of the program under
analysis.
-Use \f[B]-lib-entry\f[R] if \f[I]f\f[R] is supposed to be called in the
-middle of an execution.
+Use \f[B]\-lib\-entry\f[R] if \f[I]f\f[R] is supposed to be called in
+the middle of an execution.
.TP
--obfuscate
+\-obfuscate
prints an obfuscated version of the code (where original identifiers are
replaced by meaningless ones) and exits.
The correspondence table between original and new symbols is kept at the
beginning of the result.
.TP
--ocode \f[I]file\f[R]
-redirects pretty-printed code to \f[I]file\f[R] instead of standard
+\-ocode \f[I]file\f[R]
+redirects pretty\-printed code to \f[I]file\f[R] instead of standard
output.
.TP
-[-no]-orig-name
+[\-no]\-orig\-name
During the normalization phase, some variables may get renamed when
-different variables with the same name can co-exist (e.g.\ a global
+different variables with the same name can co\-exist (e.g.\ a global
variable and a formal parameter).
When this option is on, a message is printed each time this occurs.
Defaults to no.
.TP
-[-no]-pp-annot
+[\-no]\-pp\-annot
preprocesses annotations.
This is currently only possible when using gcc (or GNU cpp)
preprocessor.
The default is to preprocess annotations when the default preprocessor
-is identified as GNU or GNU-like.
-See also \f[B]-cpp-frama-c-compliant\f[R].
+is identified as GNU or GNU\-like.
+See also \f[B]\-cpp\-frama\-c\-compliant\f[R].
.TP
-[-no]-print
-pretty-prints the source code as normalized by CIL.
+[\-no]\-print
+pretty\-prints the source code as normalized by CIL.
Defaults to no.
.TP
--print-cpp-commands
+\-print\-cpp\-commands
outputs the preprocessing commands for all input files.
.TP
--print-config-json
-outputs extensive Frama-C configuration data in JSON format.
+\-print\-config\-json
+outputs extensive Frama\-C configuration data in JSON format.
.TP
-[-no]-print-libc
-expands \f[B]#include\f[R] directives in the pretty-printed CIL code for
-files in the Frama-C standard library.
+[\-no]\-print\-libc
+expands \f[B]#include\f[R] directives in the pretty\-printed CIL code
+for files in the Frama\-C standard library.
Defaults to no.
.TP
--print-libpath
-outputs the directory where the Frama-C kernel library is installed.
+\-print\-libpath
+outputs the directory where the Frama\-C kernel library is installed.
.TP
--print-path
-alias of \f[B]-print-share-path\f[R].
+\-print\-path
+alias of \f[B]\-print\-share\-path\f[R].
.TP
--print-plugin-path
-outputs the directory where Frama-C searches its plugins.
+\-print\-plugin\-path
+outputs the directory where Frama\-C searches its plugins.
.TP
--print-share-path
-outputs the directory where Frama-C stores shareable files
+\-print\-share\-path
+outputs the directory where Frama\-C stores shareable files
(e.g.\ standard library, machdeps, shared Makefiles).
.TP
-[-no]-remove-exn
+[\-no]\-remove\-exn
transforms throw and try/catch statements into normal C functions.
Defaults to no, unless the input source language has an exception
mechanism.
.TP
--remove-inlined \f[I]f1,\&...,fn\f[R]
+\-remove\-inlined \f[I]f1,\&...,fn\f[R]
removes inlined functions \f[I]f1,\&...,fn\f[R] from the AST, which must
-have been given to \f[B]-inline-calls\f[R].
+have been given to \f[B]\-inline\-calls\f[R].
Note: this option does not check if the given functions were fully
inlined.
.TP
--remove-projects \f[I]p1,\&...,pn\f[R]
+\-remove\-projects \f[I]p1,\&...,pn\f[R]
removes the given projects \f[I]p1,\&...,pn\f[R].
\f[B]\[at]all_but_current\f[R] removes all projects but the current one.
.TP
--remove-unused-types
+\-remove\-unused\-types
remove types and struct/union/enum declarations that are not referenced
anywhere else in the code.
This is the default.
-Use \f[B]-keep-unused-types\f[R] to keep these definitions.
+Use \f[B]\-keep\-unused\-types\f[R] to keep these definitions.
.TP
--safe-arrays
+\-safe\-arrays
for multidimensional arrays or arrays that are fields inside structs,
assumes that all accesses must be in bound (set by default).
-The opposite option is \f[B]-unsafe-arrays\f[R].
+The opposite option is \f[B]\-unsafe\-arrays\f[R].
.TP
--save \f[I]file\f[R]
-saves Frama-C\[cq]s state into \f[I]file\f[R] after analyses have taken
+\-save \f[I]file\f[R]
+saves Frama\-C\[cq]s state into \f[I]file\f[R] after analyses have taken
place.
.TP
--session \f[I]s\f[R]
+\-session \f[I]s\f[R]
sets \f[I]s\f[R] as the directory in which session files are searched.
.TP
-[-no]-set-project-as-default
+[\-no]\-set\-project\-as\-default
the current project becomes the default one (and so future
-\f[B]-then\f[R] sequences are applied on it).
+\f[B]\-then\f[R] sequences are applied on it).
Defaults to no.
.TP
-[-no]-simplify-cfg
+[\-no]\-simplify\-cfg
removes \f[B]break\f[R], \f[B]continue\f[R] and \f[B]switch\f[R]
statements before analyses.
Defaults to no.
.TP
-[-no]-simplify-trivial-loops
+[\-no]\-simplify\-trivial\-loops
simplifies trivial loops such as \f[B]do \&...
while (0)\f[R] loops.
Defaults to yes.
.TP
--then
-allows one to compose analyses: a first run of Frama-C will occur with
-the options before \f[B]-then\f[R] and a second run will be done with
-the options after \f[B]-then\f[R] on the current project from the first
+\-state \f[I]dir\f[R]
+overrides default Frama\-C state directory
+.TP
+\-then
+allows one to compose analyses: a first run of Frama\-C will occur with
+the options before \f[B]\-then\f[R] and a second run will be done with
+the options after \f[B]\-then\f[R] on the current project from the first
run.
.TP
--then-last
-like \f[B]-then\f[R], but the second group of actions is executed on the
-last project created by a program transformer.
+\-then\-last
+like \f[B]\-then\f[R], but the second group of actions is executed on
+the last project created by a program transformer.
.TP
--then-on \f[I]prj\f[R]
-similar to \f[B]-then\f[R] except that the second run is performed in
+\-then\-on \f[I]prj\f[R]
+similar to \f[B]\-then\f[R] except that the second run is performed in
project \f[I]prj\f[R].
-If no such project exists, Frama-C exits with an error.
+If no such project exists, Frama\-C exits with an error.
.TP
--then-replace
-like \f[B]-then-last\f[R], but also removes the previous current
+\-then\-replace
+like \f[B]\-then\-last\f[R], but also removes the previous current
project.
.TP
--time \f[I]file\f[R]
-appends user time and date in the given file when Frama-C exits.
+\-time \f[I]file\f[R]
+appends user time and date in the given file when Frama\-C exits.
.TP
--typecheck
+\-typecheck
forces typechecking of the source files.
This option is only relevant if no further analysis is requested (as
typechecking will implicitly occur before the analysis is launched).
.TP
--ulevel \f[I]n\f[R]
+\-ulevel \f[I]n\f[R]
syntactically unroll loops \f[I]n\f[R] times before the analysis.
This can be quite costly and some plugins (e.g.\ Eva) provide more
efficient ways to perform the same thing.
See their respective manuals for more information.
-This can also be activated on a per-loop basis via the \f[B]loop unfold
+This can also be activated on a per\-loop basis via the \f[B]loop unfold
\f[R] directive.
A negative value for \f[I]n\f[R] will inhibit such pragmas.
.TP
-[-no]-ulevel-force
+[\-no]\-ulevel\-force
ignores \f[B]loop unfold \[lq]done\[rq]\f[R] disabling syntactic loop
unrolling.
.PP
-[-no]-unicode outputs ACSL formulas with UTF-8 characters.
+[\-no]\-unicode outputs ACSL formulas with UTF\-8 characters.
This is the default.
-When given the \f[B]-no-unicode\f[R] option, Frama-C will use the ASCII
-version instead.
+When given the \f[B]\-no\-unicode\f[R] option, Frama\-C will use the
+ASCII version instead.
See the ACSL manual for the correspondence.
.TP
--unsafe-arrays
-see \f[B]-safe-arrays\f[R].
+\-unsafe\-arrays
+see \f[B]\-safe\-arrays\f[R].
.TP
-[-no]-unspecified-access
+[\-no]\-unspecified\-access
checks that read/write accesses occurring in an unspecified order
(according to the C standard\[cq]s notion of sequence points) are
performed on separate locations.
-With \f[B]-no-unspecified-access\f[R], assumes that it is always the
+With \f[B]\-no\-unspecified\-access\f[R], assumes that it is always the
case (this is the default).
.TP
--version
-outputs the version string of Frama-C.
+\-version
+outputs the version string of Frama\-C.
.TP
-[-no]-warn-invalid-pointer
+[\-no]\-warn\-invalid\-pointer
generate alarms for invalid pointer arithmetic.
Defaults to no.
.TP
-[-no]-warn-left-shift-negative
+[\-no]\-warn\-left\-shift\-negative
generate alarms for signed left shifts on negative values.
Defaults to yes.
.TP
-[-no]-warn-right-shift-negative
+[\-no]\-warn\-right\-shift\-negative
generate alarms for signed right shifts on negative values.
Defaults to no.
.TP
-[-no]-warn-pointer-downcast
+[\-no]\-warn\-pointer\-downcast
generates alarms when the downcast of a pointer may exceed the
destination range.
Defaults to yes.
.TP
-[-no]-warn-signed-downcast
+[\-no]\-warn\-signed\-downcast
generates alarms when signed downcasts may exceed the destination range.
Defaults to no.
.TP
-[-no]-warn-signed-overflow
+[\-no]\-warn\-signed\-overflow
generates alarms for signed operations that overflow.
Defaults to yes.
.TP
-[-no]-warn-unsigned-downcast
+[\-no]\-warn\-unsigned\-downcast
generates alarms when unsigned downcasts may exceed the destination
range.
Defaults to no.
.TP
-[-no]-warn-unsigned-overflow
+[\-no]\-warn\-unsigned\-overflow
generates alarms for unsigned operations that overflow.
Defaults to no.
.TP
-[-no]-warn-invalid-bool
+[\-no]\-warn\-invalid\-bool
generates alarms for reads of trap representations of _Bool lvalues.
Defaults to yes.
-.SS Plugin-specific options
+.SS Plugin\-specific options
For each plugin, the command
.RS
.PP
-frama-c -plugin-help
+frama\-c \-plugin\-help
.RE
.PP
will give the list of options that are specific to the plugin.
@@ -590,21 +599,38 @@ Unknown error
.PP
Exit statuses greater than 2 can be considered as a bug (or a feature
request for the case of exit status 3) and may be reported on
-Frama-C\[cq]s BTS (see below).
+Frama\-C\[cq]s BTS (see below).
.SH ENVIRONMENT VARIABLES
-It is possible to control the places where Frama-C looks for its files
+It is possible to control the places where Frama\-C looks for files
through the following variables.
.TP
-FRAMAC_LIB
-The directory where kernel\[cq]s compiled interfaces are installed.
+FRAMAC_SESSION
+equivalent to \-session
.TP
-FRAMAC_SHARE
-The directory where Frama-C data (e.g.\ its version of the standard
-library) is installed.
+FRAMAC_CACHE
+equivalent to \-cache
+.TP
+FRAMAC_CONFIG
+equivalent to \-config
+.TP
+FRAMAC_STATE
+equivalent to \-state
+.TP
+XDG_CACHE_HOME
+equivalent to FRAMAC_CACHE, but adds a sub\-directory frama\-c
+.TP
+XDG_CONFIG_HOME
+equivalent to FRAMAC_CONFIG, but adds a sub\-directory frama\-c
+.TP
+XDG_STATE_HOME
+equivalent to FRAMAC_STATE, but adds a sub\-directory frama\-c
+.PP
+Options have the priority over variables.
+Frama\-C variables have the priority over XDG variables.
.SH SEE ALSO
-Frama-C user manual:
-https://frama-c.com/download/frama-c-user-manual.pdf
+Frama\-C user manual:
+https://frama\-c.com/download/frama\-c\-user\-manual.pdf
.PP
-Frama-C homepage: https://frama-c.com
+Frama\-C homepage: https://frama\-c.com
.PP
-Frama-C BTS: https://git.frama-c.com/pub/frama-c/issues
+Frama\-C BTS: https://git.frama\-c.com/pub/frama\-c/issues
diff --git a/man/frama-c.1.md b/man/frama-c.1.md
index 21609dfc7c82daea5b78d37f7df0f29be26ea647..dfcc64130a0a5f126644e5818c73a4dc67551348 100644
--- a/man/frama-c.1.md
+++ b/man/frama-c.1.md
@@ -1,16 +1,16 @@
---
-title: 'FRAMA-C(1) 2024-04-24'
+title: 'FRAMA-C(1) 2024-07-23'
header-includes:
- |
```{=man}
.\"------------------------------------------------------------------------
- .\"
- .\" This file is part of Frama-C documentation
- .\"
- .\" Copyright (C) 2007-2024
- .\" CEA (Commissariat à l'énergie atomique et aux énergies
- .\" alternatives)
- .\"
+ .\"
+ .\" This file is part of Frama-C documentation
+ .\"
+ .\" Copyright (C) 2007-2024
+ .\" CEA (Commissariat à l'énergie atomique et aux énergies
+ .\" alternatives)
+ .\"
.\" you can redistribute it and/or modify it under the terms of the
.\" CC-BY-SA 4.0 license
@@ -34,8 +34,7 @@ frama-c-gui - the graphical interface of frama-c
**frama-c** is a suite of tools dedicated to the analysis of source code
written in C. It gathers several analysis techniques in a single collaborative
-framework. This framework can be extended by additional plugins placed in the
-**$FRAMAC_PLUGIN** directory. The command
+framework. This framework can be extended by additional plugins. The command
> frama-c -\-plugins
@@ -142,11 +141,17 @@ syntax. Defaults to yes.
[-no]-asm-contracts-auto-validate
: automatically marks contracts generated from asm as valid. Defaults to no.
+-cache *dir*
+: overrides default Frama-C cache directory
+
[-no]-collapse-call-cast
: allows implicit cast between the value returned by a function and the lvalue
it is assigned to. Otherwise, a temporary variable is used and the cast is made
explicit. Defaults to yes.
+-config *dir*
+: overrides default Frama-C configuration directory
+
[-no]-constfold
: folds all syntactically constant expressions in the code before analyses.
Defaults to no.
@@ -403,6 +408,9 @@ Defaults to no.
[-no]-simplify-trivial-loops
: simplifies trivial loops such as **do ... while (0)** loops. Defaults to yes.
+-state *dir*
+: overrides default Frama-C state directory
+
-then
: allows one to compose analyses: a first run of Frama-C will occur with the
options before **-then** and a second run will be done with the options after
@@ -518,15 +526,32 @@ for the case of exit status 3) and may be reported on Frama-C's BTS (see below).
# ENVIRONMENT VARIABLES
-It is possible to control the places where Frama-C looks for its files through
+It is possible to control the places where Frama-C looks for files through
the following variables.
-FRAMAC_LIB
-: The directory where kernel's compiled interfaces are installed.
+FRAMAC_SESSION
+: equivalent to -session
+
+FRAMAC_CACHE
+: equivalent to -cache
+
+FRAMAC_CONFIG
+: equivalent to -config
+
+FRAMAC_STATE
+: equivalent to -state
+
+XDG_CACHE_HOME
+: equivalent to FRAMAC_CACHE, but adds a sub-directory frama-c
+
+XDG_CONFIG_HOME
+: equivalent to FRAMAC_CONFIG, but adds a sub-directory frama-c
+
+XDG_STATE_HOME
+: equivalent to FRAMAC_STATE, but adds a sub-directory frama-c
-FRAMAC_SHARE
-: The directory where Frama-C data (e.g. its version of the standard library)
-is installed.
+Options have the priority over variables. Frama-C variables have the priority
+over XDG variables.
# SEE ALSO
diff --git a/nix/frama-c.nix b/nix/frama-c.nix
index cb25fea5c8e83100d1a2b7523451ea588a81247d..0678053029619d4777379a3970390b64a9424c39 100644
--- a/nix/frama-c.nix
+++ b/nix/frama-c.nix
@@ -124,7 +124,7 @@ stdenvNoCC.mkDerivation rec {
dune_opt = if release_mode then "--release" else "" ;
buildPhase = (if cover then ''
- export DUNE_WORKSPACE="dev/dune-workspace.cover"
+ export DUNE_WORKSPACE="$(pwd)/dev/dune-workspace.cover"
'' else "") +
''
dune build -j2 --display short --error-reporting=twice $dune_opt @install
diff --git a/nix/kernel-tests.nix b/nix/kernel-tests.nix
index 91451c9310cfb8e9a187abf8c422d2f2954308e2..fcc7951889bc170676198dd17fac91bbec1fc617 100644
--- a/nix/kernel-tests.nix
+++ b/nix/kernel-tests.nix
@@ -19,6 +19,7 @@ mk_tests {
dune runtest -j1 --display short \
src/plugins/server/tests/batch \
tests/fc_script \
+ tests/misc \
tests/syntax
make -C share/machdeps check-schema
'';
diff --git a/nix/mk_tests.nix b/nix/mk_tests.nix
index ceab5c12649c87c2822ba1fc6faa433ac6658654..4a54d793df4e03181c10f31f7b7a997a7f56b727 100644
--- a/nix/mk_tests.nix
+++ b/nix/mk_tests.nix
@@ -92,7 +92,7 @@ stdenvNoCC.mkDerivation {
(if cover
then ''
mkdir -p _bisect
- export DUNE_WORKSPACE="dev/dune-workspace.cover"
+ export DUNE_WORKSPACE="$(pwd)/dev/dune-workspace.cover"
export BISECT_FILE="$(pwd)/_bisect/bisect-"
''
else "");
diff --git a/share/analysis-scripts/list_functions.ml b/share/analysis-scripts/list_functions.ml
index 38de36d9b3a15198a18f4caf26ef234c0dbde20e..b497e3d40021de949465780237455d794213b3f7 100644
--- a/share/analysis-scripts/list_functions.ml
+++ b/share/analysis-scripts/list_functions.ml
@@ -115,7 +115,7 @@ class stmt_count_visitor =
location-based approach. *)
let located_within_framac_libc loc =
let pos = fst loc in
- Filepath.is_relative ~base_name:Fc_config.framac_libc pos.Filepath.pos_path
+ Filepath.is_relative ~base_name:System_config.Share.libc pos.Filepath.pos_path
class fun_cabs_visitor print_libc = object(self)
inherit Cabsvisit.nopCabsVisitor
diff --git a/src/init/toplevel/toplevel_config.ml b/src/init/toplevel/toplevel_config.ml
index 697a2ad40cb44b1bb6e6bf28e947302895947f5a..9638c5d82a46847ff0d16802c578914dd9e7dbd2 100644
--- a/src/init/toplevel/toplevel_config.ml
+++ b/src/init/toplevel/toplevel_config.ml
@@ -20,4 +20,4 @@
(* *)
(**************************************************************************)
-let () = Topdirs.dir_directory Fc_config.libdir
+let () = Topdirs.dir_directory System_config.Lib.main
diff --git a/src/kernel_internals/runtime/dump_config.ml b/src/kernel_internals/runtime/dump_config.ml
index 4b12a03e5987469449fb1954717627d656e48578..2e5727d948e4e5f1382a5fc0b753d72fff2d7eee 100644
--- a/src/kernel_internals/runtime/dump_config.ml
+++ b/src/kernel_internals/runtime/dump_config.ml
@@ -45,31 +45,31 @@ let dump_to_json () =
let string s = `String s in
let list f l = `List (List.map f l) in
`Assoc [
- "version", `String Fc_config.version ;
- "codename", `String Fc_config.codename ;
- "version_and_codename", `String Fc_config.version_and_codename ;
- "major_version", `Int Fc_config.major_version ;
- "minor_version", `Int Fc_config.minor_version ;
- "is_gui", `Bool Fc_config.is_gui ;
- (* "lablgtk", `String Fc_config.lablgtk ;
- * "ocamlc", `String Fc_config.ocamlc ;
- * "ocamlopt", `String Fc_config.ocamlopt ;
- * "ocaml_wflags", `String Fc_config.ocaml_wflags ; *)
- "datadir", `String (Fc_config.datadir:>string) ;
+ "version", `String System_config.Version.id ;
+ "codename", `String System_config.Version.codename ;
+ "version_and_codename", `String System_config.Version.id_and_codename ;
+ "major_version", `Int System_config.Version.major ;
+ "minor_version", `Int System_config.Version.minor ;
+ "is_gui", `Bool System_config.is_gui ;
+ (* "lablgtk", `String System_config.lablgtk ;
+ * "ocamlc", `String System_config.ocamlc ;
+ * "ocamlopt", `String System_config.ocamlopt ;
+ * "ocaml_wflags", `String System_config.ocaml_wflags ; *)
+ "datadir", `String (System_config.Share.main:>string) ;
"datadirs",
- list string (Filepath.Normalized.to_string_list Fc_config.datadirs) ;
- "framac_libc", `String (Fc_config.framac_libc:>string) ;
+ list string (Filepath.Normalized.to_string_list System_config.Share.dirs) ;
+ "framac_libc", `String (System_config.Share.libc:>string) ;
"plugin_dir",
- list string (Filepath.Normalized.to_string_list Fc_config.plugin_dir) ;
- "lib_dir", `String (Fc_config.libdir:>string) ;
+ list string (Filepath.Normalized.to_string_list System_config.Plugins.dirs) ;
+ "lib_dir", `String (System_config.Lib.main:>string) ;
"lib_dirs",
- list string (Filepath.Normalized.to_string_list Fc_config.libdirs) ;
- "preprocessor", `String Fc_config.preprocessor ;
- "using_default_cpp", `Bool Fc_config.using_default_cpp ;
- "preprocessor_is_gnu_like", `Bool Fc_config.preprocessor_is_gnu_like ;
+ list string (Filepath.Normalized.to_string_list System_config.Lib.dirs) ;
+ "preprocessor", `String System_config.Preprocessor.command ;
+ "using_default_cpp", `Bool System_config.Preprocessor.is_default ;
+ "preprocessor_is_gnu_like", `Bool System_config.Preprocessor.is_gnu_like ;
"preprocessor_supported_arch_options",
- list string Fc_config.preprocessor_supported_arch_options ;
- "preprocessor_keep_comments", `Bool Fc_config.preprocessor_keep_comments ;
+ list string System_config.Preprocessor.supported_arch_options ;
+ "preprocessor_keep_comments", `Bool System_config.Preprocessor.keep_comments ;
"current_machdep", `String (Kernel.Machdep.get ()) ;
"machdeps", list string (File.list_available_machdeps ()) ;
"plugins", list string (list_plugin_names ()) ;
diff --git a/src/kernel_internals/runtime/dune b/src/kernel_internals/runtime/dune
index d960851d96cfe9b33444f9d19a3860b798a4fde1..797394691da8f02ee5b2c4aac6aaadc1cec2736c 100644
--- a/src/kernel_internals/runtime/dune
+++ b/src/kernel_internals/runtime/dune
@@ -21,7 +21,7 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(rule
- (targets fc_config.ml)
- (deps fc_config.ml.in ../../../config.sed)
- (action (with-stdout-to fc_config.ml (run sed -f ../../../config.sed fc_config.ml.in)))
+ (targets system_config.ml)
+ (deps system_config.ml.in ../../../config.sed)
+ (action (with-stdout-to system_config.ml (run sed -f ../../../config.sed system_config.ml.in)))
)
diff --git a/src/kernel_internals/runtime/fc_config.ml.in b/src/kernel_internals/runtime/fc_config.ml.in
deleted file mode 100644
index 833d802008eb533f263a9ebdcff6434ab2f2e23c..0000000000000000000000000000000000000000
--- a/src/kernel_internals/runtime/fc_config.ml.in
+++ /dev/null
@@ -1,77 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2024 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-# 24 "src/kernel_internals/runtime/fc_config.ml.in"
-
-let version = "@VERSION@"
-let codename = "@VERSION_CODENAME@"
-let version_and_codename = version ^ " (" ^ codename ^ ")"
-
-let major_version = @MAJOR_VERSION@
-
-let minor_version = @MINOR_VERSION@
-
-let is_gui = Frama_c_very_first.Gui_init.is_gui
-
-let datadirs = (List.map Filepath.Normalized.of_string Config_data.Sites.share)
-let datadir = List.hd (List.rev datadirs)
-
-let libdirs = (List.map Filepath.Normalized.of_string Config_data.Sites.lib)
-let libdir = List.hd (List.rev libdirs)
-
-let plugin_dir = List.map Filepath.Normalized.of_string Config_data.Sites.plugins
-
-let plugin_path =
- String.concat ":" (Filepath.Normalized.to_string_list plugin_dir)
-
-let framac_libc = Filepath.Normalized.concat datadir "libc"
-
-let () = Filepath.add_symbolic_dir_list "FRAMAC_SHARE" datadirs
-let () = Filepath.add_symbolic_dir_list "FRAMAC_PLUGIN" plugin_dir
-
-let default_cpp = "@FRAMAC_DEFAULT_CPP@"
-
-let default_cpp_args = " @FRAMAC_DEFAULT_CPP_ARGS@"
-
-let env_or_default f vdefault =
- try
- let env = Sys.getenv "CPP" ^ default_cpp_args in
- if env=default_cpp then vdefault else f env
- with Not_found -> vdefault
-
-let preprocessor = env_or_default (fun x -> x) default_cpp
-
-let using_default_cpp = env_or_default (fun _ -> false) true
-
-let preprocessor_is_gnu_like =
- env_or_default
- (fun _ ->
- (* be more lenient when trying to determine if the preprocessor
- is gnu-like: in Cygwin, for instance, CC is "<prefix>-gcc" but
- CPP is "<prefix>-cpp", so this extra test allows proper detection. *)
- let env = Sys.getenv "CC" ^ default_cpp_args in
- env=default_cpp) @FRAMAC_GNU_CPP@
-
-let preprocessor_supported_arch_options = [@DEFAULT_CPP_SUPPORTED_ARCH_OPTS@]
-
-let preprocessor_keep_comments =
- env_or_default (fun _ -> true) @DEFAULT_CPP_KEEP_COMMENTS@
diff --git a/src/kernel_internals/runtime/fc_config.mli b/src/kernel_internals/runtime/fc_config.mli
deleted file mode 100644
index fe303eec5779ce977d9221abc22cf5a7f18992b8..0000000000000000000000000000000000000000
--- a/src/kernel_internals/runtime/fc_config.mli
+++ /dev/null
@@ -1,118 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2024 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-(** Information about version of Frama-C.
- The body of this module is generated from Makefile. *)
-
-val version: string
-(** Frama-C Version identifier. *)
-
-val codename: string
-(** Frama-C version codename.
- @since 18.0-Argon *)
-
-val version_and_codename: string
-(** Frama-C version and codename.
- @since 18.0-Argon *)
-
-val major_version: int
-(** Frama-C major version number.
- @since 19.0-Potassium *)
-
-val minor_version: int
-(** Frama-C minor version number.
- @since 19.0-Potassium *)
-
-val is_gui: bool
-(** Is the Frama-C GUI running?
- @since Beryllium-20090601-beta1
- @since frama-c-trunk not anymore a reference
-*)
-
-val datadirs: Filepath.Normalized.t list
-(** Directories where architecture independent files are in order of
- priority.
- @since 19.0-Potassium *)
-
-val datadir: Filepath.Normalized.t
-(** Last directory of datadirs (the directory of frama-c installation)
- @since 19.0-Potassium *)
-
-val framac_libc: Filepath.Normalized.t
-(** Directory where Frama-C libc headers are.
- @since 19.0-Potassium *)
-
-val libdirs: Filepath.Normalized.t list
-(** Directories where library and executable files are, in order of
- priority.
- @since 26.0-Iron *)
-
-val libdir: Filepath.Normalized.t
-(** Last directory of libdirs (the directory of frama-c installation)
- @since 26.0-Iron *)
-
-val plugin_dir: Filepath.Normalized.t list
-(** Directory where the Frama-C dynamic plug-ins are. *)
-
-val plugin_path: string
-(** The colon-separated concatenation of [plugin_dir].
- @since Magnesium-20151001 *)
-
-val preprocessor: string
-(** Name of the default command to call the preprocessor.
- If the CPP environment variable is set, use it
- else use the built-in default from autoconf. Usually this is
- "gcc -C -E -I."
- @since Oxygen-20120901 *)
-
-val using_default_cpp: bool
-(** whether the preprocessor command is the one defined at configure time
- or the result of taking a CPP environment variable, in case it differs
- from the configure-time command.
-
- @since Phosphorus-20170501-beta1 *)
-
-val preprocessor_is_gnu_like: bool
-(** whether the default preprocessor accepts the same options as gcc
- (i.e. is either gcc or clang), when this is the case, the default
- command line for preprocessing contains more options.
- @since Sodium-20150201
-*)
-
-val preprocessor_supported_arch_options: string list
-(** architecture-related options (e.g. -m32) known to be supported by
- the default preprocessor. Used to match preprocessor commands to
- selected machdeps.
- @since Phosphorus-20170501-beta1
-*)
-
-val preprocessor_keep_comments: bool
-(** [true] if the default preprocessor selected during compilation is
- able to keep comments (hence ACSL annotations) in its output.
- @since Neon-rc3
-*)
-
-(*
- Local Variables:
- compile-command: "make -C ../../.."
- End:
-*)
diff --git a/src/kernel_internals/runtime/macos_dirs.ml b/src/kernel_internals/runtime/macos_dirs.ml
new file mode 100644
index 0000000000000000000000000000000000000000..8e401a00abf0f22903da8d805b9a7b2a07163cad
--- /dev/null
+++ b/src/kernel_internals/runtime/macos_dirs.ml
@@ -0,0 +1,39 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+let home () =
+ match Sys.getenv "HOME" with
+ | "" -> raise Not_found
+ | s -> Filepath.Normalized.of_string s
+
+let env_or_default env default =
+ let open Filepath.Normalized in
+ match Sys.getenv_opt env with
+ | Some s when s <> "" -> concat (of_string s) "frama-c"
+ | _ -> concats (home ()) default
+
+let cache () =
+ env_or_default "XDG_CACHE_HOME" [ "Library" ; "Caches" ; "frama-c"]
+let config () =
+ env_or_default "XDG_CONFIG_HOME" [ "Application Support" ; "frama-c" ; "config" ]
+let state () =
+ env_or_default "XDG_STATE_HOME" [ "Application Support" ; "frama-c" ; "state" ]
diff --git a/src/kernel_internals/runtime/special_hooks.ml b/src/kernel_internals/runtime/special_hooks.ml
index fe42c94af1e1bf2c2d4e3b78ff277771d186b2a0..d888e026716f7371c4ad6c5ec839af847ee34e26 100644
--- a/src/kernel_internals/runtime/special_hooks.ml
+++ b/src/kernel_internals/runtime/special_hooks.ml
@@ -33,14 +33,14 @@ let print_config () =
FRAMAC_SHARE = %S@\n \
FRAMAC_PLUGIN = %S@\n \
FRAMAC_LIB = %S%t@."
- Fc_config.version_and_codename
- (String.concat ":" (Filepath.Normalized.to_string_list Fc_config.datadirs))
- (String.concat ":" (Filepath.Normalized.to_string_list Fc_config.plugin_dir))
- (String.concat ":" (Filepath.Normalized.to_string_list Fc_config.libdirs))
+ System_config.Version.id_and_codename
+ (System_config.Share.path)
+ (System_config.Plugins.path)
+ (System_config.Lib.path)
(fun fmt ->
- if Fc_config.preprocessor = "" then
+ if System_config.Preprocessor.command = "" then
Format.fprintf fmt "@\nWarning: no default preprocessor"
- else if not Fc_config.preprocessor_keep_comments then
+ else if not System_config.Preprocessor.keep_comments then
Format.fprintf fmt
"@\nWarning: default preprocessor is not able to keep comments \
(hence ACSL annotations) in its output")
@@ -66,21 +66,21 @@ let print_configl get value () =
end
let print_version =
- print_config Kernel.PrintVersion.get Fc_config.version_and_codename
+ print_config Kernel.PrintVersion.get System_config.Version.id_and_codename
let () = Cmdline.run_after_early_stage print_version
let print_version_newline =
- print_config ~newline:true Kernel.Version.get Fc_config.version_and_codename
+ print_config ~newline:true Kernel.Version.get System_config.Version.id_and_codename
let () = Cmdline.run_after_early_stage print_version_newline
-let print_sharepath = print_configl Kernel.PrintShare.get Fc_config.datadirs
+let print_sharepath = print_configl Kernel.PrintShare.get System_config.Share.dirs
let () = Cmdline.run_after_early_stage print_sharepath
-let print_libpath = print_configl Kernel.PrintLib.get [Fc_config.libdir]
+let print_libpath = print_configl Kernel.PrintLib.get [System_config.Lib.main]
let () = Cmdline.run_after_early_stage print_libpath
let print_pluginpath =
- print_config Kernel.PrintPluginPath.get Fc_config.plugin_path
+ print_config Kernel.PrintPluginPath.get System_config.Plugins.path
let () = Cmdline.run_after_early_stage print_pluginpath
(**************************************************************************)
diff --git a/src/kernel_internals/runtime/system_config.ml.in b/src/kernel_internals/runtime/system_config.ml.in
new file mode 100644
index 0000000000000000000000000000000000000000..028fd90f61dc36f31d07c00a11b2203cc1f9dedb
--- /dev/null
+++ b/src/kernel_internals/runtime/system_config.ml.in
@@ -0,0 +1,97 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+# 24 "src/kernel_internals/runtime/system_config.ml.in"
+
+module Version = struct
+ let id = "@VERSION@"
+ let codename = "@VERSION_CODENAME@"
+ let id_and_codename = id ^ " (" ^ codename ^ ")"
+ let major = @MAJOR_VERSION@
+ let minor = @MINOR_VERSION@
+end
+
+let is_gui = Frama_c_very_first.Gui_init.is_gui
+
+module Share = struct
+ let dirs = List.map Filepath.Normalized.of_string Config_data.Sites.share
+ let path = String.concat ":" (Filepath.Normalized.to_string_list dirs)
+ let main = List.hd (List.rev dirs)
+ let libc = Filepath.Normalized.concat main "libc"
+
+ let () = Filepath.add_symbolic_dir_list "FRAMAC_SHARE" dirs
+end
+
+module Lib = struct
+ let dirs = List.map Filepath.Normalized.of_string Config_data.Sites.lib
+ let path = String.concat ":" (Filepath.Normalized.to_string_list dirs)
+ let main = List.hd (List.rev dirs)
+end
+
+module Plugins = struct
+ let dirs = List.map Filepath.Normalized.of_string Config_data.Sites.plugins
+ let path = String.concat ":" (Filepath.Normalized.to_string_list dirs)
+
+ let () = Filepath.add_symbolic_dir_list "FRAMAC_PLUGIN" dirs
+
+ let load name =
+ Config_data.Plugins.Plugins.load name
+
+ let load_all () =
+ if is_gui then Config_data.Plugins.Plugins_gui.load_all ();
+ Config_data.Plugins.Plugins.load_all ()
+end
+
+module Preprocessor = struct
+ let default = "@FRAMAC_DEFAULT_CPP@"
+
+ let default_args = " @FRAMAC_DEFAULT_CPP_ARGS@"
+
+ let env_or_default f vdefault =
+ try
+ let env = Sys.getenv "CPP" ^ default_args in
+ if env = default then vdefault else f env
+ with Not_found -> vdefault
+
+ let command = env_or_default (fun x -> x) default
+
+ let is_default = env_or_default (fun _ -> false) true
+
+ let is_gnu_like =
+ env_or_default
+ (fun _ ->
+ (* be more lenient when trying to determine if the preprocessor
+ is gnu-like: in Cygwin, for instance, CC is "<prefix>-gcc" but
+ CPP is "<prefix>-cpp", so this extra test allows proper detection.
+ *)
+ let env = Sys.getenv "CC" ^ default_args in
+ env=default) @FRAMAC_GNU_CPP@
+
+ let keep_comments =
+ env_or_default (fun _ -> true) @DEFAULT_CPP_KEEP_COMMENTS@
+
+ let supported_arch_options = [@DEFAULT_CPP_SUPPORTED_ARCH_OPTS@]
+end
+
+module User_dirs = struct
+ include @FRAMAC_TARGET_SYSTEM_CONFIG_INCLUDE@
+end
diff --git a/src/kernel_internals/runtime/system_config.mli b/src/kernel_internals/runtime/system_config.mli
new file mode 100644
index 0000000000000000000000000000000000000000..ebe5478d892cc254e449ba61094510f007b841d4
--- /dev/null
+++ b/src/kernel_internals/runtime/system_config.mli
@@ -0,0 +1,140 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** Information about the environment *)
+
+module Version : sig
+ val id: string
+ (** Frama-C version identifier. *)
+
+ val codename: string
+ (** Frama-C version codename. *)
+
+ val id_and_codename: string
+ (** Frama-C version and codename. *)
+
+ val major: int
+ (** Frama-C major version number. *)
+
+ val minor: int
+ (** Frama-C minor version number. *)
+end
+
+(** Unless you are working in the kernel of Frama-C, you should not use this. *)
+module Share : sig
+ val dirs: Filepath.Normalized.t list
+ (** Directories where architecture-independent files are located, in order of
+ priority.
+ *)
+
+ val main: Filepath.Normalized.t
+ (** Last directory of {!dirs} (the directory of frama-c installation) *)
+
+ val path: string
+ (** The colon-separated concatenation of {!dirs}. *)
+
+ val libc: Filepath.Normalized.t
+ (** Directory where Frama-C libc headers are. *)
+end
+
+(** Unless you are working in the kernel of Frama-C, you should not use this. *)
+module Lib : sig
+ val dirs: Filepath.Normalized.t list
+ (** Directories where library and executable files are located, in order of
+ priority. *)
+
+ val path: string
+ (** The colon-separated concatenation of {!dirs}. *)
+
+ val main: Filepath.Normalized.t
+ (** Last directory of libdirs (the directory of frama-c installation) *)
+end
+
+(** Unless you are working in the kernel of Frama-C, you should not use this. *)
+module Plugins : sig
+ val dirs: Filepath.Normalized.t list
+ (** Directories where the Frama-C dynamic plug-ins are located. *)
+
+ val path: string
+ (** The colon-separated concatenation of {!dirs}. *)
+
+ val load: string -> unit
+ (** Load given plug-in name *)
+
+ val load_all: unit -> unit
+ (** Load all plug-ins, do not load GUI plug-in when not in GTK GUI mode *)
+end
+
+(** Unless you are working in the kernel of Frama-C, you should not use this. *)
+module Preprocessor : sig
+ val command: string
+ (** Name of the default command to call the preprocessor.
+ If the CPP environment variable is set, use it;
+ else use the built-in default from autoconf. Usually this is
+ "gcc -C -E -I."
+ *)
+
+ val is_default: bool
+ (** whether the preprocessor command is the one defined at configure time
+ or the result of taking a CPP environment variable, in case it differs
+ *)
+
+ val is_gnu_like: bool
+ (** whether the default preprocessor accepts the same options as gcc
+ (i.e. is either gcc or clang). When this is the case, the default
+ command line for preprocessing contains more options.
+ *)
+
+ val keep_comments: bool
+ (** [true] if the default preprocessor selected during compilation is
+ able to keep comments (hence ACSL annotations) in its output.
+ *)
+
+ val supported_arch_options: string list
+ (** architecture-related options (e.g. -m32) known to be supported by
+ the default preprocessor. Used to match preprocessor commands to
+ selected machdeps.
+ *)
+end
+
+(** Default user directories
+ Unless you are working in the kernel of Frama-C, you should not use this. *)
+module User_dirs : sig
+ val cache: unit -> Filepath.Normalized.t
+ (** Where Frama-C should read/write cached files. *)
+
+ val config: unit -> Filepath.Normalized.t
+ (** Where Frama-C should read/write config files. *)
+
+ val state: unit -> Filepath.Normalized.t
+ (** Where Frama-C should read/write state files *)
+end
+
+val is_gui: bool
+(** Is the Frama-C GUI running? *)
+
+
+(*
+ Local Variables:
+ compile-command: "make -C ../../.."
+ End:
+*)
diff --git a/src/kernel_internals/runtime/unix_dirs.ml b/src/kernel_internals/runtime/unix_dirs.ml
new file mode 100644
index 0000000000000000000000000000000000000000..770c0130023dfa28ac73f96df625eacacb68a479
--- /dev/null
+++ b/src/kernel_internals/runtime/unix_dirs.ml
@@ -0,0 +1,42 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+let home () =
+ match Sys.getenv "HOME" with
+ | "" -> raise Not_found
+ | s -> Filepath.Normalized.of_string s
+
+let env_or_default env default =
+ let open Filepath.Normalized in
+ let location =
+ match Sys.getenv_opt env with
+ | Some env when env <> "" -> of_string env
+ | _ -> concats (home ()) default
+ in
+ concat location "frama-c"
+
+let cache () =
+ env_or_default "XDG_CACHE_HOME" [ ".cache" ]
+let config () =
+ env_or_default "XDG_CONFIG_HOME" [ ".config" ]
+let state () =
+ env_or_default "XDG_STATE_HOME" [ ".local" ; "state" ]
diff --git a/src/kernel_internals/runtime/win_dirs.ml b/src/kernel_internals/runtime/win_dirs.ml
new file mode 100644
index 0000000000000000000000000000000000000000..5745da20b15a5b6eb7d3ca69eecac54434f6218b
--- /dev/null
+++ b/src/kernel_internals/runtime/win_dirs.ml
@@ -0,0 +1,35 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+let env_or_default env default sub =
+ let open Filepath.Normalized in
+ match Sys.getenv_opt env, sub with
+ | Some s, _ (* ignored *) when s <> "" -> concat (of_string s) "frama-c"
+ | _, Some sub -> concats (of_string default) [ "frama-c" ; sub ]
+ | _, None -> concat (of_string default) "frama-c"
+
+let cache () =
+ env_or_default "XDG_CACHE_HOME" (Sys.getenv "TEMP") None
+let config () =
+ env_or_default "XDG_CONFIG_HOME" (Sys.getenv "LOCALAPPDATA") (Some "config")
+let state () =
+ env_or_default "XDG_STATE_HOME" (Sys.getenv "LOCALAPPDATA") (Some "state")
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 8258d59539142532eb1ef57860b55587a8aca240..6c2cd09b4ae3b7d7309a91cddaa17d97c76b9915 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -339,7 +339,7 @@ let process_stdlib_pragma name args =
match args with
| [ ACons ("pop",_) ] -> pop_stdheader (); None
| [ ACons ("push",_); AStr s ] ->
- let base_name = (Fc_config.framac_libc:>string) in
+ let base_name = (System_config.Share.libc:>string) in
let relative_name = Filepath.relativize ~base_name s in
push_stdheader relative_name;
None
diff --git a/src/kernel_services/ast_queries/cil_builtins.ml b/src/kernel_services/ast_queries/cil_builtins.ml
index 76e4ec86b744821c06c724548a61668fe2f7daeb..1a6dc1cdbda38ab9379de4084625ef1b51742409 100644
--- a/src/kernel_services/ast_queries/cil_builtins.ml
+++ b/src/kernel_services/ast_queries/cil_builtins.ml
@@ -387,16 +387,14 @@ let instantiate_available_templates type_table name (entry : builtin_template) =
let init_gcc_builtin_templates () =
let fp =
- Datatype.Filepath.concat ~existence:Filepath.Must_exist
- Fc_config.datadir "compliance/gcc_builtins.json"
+ Kernel.Share.get_file "compliance/gcc_builtins.json"
in
Json.init_builtin_templates ~default_compiler:GCC fp;
Gcc_builtin_templates_loaded.set true
let init_other_builtin_templates () =
let fp =
- Datatype.Filepath.concat ~existence:Filepath.Must_exist
- Fc_config.datadir "compliance/compiler_builtins.json"
+ Kernel.Share.get_file "compliance/compiler_builtins.json"
in
Json.init_builtin_templates fp
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 24615768362c0e13990a0290256f6203ac723b56..234bd09e5f6a41fd1fc26b8e4cdbfa6958764ba3 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -81,9 +81,9 @@ let cpp_opt_kind () =
else Unknown
let is_cpp_gnu_like () =
- let open Fc_config in
+ let open System_config.Preprocessor in
let cpp_cmd = Kernel.CppCommand.get () in
- match cpp_cmd = "", using_default_cpp, preprocessor_is_gnu_like with
+ match cpp_cmd = "", is_default, is_gnu_like with
| true, true, true -> Gnu
| true, true, false -> Not_gnu
| _, _, _ -> cpp_opt_kind ()
@@ -92,10 +92,10 @@ let is_cpp_gnu_like () =
If the program has an explicit argument -cpp-command "XX -Y"
(quotes are required by the shell)
then XX -Y
- else use the command in [Fc_config.preprocessor].*)
+ else use the command in [System_config.Preprocessor.command].*)
let get_preprocessor_command () =
let cmdline = Kernel.CppCommand.get() in
- if cmdline <> "" then cmdline else Fc_config.preprocessor
+ if cmdline <> "" then cmdline else System_config.Preprocessor.command
let from_filename ?cpp f =
let cpp =
@@ -130,7 +130,7 @@ let from_filename ?cpp f =
if Hashtbl.mem check_suffixes suf then
External (f, suf)
else if cpp <> "" then begin
- if not Fc_config.preprocessor_keep_comments then
+ if not System_config.Preprocessor.keep_comments then
Kernel.warning ~once:true
"Default preprocessor does not keep comments. Any ACSL annotations \
on non-preprocessed files will be discarded.";
@@ -270,7 +270,7 @@ let print_machdep fmt (m : Cil_types.mach) =
(if m.has__builtin_va_list then "has" else "has not") ;
end
-let machdep_dir () = Kernel.Share.get_dir ~mode:`Must_exist "machdeps"
+let machdep_dir () = Kernel.Share.get_dir "machdeps"
let regexp_machdep = Str.regexp "^machdep_\\([^.]*\\).yaml$"
@@ -490,7 +490,7 @@ let build_cpp_cmd = function
let machdep_dir =
Machdep.generate_machdep_header ~censored_macros (get_machdep())
in
- [(machdep_dir:>string); (Fc_config.framac_libc:>string)]
+ [(machdep_dir:>string); (System_config.Share.libc:>string)]
end
else []
in
@@ -1865,7 +1865,7 @@ let init_from_cmdline () =
Project.set_current prj2;
end;
let files = Kernel.Files.get () in
- if files = [] && not Fc_config.is_gui then Kernel.warning "no input file.";
+ if files = [] && not System_config.is_gui then Kernel.warning "no input file.";
let files = List.map (fun f -> from_filename f) files in
try
init_from_c_files files;
diff --git a/src/kernel_services/cmdline_parameters/cmdline.ml b/src/kernel_services/cmdline_parameters/cmdline.ml
index 30740f790341dca5d1a0c8618e07a341a2c0b259..3611c1f588e244c6ed8425cabf6db9acb4a775c3 100644
--- a/src/kernel_services/cmdline_parameters/cmdline.ml
+++ b/src/kernel_services/cmdline_parameters/cmdline.ml
@@ -84,7 +84,7 @@ let long_plugin_name s =
if s = Log.kernel_label_name then "Frama-C" else "Plug-in " ^ s
let additional_info () =
- if Fc_config.is_gui then
+ if System_config.is_gui then
"\nReverting to previous state.\n\
Check the Console tab for additional information."
else
@@ -114,7 +114,7 @@ let request_crash_report =
Note that a version and a backtrace alone often do not contain enough\n\
information to understand the bug. Guidelines for reporting bugs are at:\n\
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs\n"
- Fc_config.version_and_codename
+ System_config.Version.id_and_codename
let protect = function
| Sys.Break ->
@@ -1033,7 +1033,7 @@ let plugin_help shortname =
let help () =
Log.print_on_output
begin fun fmt ->
- Format.fprintf fmt "\nThis is Frama-C %s\n" Fc_config.version_and_codename ;
+ Format.fprintf fmt "\nThis is Frama-C %s\n" System_config.Version.id_and_codename ;
Format.fprintf fmt "\nUsage:\n %s [options files ...]\n" Sys.argv.(0) ;
let print_line fmt s =
Format.(pp_print_string fmt s ; pp_print_newline fmt ()) in
diff --git a/src/kernel_services/cmdline_parameters/parameter_builder.ml b/src/kernel_services/cmdline_parameters/parameter_builder.ml
index 2c8544e8f2571a06e9fe2780e0f9706f372bb64e..8bba9b1b4f4f0d9a1894b4846fad0da64c8995f6 100644
--- a/src/kernel_services/cmdline_parameters/parameter_builder.ml
+++ b/src/kernel_services/cmdline_parameters/parameter_builder.ml
@@ -537,6 +537,100 @@ struct
let is_empty () = Filepath.Normalized.is_empty (get ())
end
+ (* ************************************************************************ *)
+ (** {3 Make_*_dir} *)
+ (* ************************************************************************ *)
+
+ (** Builds a Site_dir from an existing one. The corresponding directory always
+ performs a full path resolution.
+
+ @since Frama-C+dev
+ *)
+ module Make_site_dir
+ (Parent: Parameter_sig.Site_dir)
+ (Info: sig val name: string end)
+ : Parameter_sig.Site_dir
+ =
+ struct
+ (* Note: it recursively rebuilds the path relative to the root directory,
+ until we reach the root and resolve the path. *)
+ let get_dir name = Parent.get_dir (Info.name ^ "/" ^ name)
+ let get_file name = Parent.get_file (Info.name ^ "/" ^ name)
+ end
+
+ (** Builds a User_dir from an existing one.
+
+ @since Frama-C+dev
+ *)
+ module Make_user_dir
+ (Parent: Parameter_sig.User_dir)
+ (Info: sig val name: string end)
+ : Parameter_sig.User_dir
+ =
+ struct
+ let get_dir ?create_path name =
+ Parent.get_dir ?create_path (Info.name ^ "/" ^ name)
+ let get_file ?create_path name =
+ Parent.get_file ?create_path (Info.name ^ "/" ^ name)
+ end
+
+ module Make_user_dir_opt
+ (Parent: Parameter_sig.User_dir)
+ (Info: sig
+ include Parameter_sig.Input_with_arg
+ val env: string option
+ val dirname: string
+ end): Parameter_sig.User_dir_opt
+ =
+ struct
+ open Fc_Filepath.Normalized
+
+ module Dir_name =
+ Filepath
+ (struct
+ include Info
+ let existence = Fc_Filepath.Indifferent
+ let file_kind = ""
+ end)
+
+ let get () =
+ if Dir_name.is_set () then Dir_name.get ()
+ else
+ match Option.bind Info.env Sys.getenv_opt with
+ | Some s when s <> "" -> of_string s
+ | _ -> Parent.get_dir Info.dirname
+
+ let set = Dir_name.set
+ let is_set = Dir_name.is_set
+
+ let expected ~dir path =
+ if dir <> Fc_Filepath.is_dir path then
+ P.L.abort "%a is expected to be a %s"
+ pretty path (if dir then "directory" else "file")
+
+ let mk_dir d =
+ try ignore @@ Extlib.mkdir ~parents:true d 0o755
+ with Unix.Unix_error _ ->
+ P.L.abort "cannot create %s directory `%a'" Info.dirname pretty d
+
+ let get_dir ?(create_path=false) s =
+ let dir = concat (get ()) s in
+ if Fc_Filepath.exists dir
+ then (expected ~dir:true dir ; dir)
+ else if create_path
+ then (mk_dir dir ; dir)
+ else dir
+
+ let get_file ?create_path s =
+ let base_dir = get_dir ?create_path @@ Filename.dirname s in
+ (* No need to create anything here, as the path of sub-directories has
+ been already created by [get_dir] for computing [base_dir]. *)
+ let path = concat base_dir @@ Filename.basename s in
+ if Fc_Filepath.exists path then
+ expected ~dir:false path ;
+ path
+ end
+
(* ************************************************************************ *)
(** {3 Custom parameters} *)
(* ************************************************************************ *)
diff --git a/src/kernel_services/cmdline_parameters/parameter_sig.ml b/src/kernel_services/cmdline_parameters/parameter_sig.ml
index c07ef6b5afc0021aa92676853801dc1eacc6deb0..6d04fc0d819da735a5d1527572ab7421b3652656 100644
--- a/src/kernel_services/cmdline_parameters/parameter_sig.ml
+++ b/src/kernel_services/cmdline_parameters/parameter_sig.ml
@@ -324,43 +324,100 @@ module type Filepath = sig
val is_empty: unit -> bool
end
-(** signature for searching files in a specific directory. *)
-module type Specific_dir = sig
+(** Dune site directories (share, lib, ...) and subdirectories.
+ They are connected to a root module (see {!Site_root}), that may not be
+ unique, and these are considered as installed files (although the user might
+ provide another location).
+ @since Frama-C+dev
+*)
+module type Site_dir = sig
+ val get_dir: string -> Filepath.Normalized.t
+ (** [get_dir name] tries to find the directory named [name] in the
+ site. The function aborts if: [name] cannot be found or is a file instead
+ of a directory, otherwise it returns the path.
+
+ Be careful! This function finds the first directory that exists in the
+ site path. Thus, by extending this path, we get *only* the subdirs and
+ files in this directory, not in all directories of same name.
+ {!Builder.Make_site_dir} can be used to get directories that will always
+ perform the resolution.
+ *)
+
+ val get_file: string -> Filepath.Normalized.t
+ (** [get_file name] tries to find the file named [name] in the
+ site. The function aborts if: [name] cannot be found or is a directory
+ instead of a file, otherwise it returns the path.
+ *)
+end
+
+(** Dune site roots (share, lib, ...).
+
+ @since Frama-C+dev
+*)
+module type Site_root = sig
val set: Filepath.Normalized.t -> unit
- (** Sets the plugin <specific-dir> directory (without creating it). *)
+ (** Sets the <dune-site-dir> directory (without creating it). *)
val get: unit -> Filepath.Normalized.t
- (** @return the plugin <specific-dir> directory (without creating it). *)
+ (** @return the <dune-site-dir> directory (without creating it). *)
val is_set: unit -> bool
- (** @return whether the plugin <specific-dir> has been set. *)
-
- val get_dir:
- ?mode:[`Normalize_only | `Create_path | `Must_exist ] ->
- string ->
- Filepath.Normalized.t
- (** [get_dir ?mode p] returns a (local) path [p], i.e. relative to the plugin
- <specific-dir> directory, of a sub-directory of the plugin <specific-dir>
- directory.
- @param mode determines how to handle the resulting path:
- + [Normalize_only] just normalizes the resulting path (default).
- + [Create_path] creates the resulting path, if does not exist.
- + [Must_exist] aborts if the resulting path does not exist. *)
-
- val get_file:
- ?mode:[`Normalize_only | `Create_path | `Must_exist ] ->
- string ->
- Filepath.Normalized.t
- (** [get_file ?mode p] returns a (local) path [p], i.e. relative to the
- plugin <specific-dir> directory, of a file in the plugin <specific-dir>
- directory.
- @param mode determines how to handle the resulting path:
- + [Normalize_only] just normalizes the resulting path (default).
- + [Create_path] creates the dirname of resulting path, if does not exist.
- + [Must_exist] aborts if the resulting path does not exist. *)
+ (** @return whether the <dune-site-dir> has been set. *)
+
+ include Site_dir
end
+(** User directories (session, config, state, ...).
+ We do not expect these directories/files to exist. Several roots are
+ provided in {!Plugin}, namely {!Plugin.Session}, {!Plugin.Cache_dir},
+ {!Plugin.Config_dir} and {!Plugin.State_dir}.
+
+ @since Frama-C+dev
+*)
+module type User_dir = sig
+ val get_dir: ?create_path:bool -> string -> Filepath.Normalized.t
+ (** [get_dir ~create_path name] tries to get the directory [name].
+ The function aborts if:
+ - a file named [name] exists,
+ - creating a the directory fails.
+
+ Otherwise returns the path, and creates it if [create_path] is true
+ (it defaults to false). Subdirectories modules can be created with
+ {!Builder.Make_user_dir} and {!Builder.Make_user_dir_opt}.
+ *)
+
+ val get_file: ?create_path:bool -> string -> Filepath.Normalized.t
+ (** [get_file ~create_path name] tries to get the file [name].
+ The function aborts if:
+ - a directory named [name] exists,
+ - creating the path to the file fails.
+
+ Otherwise returns the path, and creates the directories that lead to the
+ file if [create_path] is true (it defaults to false). The file is *not*
+ created by the function.
+ *)
+end
+
+(** Basically {!User_dir} but with an option to override the original path.
+
+ @since Frama-C+dev
+*)
+module type User_dir_opt = sig
+ include User_dir
+
+ val set: Filepath.Normalized.t -> unit
+ (** Sets the <user-dir> directory (without creating it). *)
+
+ val get: unit -> Filepath.Normalized.t
+ (** @return the <user-dir> directory (without creating it). *)
+
+ val is_set: unit -> bool
+ (** @return whether the <user-dir> has been set. *)
+end
+
+
+
(* ************************************************************************** *)
(** {3 Collections} *)
(* ************************************************************************** *)
@@ -573,6 +630,47 @@ module type Builder = sig
and vice-versa. *)
end): Filepath
+ (** Builds a {!Site_dir} from an existing one. The first parameter is the
+ parent directory. The second gives the name of the directory to create.
+
+ @since Frama-C+dev
+ *)
+ module Make_site_dir
+ (_: Site_dir)
+ (_: sig val name: string end)
+ : Site_dir
+
+
+ (** Builds a {!User_dir} from an existing one. The first parameter is the
+ parent directory. The second gives the name of the directory to create.
+
+ @since Frama-C+dev
+ *)
+ module Make_user_dir
+ (_: User_dir)
+ (_: sig val name: string end)
+ : User_dir
+
+ (** Builds a {!User_dir_opt} from an existing {!User_dir}. The first parameter
+ is the parent directory. The second gives the name of the directory to
+ create (also used to create the option name), a possible environment
+ variable name and the help message for the option.
+
+ @since Frama-C+dev
+ *)
+ module Make_user_dir_opt
+ (_: User_dir)
+ (_: sig
+ include Input_with_arg
+ val env: string option
+ (** Can be used to provide an environment variable that can be used
+ instead of the option. The option has higher priority.
+ *)
+
+ val dirname: string
+ (** The name of the directory *)
+ end): User_dir_opt
+
(** Allow using custom types as parameters.
@since 29.0-Copper *)
module Custom(X: sig
diff --git a/src/kernel_services/plugin_entry_points/dynamic.ml b/src/kernel_services/plugin_entry_points/dynamic.ml
index cc95ee4b7bb853d1db8b96409f3a0e0ca1e0cae1..3efe5f97b041b73cbab392862554201c989f0497 100644
--- a/src/kernel_services/plugin_entry_points/dynamic.ml
+++ b/src/kernel_services/plugin_entry_points/dynamic.ml
@@ -119,11 +119,15 @@ let load_packages pkgs =
(* -------------------------------------------------------------------------- *)
let load_plugin_path () =
- if Fc_config.is_gui then Config_data.Plugins.Plugins_gui.load_all ();
- Config_data.Plugins.Plugins.load_all ()
+ System_config.Plugins.load_all ()
let load_plugin m =
- Config_data.Plugins.Plugins.load m
+ try System_config.Plugins.load m
+ (* Ok, this is ugly, but Dune Site does not give any way to catch this ...
+ Note that we abort with a user error.
+ *)
+ with e -> Klog.abort "Failed to load plug-in %S@.Exception: %s" m
+ (Printexc.to_string e)
let load_module m =
let base,ext = split_ext m in
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index d4fff3d5b98449f14cd15cbd8ed2581f013ee6ba..792ea61154286dd65b41f44ee1967eb682a259c1 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -28,6 +28,7 @@ module FcPlugin = Plugin
let () = Plugin.register_kernel ()
+let () = Plugin.is_session_visible ()
module P = Plugin.Register
(struct
let name = ""
@@ -735,7 +736,7 @@ module PrintLibc =
let option_name = "-print-libc"
let help = "when pretty-printing C code, keep prototypes coming \
from Frama-C standard library"
- let default = Fc_config.is_gui (* always print by default on the GUI *)
+ let default = System_config.is_gui (* always print by default on the GUI *)
end)
let () = Parameter_customize.set_group inout_source
@@ -961,33 +962,31 @@ let () = Cmdline.load_all_plugins := bootstrap_loader
let () = Parameter_customize.set_cmdline_stage Cmdline.Extending
let () = Parameter_customize.set_group saveload
let () = Parameter_customize.do_not_projectify ()
-module Session_dir =
- P.Filepath
- (struct
- let option_name = "-session"
- let arg_name = "path"
- let existence = Filepath.Indifferent
- let file_kind = "directory"
- let help = "directory in which session files are searched"
- end)
+module Session_dir = Session
let () = Plugin.session_is_set_ref := Session_dir.is_set
let () = Plugin.session_ref := Session_dir.get
let () = Parameter_customize.set_cmdline_stage Cmdline.Extending
let () = Parameter_customize.set_group saveload
let () = Parameter_customize.do_not_projectify ()
-module Config_dir =
- P.Filepath
- (struct
- let option_name = "-config"
- let arg_name = "path"
- let existence = Filepath.Indifferent
- let file_kind = "directory"
- let help = "directory in which configuration files are searched"
- end)
+module Cache_dir = Cache_dir ()
+let () = Plugin.cache_is_set_ref := Cache_dir.is_set
+let () = Plugin.cache_ref := Cache_dir.get
+
+let () = Parameter_customize.set_cmdline_stage Cmdline.Extending
+let () = Parameter_customize.set_group saveload
+let () = Parameter_customize.do_not_projectify ()
+module Config_dir = Config_dir ()
let () = Plugin.config_is_set_ref := Config_dir.is_set
let () = Plugin.config_ref := Config_dir.get
+let () = Parameter_customize.set_cmdline_stage Cmdline.Extending
+let () = Parameter_customize.set_group saveload
+let () = Parameter_customize.do_not_projectify ()
+module State_dir = State_dir ()
+let () = Plugin.state_is_set_ref := State_dir.is_set
+let () = Plugin.state_ref := State_dir.get
+
(* ************************************************************************* *)
(** {2 Parsing} *)
(* ************************************************************************* *)
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 13e35743a12a0bde3dc27e575bdf4e1bcd98023d..33076ff8e300aa22381f31d9c7e4094044c52b9b 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -412,18 +412,28 @@ module LoadLibrary: Parameter_sig.String_list
module AutoLoadPlugins: Parameter_sig.Bool
(** Behavior of option "-autoload-plugins" *)
-module Session_dir: Parameter_sig.Filepath
+module Session_dir: Parameter_sig.User_dir
(** Directory in which session files are searched.
@since Neon-20140301
@before 23.0-Vanadium parameter type was string instead of Filepath.
*)
-module Config_dir: Parameter_sig.Filepath
+module Cache_dir: Parameter_sig.User_dir
+(** Directory in which cache files are searched.
+ @since Frama-C+dev
+*)
+
+module Config_dir: Parameter_sig.User_dir
(** Directory in which config files are searched.
@since Neon-20140301
@before 23.0-Vanadium parameter type was string instead of Filepath.
*)
+module State_dir: Parameter_sig.User_dir
+(** Directory in which state files are searched.
+ @since Frama-C+dev
+*)
+
(* this stop special comment does not work as expected (and as explained in the
OCamldoc manual, Section 15.2.2. It just skips all the rest of the file
instead of skipping until the next stop comment...
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index 8ed97729a29b2f52953d487f16b4fb484e891332..6b8cb5198259983f2495a8dc889f9cb3060201aa 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -27,8 +27,12 @@ let empty_string = ""
let positive_debug_ref = ref 0
let session_is_set_ref = Extlib.mk_fun "session_is_set_ref"
let session_ref = Extlib.mk_fun "session_ref"
+let cache_is_set_ref = Extlib.mk_fun "cache_is_set_ref"
+let cache_ref = Extlib.mk_fun "cache_ref"
let config_is_set_ref = Extlib.mk_fun "config_is_set_ref"
let config_ref = Extlib.mk_fun "config_ref"
+let state_is_set_ref = Extlib.mk_fun "state_is_set_ref"
+let state_ref = Extlib.mk_fun "state_ref"
(* ************************************************************************* *)
(** {2 Signatures} *)
@@ -38,9 +42,11 @@ module type S_no_log = sig
val add_group: ?memo:bool -> string -> Cmdline.Group.t
module Verbose: Parameter_sig.Int
module Debug: Parameter_sig.Int
- module Share: Parameter_sig.Specific_dir
- module Session: Parameter_sig.Specific_dir
- module Config: Parameter_sig.Specific_dir
+ module Share: Parameter_sig.Site_root
+ module Session: Parameter_sig.User_dir_opt
+ module Cache_dir () : Parameter_sig.User_dir_opt
+ module Config_dir () : Parameter_sig.User_dir_opt
+ module State_dir () : Parameter_sig.User_dir_opt
val help: Cmdline.Group.t
val messages: Cmdline.Group.t
val add_plugin_output_aliases:
@@ -82,9 +88,6 @@ let is_share_visible () = share_visible_ref := true
let session_visible_ref = ref false
let is_session_visible () = session_visible_ref := true
-let config_visible_ref = ref false
-let is_config_visible () = config_visible_ref := true
-
let plugin_subpath_ref = ref None
let plugin_subpath s = plugin_subpath_ref := Some s
@@ -94,7 +97,6 @@ let reset_plugin () =
kernel := false;
share_visible_ref := false;
session_visible_ref := false;
- config_visible_ref := false;
plugin_subpath_ref := None;
default_msg_keys_ref := [];
;;
@@ -289,213 +291,173 @@ struct
(** {3 Specific directories} *)
(* ************************************************************************ *)
- module Make_specific_dir
- (O: Parameter_sig.Input_with_arg)
+ module Share : Parameter_sig.Site_root = struct
+ let is_visible = !share_visible_ref
+ let is_kernel = is_kernel () (* the side effect must be applied right now *)
+
+ let () =
+ Parameter_customize.set_cmdline_stage Cmdline.Extended;
+ if is_visible then Parameter_customize.is_reconfigurable ()
+ else Parameter_customize.is_invisible ()
+
+ module Dir_name =
+ Filepath
+ (struct
+ let option_name = prefix ^ "share"
+ let arg_name = "dir"
+ let help =
+ if is_visible then
+ "set the plug-in share directory to <dir> (may be used if the \
+ plug-in is not installed at the same place as Frama-C)"
+ else empty_string
+ let existence = Fc_Filepath.Must_exist
+ let file_kind = ""
+ end)
+
+ let set filepath = Dir_name.set filepath
+ let get () = Dir_name.get ()
+ let is_set () = Dir_name.is_set ()
+
+ let add_plugin path =
+ if is_kernel then path
+ else Fc_Filepath.Normalized.concat path plugin_subpath
+
+ let dirs () =
+ if is_visible && is_set () then [ get () ]
+ else List.map add_plugin System_config.Share.dirs
+
+ let find ~is_dir relative =
+ let exception Found of Fc_Filepath.Normalized.t in
+ let check_presence dir =
+ let path = Fc_Filepath.Normalized.concat dir relative in
+ if Fc_Filepath.exists path then raise (Found path)
+ in
+ try
+ List.iter check_presence (dirs ()) ;
+ L.abort
+ "Could not find %s %s in Frama-C%s share"
+ (if is_dir then "directory" else "file")
+ relative
+ (if is_kernel then "" else "/" ^ P.name)
+ with
+ | Found path when is_dir <> Fc_Filepath.is_dir path ->
+ L.abort "%a is expected to be a %s"
+ Fc_Filepath.Normalized.pretty path
+ (if is_dir then "directory" else "file")
+ | Found path -> path
+
+ let get_dir = find ~is_dir:true
+ let get_file = find ~is_dir:false
+ end
+
+ module Make_user_dir_root
(D: sig
- val dirs: unit -> Fc_Filepath.Normalized.t list
- val visible_ref: bool
+ val name : string
+ val default_root : unit -> Fc_Filepath.Normalized.t
+ val kernel_get : unit -> Fc_Filepath.Normalized.t
+ val is_visible : bool
end)
=
struct
+ open Fc_Filepath.Normalized
- let is_visible = D.visible_ref
- let is_kernel = is_kernel () (* the side effect must be applied right now *)
+ let is_visible = D.is_visible
+ let is_kernel = P.name = ""
let () =
Parameter_customize.set_cmdline_stage Cmdline.Extended;
if is_visible then Parameter_customize.is_reconfigurable ()
else Parameter_customize.is_invisible ()
+ let prefix = if is_kernel then "-" else prefix
+ let var_name =
+ Stdlib.String.uppercase_ascii
+ ("FRAMAC_" ^ (if is_kernel then "" else P.shortname ^ "_") ^ D.name)
+
module Dir_name =
Filepath
(struct
- let option_name = prefix ^ O.option_name
- let arg_name = O.arg_name
- let help = if is_visible then O.help else empty_string
+ let option_name = prefix ^ D.name
+ let arg_name = "dir"
+ let help =
+ if is_visible && is_kernel
+ then Format.asprintf "set the Frama-C %s directory to <dir>" D.name
+ else
+ if is_visible
+ then Format.asprintf "set the plug-in %s directory to <dir>" D.name
+ else empty_string
+
let existence = Fc_Filepath.Indifferent
let file_kind = ""
end)
- let mk_dir d =
- let d' = Fc_Filepath.Normalized.of_string d in
- try
- if Extlib.mkdir ~parents:true d' 0o755 then
- L.warning "created %s directory `%a'" O.option_name Fc_Filepath.Normalized.pretty d';
- d
- with Unix.Unix_error _ ->
- L.abort "cannot create %s directory `%a'" O.option_name Fc_Filepath.Normalized.pretty d'
-
- let set filepath = Dir_name.set filepath
- let get () = Dir_name.get ()
- let is_set () = Dir_name.is_set ()
+ let get () =
+ if Dir_name.is_set () then Dir_name.get ()
+ else match Sys.getenv_opt var_name with
+ | Some s when s <> "" -> of_string s
+ | _ when is_kernel -> D.default_root ()
+ | _ -> concat (D.kernel_get ()) P.shortname
- let base_dirs () =
- (* Get the specified dir if any. *)
- let plugin_base_dir =
- if is_visible
- then Dir_name.get ()
- else Datatype.Filepath.dummy
- in
- if not (plugin_base_dir = Datatype.Filepath.dummy)
- then [plugin_base_dir]
- else begin
- (* No specified dir: look for the default ones.
- At least one default value must be in place. *)
- let dirs = D.dirs () in
- assert (dirs <> []);
- if is_kernel
- then dirs
- else
- List.map
- (fun x -> Datatype.Filepath.concat x plugin_subpath)
- dirs
- end
+ let set = Dir_name.set
+ let is_set = Dir_name.is_set
- let get_dir ?(mode=`Normalize_only) s =
- match mode with
- | `Must_exist ->
- begin
- let dir =
- let exception Found of Datatype.Filepath.t in
- try
- List.fold_left
- (fun dummy d ->
- let name = Datatype.Filepath.concat d s in
- if Fc_Filepath.exists name
- then raise (Found name)
- else dummy)
- None
- (base_dirs ())
- with Found d ->
- Some d
- in
- match dir with
- | None ->
- let pp_path fmt (path:Dir_name.t) =
- Format.pp_print_string fmt (path :> string)
- in
- let pp_subdir fmt = function
- | "." -> ()
- | s -> Format.fprintf fmt " sub-directory %s in " s
- in
- L.abort "there is no%a %s directories: %a"
- pp_subdir s
- O.option_name
- (Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt ", ") pp_path)
- (base_dirs ())
- | Some d -> d
- end
- | _ ->
- begin
- (* In presence of more than one base directory, consider the first to
- form the resulting [filepath]. *)
- let filepath =
- match base_dirs () with
- | [] -> assert false
- | d :: _ -> Datatype.Filepath.concat d s
- in
- match mode with
- | `Must_exist ->
- (* Already taken care of. *)
- assert false
- | `Normalize_only ->
- filepath
- | `Create_path ->
- begin
- (try
- if not (Fc_Filepath.is_dir filepath)
- then
- (* [filepath] already exists, and it is a file. *)
- L.abort
- "cannot create directory as file %a already exists"
- Datatype.Filepath.pretty filepath
- with Sys_error _ ->
- (* [filepath] does not exist: create the directory path. *)
- ignore (mk_dir (filepath :> string)));
- filepath
- end
- end
-
- let get_file ?(mode=`Normalize_only) s =
- let s_dirname = Filename.dirname s in
- let base_dir = get_dir ~mode s_dirname in
- let s_basename = Filename.basename s in
- let filepath = Datatype.Filepath.concat base_dir s_basename in
- match mode with
- | `Must_exist ->
- if Fc_Filepath.exists filepath
- then filepath
- else L.abort "there is no file %s in %s directories" (filepath :> string) O.option_name
- | `Normalize_only ->
- filepath
- | `Create_path ->
- (* No need to create anything here, as the path of sub-directories has
- been already created by [get_dir] for computing [base_dir]. *)
- filepath
+ let expected ~dir path =
+ if dir <> Fc_Filepath.is_dir path then
+ L.abort "%a is expected to be a %s"
+ pretty path (if dir then "directory" else "file")
+ let mk_dir d =
+ try ignore @@ Extlib.mkdir ~parents:true d 0o755
+ with Unix.Unix_error _ ->
+ L.abort "cannot create %s directory `%a'" D.name pretty d
+
+ let get_dir ?(create_path=false) s =
+ let dir = concat (get ()) s in
+ if Fc_Filepath.exists dir
+ then (expected ~dir:true dir ; dir)
+ else if create_path
+ then (mk_dir dir ; dir)
+ else dir
+
+ let get_file ?create_path s =
+ let base_dir = get_dir ?create_path @@ Filename.dirname s in
+ (* No need to create anything here, as the path of sub-directories has
+ been already created by [get_dir] for computing [base_dir]. *)
+ let path = concat base_dir @@ Filename.basename s in
+ if Fc_Filepath.exists path then expected ~dir:false path ;
+ path
end
- module Share =
- Make_specific_dir
+ module Session = Make_user_dir_root
(struct
- let option_name = "share"
- let arg_name = "dir"
- let help = "set the plug-in share directory to <dir> \
- (may be used if the plug-in is not installed at the same place as Frama-C)"
- end)
- (struct
- let dirs () = Fc_config.datadirs
- let visible_ref = !share_visible_ref
+ let name = "session"
+ let default_root () = Fc_Filepath.Normalized.of_string "./.frama-c"
+ let kernel_get () = !session_ref ()
+ let is_visible = !session_visible_ref
end)
- module Session =
- Make_specific_dir
- (struct
- let option_name = "session"
- let arg_name = "dir"
- let help = "set the plug-in session directory to <dir>"
- end)
+ module Cache_dir () = Make_user_dir_root
(struct
- let dirs () = [
- if !session_is_set_ref () then !session_ref ()
- else
- Fc_Filepath.Normalized.of_string
- (try Sys.getenv "FRAMAC_SESSION"
- with Not_found -> "./.frama-c")
- ]
- let visible_ref = !session_visible_ref
+ let name = "cache"
+ let default_root = System_config.User_dirs.cache
+ let kernel_get () = !cache_ref ()
+ let is_visible = !Parameter_customize.is_visible_ref
end)
- module Config =
- Make_specific_dir
+ module Config_dir () = Make_user_dir_root
(struct
- let option_name = "config"
- let arg_name = "dir"
- let help = "set the plug-in config directory to <dir> \
- (may be used on systems with no default user directory)"
+ let name = "config"
+ let default_root = System_config.User_dirs.config
+ let kernel_get () = !config_ref ()
+ let is_visible = !Parameter_customize.is_visible_ref
end)
+
+ module State_dir () = Make_user_dir_root
(struct
- let dirs () = [
- let to_path = Fc_Filepath.Normalized.of_string in
- let d, vis =
- if !config_is_set_ref () then !config_ref (), false
- else
- try to_path (Sys.getenv "FRAMAC_CONFIG"), false
- with Not_found ->
- try to_path (Sys.getenv "USERPROFILE"), false (* Win32 *)
- with Not_found ->
- (* Unix like *)
- try to_path (Sys.getenv "XDG_CONFIG_HOME"), true
- with Not_found ->
- try
- Fc_Filepath.Normalized.concat
- (to_path (Sys.getenv "HOME")) ".config", true
- with Not_found -> to_path ".", false
- in
- Fc_Filepath.Normalized.concat
- d (if vis then "frama-c" else ".frama-c")
- ]
- let visible_ref = !config_visible_ref
+ let name = "state"
+ let default_root = System_config.User_dirs.state
+ let kernel_get () = !state_ref ()
+ let is_visible = !Parameter_customize.is_visible_ref
end)
let help = add_group "Getting Information"
diff --git a/src/kernel_services/plugin_entry_points/plugin.mli b/src/kernel_services/plugin_entry_points/plugin.mli
index 887bdc5befc77e2ff76837694e78a33d6a24b97f..ead0e265436204b8c0ca83908914de35f928c6b3 100644
--- a/src/kernel_services/plugin_entry_points/plugin.mli
+++ b/src/kernel_services/plugin_entry_points/plugin.mli
@@ -44,16 +44,33 @@ module type S_no_log = sig
module Debug: Parameter_sig.Int
(** Handle the specific `share' directory of the plug-in.
- @since Oxygen-20120901 *)
- module Share: Parameter_sig.Specific_dir
+ @since Oxygen-20120901
+ @before Frama-C+dev more modes were allowed
+ *)
+ module Share: Parameter_sig.Site_root
(** Handle the specific `session' directory of the plug-in.
- @since Neon-20140301 *)
- module Session: Parameter_sig.Specific_dir
+ @since Neon-20140301
+ @before Frama-C+dev Session was a Specific_dir.
+ *)
+ module Session: Parameter_sig.User_dir_opt
+
+ (** Handle the specific `cache' directory of the plug-in.
+ @since Frama-C+dev
+ *)
+ module Cache_dir (): Parameter_sig.User_dir_opt
(** Handle the specific `config' directory of the plug-in.
- @since Neon-20140301 *)
- module Config: Parameter_sig.Specific_dir
+ @since Neon-20140301
+ @before Frama-C+dev this was not a functor and one could expect the
+ directory to exist
+ *)
+ module Config_dir (): Parameter_sig.User_dir_opt
+
+ (** Handle the specific `state' directory of the plug-in.
+ @since Frama-C+dev
+ *)
+ module State_dir (): Parameter_sig.User_dir_opt
val help: Cmdline.Group.t
(** The group containing option -*-help.
@@ -131,11 +148,6 @@ val is_session_visible: unit -> unit
To be called just before applying {!Register} to create plug-in services.
@since Neon-20140301 *)
-val is_config_visible: unit -> unit
-(** Make visible to the end-user the -<plug-in>-config option.
- To be called just before applying {!Register} to create plug-in services.
- @since Neon-20140301 *)
-
val plugin_subpath: string -> unit
(** Use the given string as the sub-directory in which the plugin files will
be installed (ie. [share/frama-c/plugin_subpath]...). Relevant for
@@ -178,9 +190,15 @@ val positive_debug_ref: int ref
val session_is_set_ref: (unit -> bool) ref
val session_ref: (unit -> Filepath.Normalized.t) ref
+val cache_is_set_ref: (unit -> bool) ref
+val cache_ref: (unit -> Filepath.Normalized.t) ref
+
val config_is_set_ref: (unit -> bool) ref
val config_ref: (unit -> Filepath.Normalized.t) ref
+val state_is_set_ref: (unit -> bool) ref
+val state_ref: (unit -> Filepath.Normalized.t) ref
+
(**/**)
(*
diff --git a/src/libraries/project/project.ml b/src/libraries/project/project.ml
index 6e61f48dda7702ec75f373bf6a28489a189e413c..ec66fdebc1096de932680f2b40704a1d81132a43 100644
--- a/src/libraries/project/project.ml
+++ b/src/libraries/project/project.ml
@@ -448,7 +448,7 @@ let magic = 9 (* magic number *)
let save_projects selection projects filename =
let cout = open_out_bin (filename : Filepath.Normalized.t :> string) in
- output_value cout Fc_config.version;
+ output_value cout System_config.Version.id;
output_value cout magic;
output_value cout !Graph.Blocks.cpt_vertex;
let states : (t * (string * State.state_on_disk) list) list =
@@ -613,7 +613,7 @@ let load_projects ~project_under_copy selection ?name filename =
raise (IOError s)
end
in
- check_magic cin (fun x -> x) Fc_config.version;
+ check_magic cin (fun x -> x) System_config.Version.id;
check_magic cin (fun n -> "magic number " ^ string_of_int n) magic;
let ocamlgraph_counter = read cin in
let pre_existing_projects = Descr.init project_under_copy in
diff --git a/src/libraries/utils/command.ml b/src/libraries/utils/command.ml
index 4052871a30ad329bab925e1c351042cf14c1ae2c..0e08f4f6f3101a5274c6f7f26cfdab42af34f8e3 100644
--- a/src/libraries/utils/command.ml
+++ b/src/libraries/utils/command.ml
@@ -238,7 +238,7 @@ let command_async ?stdout ?stderr cmd args =
command_generic ~async:true ?stdout ?stderr cmd args
let command ?(timeout=0) ?stdout ?stderr cmd args =
- if Fc_config.is_gui || timeout > 0 then
+ if System_config.is_gui || timeout > 0 then
let f = command_generic ~async:true ?stdout ?stderr cmd args in
let res = ref(Unix.WEXITED 99) in
let ftimeout = float_of_int timeout in
diff --git a/src/plugins/e-acsl/src/project_initializer/rtl.ml b/src/plugins/e-acsl/src/project_initializer/rtl.ml
index be5d5eb32d2a062c937c4ad3f6fbacb69418a82d..f0780382e5e2da28d3ace5b32ea24c179caeb828 100644
--- a/src/plugins/e-acsl/src/project_initializer/rtl.ml
+++ b/src/plugins/e-acsl/src/project_initializer/rtl.ml
@@ -23,7 +23,7 @@
open Cil_types
open Cil_datatype
-let rtl_file () = Options.Share.get_file ~mode:`Must_exist "e_acsl.h"
+let rtl_file () = Options.Share.get_file "e_acsl.h"
(* create the RTL AST in a fresh project *)
let create_rtl_ast prj =
diff --git a/src/plugins/eva/domains/cvalue/builtins.ml b/src/plugins/eva/domains/cvalue/builtins.ml
index 405b76bb14396767b3f61c00b506a431a1b32412..8cfee381861efc145d1e16ebd17f91d670211f49 100644
--- a/src/plugins/eva/domains/cvalue/builtins.ml
+++ b/src/plugins/eva/domains/cvalue/builtins.ml
@@ -151,7 +151,7 @@ let warn_builtin_override kf source bname =
let internal =
(* TODO: treat this 'internal' *)
let file = source.Filepath.pos_path in
- Filepath.is_relative ~base_name:Fc_config.datadir file
+ Filepath.is_relative ~base_name:System_config.Share.main file
in
if Kernel_function.is_definition kf && not internal
then
diff --git a/src/plugins/eva/utils/library_functions.ml b/src/plugins/eva/utils/library_functions.ml
index 98e63c0048c6b3d44cd9a27b05cb493f0a323194..e102542a0f6be3c1e8cdd0baa4d0878a91b01942 100644
--- a/src/plugins/eva/utils/library_functions.ml
+++ b/src/plugins/eva/utils/library_functions.ml
@@ -111,7 +111,7 @@ let warn_unsupported_spec name =
"@[The specification of function '%s' is currently not supported by Eva.@ \
Consider adding '%a'@ to the analyzed source files.@]"
name Filepath.Normalized.pretty
- (Filepath.Normalized.concat Fc_config.framac_libc header)
+ (Filepath.Normalized.concat System_config.Share.libc header)
with Not_found -> ()
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index 2196841e685c48c15c9ec87af00fd711069f4c63..33403999da9d1bd033efa5709bc5b7a94386b705 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -1846,8 +1846,8 @@ class main_window () : main_window_extension_points =
end
let make_splash () =
- GMain.Rc.add_default_file ((Fc_config.datadir:>string) ^"/frama-c.rc");
- GMain.Rc.add_default_file ((Fc_config.datadir:>string) ^"/frama-c-user.rc");
+ GMain.Rc.add_default_file ((System_config.Share.main:>string) ^"/frama-c.rc");
+ GMain.Rc.add_default_file ((System_config.Share.main:>string) ^"/frama-c-user.rc");
(*print_endline ("BOOT: " ^ (Glib.Main.setlocale `ALL None));*)
let (_:string) = GtkMain.Main.init ~setlocale:false () in
(*print_endline ("START: " ^ (Glib.Main.setlocale `ALL None));*)
diff --git a/src/plugins/gui/filetree.ml b/src/plugins/gui/filetree.ml
index ad6f63a75dff74eea5382461785a8619cd133c95..4543cc17c76c8d9a35c51daadae8e100ce8c1a0e 100644
--- a/src/plugins/gui/filetree.ml
+++ b/src/plugins/gui/filetree.ml
@@ -294,7 +294,7 @@ module MYTREE = struct
let comes_from_share filename =
let path = Filepath.Normalized.of_string filename in
- Filepath.is_relative ~base_name:Fc_config.datadir path
+ Filepath.is_relative ~base_name:System_config.Share.main path
let is_function t = match t with
| MFile _ -> false
diff --git a/src/plugins/gui/gtk_helper.ml b/src/plugins/gui/gtk_helper.ml
index 3bf2e03f8aef733f744e9f5c40337d28175ee448..5f754a5e98b29b3b7a3494f514e7d63eb5824703 100644
--- a/src/plugins/gui/gtk_helper.ml
+++ b/src/plugins/gui/gtk_helper.ml
@@ -24,7 +24,7 @@
let () =
begin
- Wutil.share := (Fc_config.datadir :> string);
+ Wutil.share := (System_config.Share.main :> string);
Wutil.flush := (fun msg -> Gui_parameters.warning "%s" msg);
end
@@ -32,7 +32,7 @@ let framac_logo, framac_icon =
try
let img ext =
Some (GdkPixbuf.from_file
- ((Fc_config.datadir:>string) ^ "/frama-c." ^ ext))
+ ((System_config.Share.main:>string) ^ "/frama-c." ^ ext))
in
img "png", img "ico"
with
@@ -48,7 +48,7 @@ let framac_logo, framac_icon =
module Configuration = struct
include Cilconfig
let configuration_file () =
- Gui_parameters.Config.get_file ~mode:`Create_path "frama-c-gui.config"
+ Gui_parameters.Config_dir.get_file ~create_path:true "frama-c-gui.config"
let load () = loadConfiguration (configuration_file ())
let save () = saveConfiguration (configuration_file ())
let reset () = Extlib.safe_remove (configuration_file () :> string);
diff --git a/src/plugins/gui/gui_parameters.ml b/src/plugins/gui/gui_parameters.ml
index 70882c2143ae26620c0dfb60a8e94b116ef114a1..c34495398aa0e4c4d3aed68f8fe7fca4e41df336 100644
--- a/src/plugins/gui/gui_parameters.ml
+++ b/src/plugins/gui/gui_parameters.ml
@@ -20,7 +20,6 @@
(* *)
(**************************************************************************)
-let () = Plugin.is_config_visible ()
include Plugin.Register
(struct
let name = "GUI"
@@ -28,6 +27,8 @@ include Plugin.Register
let help = "Graphical User Interface"
end)
+module Config_dir = Config_dir ()
+
let () = Parameter_customize.do_not_projectify ()
module Project_name =
Empty_string
diff --git a/src/plugins/gui/gui_parameters.mli b/src/plugins/gui/gui_parameters.mli
index ecc785aeda042a503c414c139ff8c92ec2d89e3a..e13bb21231ec8e4b02067c00efa9e3d573e57238 100644
--- a/src/plugins/gui/gui_parameters.mli
+++ b/src/plugins/gui/gui_parameters.mli
@@ -24,6 +24,8 @@
include Plugin.S
+module Config_dir : Parameter_sig.User_dir
+
module Project_name: Parameter_sig.String
(** Option -gui-project. *)
diff --git a/src/plugins/gui/help_manager.ml b/src/plugins/gui/help_manager.ml
index 8d8e9732f9608c203d1b12a0911028b19da2b25a..d5e9ba63a562c8a370e8128cfb8ccb994b5ad2d9 100644
--- a/src/plugins/gui/help_manager.ml
+++ b/src/plugins/gui/help_manager.ml
@@ -100,7 +100,7 @@ let show main_ui =
~license
~website:"http://frama-c.com"
~website_label:"Questions and support"
- ~version:Fc_config.version_and_codename
+ ~version:System_config.Version.id_and_codename
~comments:"Frama-C is a suite of tools dedicated to the analysis of the \
source code of software written in C."
()
diff --git a/src/plugins/markdown-report/sarif_gen.ml b/src/plugins/markdown-report/sarif_gen.ml
index 99b049c7bdd8685f3320218feea97c6ba13ae3af..f450316a9de079c805eaf7c2fa62f95387f4fba6 100644
--- a/src/plugins/markdown-report/sarif_gen.ml
+++ b/src/plugins/markdown-report/sarif_gen.ml
@@ -28,7 +28,7 @@ let frama_c_sarif () =
if Mdr_params.SarifDeterministic.get () then
"0+omitted-for-deterministic-output", ""
else
- Fc_config.version_and_codename, Fc_config.version
+ System_config.Version.id_and_codename, System_config.Version.id
in
let fullName = name ^ "-" ^ version in
let downloadUri = "https://frama-c.com/download.html" in
diff --git a/src/plugins/report/classify.ml b/src/plugins/report/classify.ml
index b4dc9b17d2e0b1782dd79cb0dd98380601f2fb72..98cf1b9b3514e00447f62d03052cdd8d4ced82ac 100644
--- a/src/plugins/report/classify.ml
+++ b/src/plugins/report/classify.ml
@@ -546,7 +546,7 @@ let classify () =
report_number "Unclassified: " !nb_unclassified R.OutputUnclassified.get ;
if !nb_errors > 0 && R.Exit.get () then
R.abort "Classified errors found" ;
- if not Fc_config.is_gui then clear_events () ;
+ if not System_config.is_gui then clear_events () ;
end
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/kernel_main.ml b/src/plugins/server/kernel_main.ml
index 1d178f7240cbd57164af6cdeaefdbff7b0194e2e..3e3f2b501e1f3322a0485bb283313adcac6e13f3 100644
--- a/src/plugins/server/kernel_main.ml
+++ b/src/plugins/server/kernel_main.ml
@@ -107,10 +107,10 @@ let () =
~descr:(Md.plain "Frama-C Kernel configuration")
signature
begin fun rq () ->
- set_version rq Fc_config.version ;
- set_datadir rq (Filepath.Normalized.to_string_list Fc_config.datadirs);
+ set_version rq System_config.Version.id ;
+ set_datadir rq (Filepath.Normalized.to_string_list System_config.Share.dirs);
set_pluginpath rq
- (Filepath.Normalized.to_string_list Fc_config.plugin_dir) ;
+ (Filepath.Normalized.to_string_list System_config.Plugins.dirs) ;
end
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/server_doc.ml b/src/plugins/server/server_doc.ml
index 7b65b2bc32f1a8600ceb304f2ee399f07559124f..7c6fb95f3f71948133b2c7b68db389e3c62c5b7e 100644
--- a/src/plugins/server/server_doc.ml
+++ b/src/plugins/server/server_doc.ml
@@ -370,7 +370,7 @@ let dump ~root ?(meta=true) () =
Yojson.Basic.to_file (path:>string) maindata ;
let body =
[ Md.H1 (Md.plain "Presentation", None);
- Md.Block (Md.text (Md.format "Version %s" Fc_config.version))]
+ Md.Block (Md.text (Md.format "Version %s" System_config.Version.id))]
@
table_of_contents ()
@
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 25d3218843795c5157b54a1685279812b6263ce3..8cd2d6366bb5baa79e2c7c6919e4fb2dc60d3ad9 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -58,7 +58,7 @@ let get_why3_conf = Conf.memoize
let main = Why3.Whyconf.get_main config in
let ld =
(WpContext.directory () :> string)::
- ((Wp_parameters.Share.get_dir ~mode:`Must_exist "why3") :> string)::
+ ((Wp_parameters.Share.get_dir "why3") :> string)::
(Why3.Whyconf.loadpath main) in
{ env = Why3.Env.create_env ld ; config = main }
end
diff --git a/src/plugins/wp/driver.mll b/src/plugins/wp/driver.mll
index a15af98a9889f7d51ded4e6b8579bec6f6afeaa7..cde182958a1d8429de7c3442f185eb13bd7ac82c 100644
--- a/src/plugins/wp/driver.mll
+++ b/src/plugins/wp/driver.mll
@@ -491,7 +491,7 @@ and bal = parse
let descr = String.concat "," drvs in
let includes =
let directories =
- [Wp_parameters.Share.get_dir ~mode:`Must_exist "."]
+ [Wp_parameters.Share.get_dir "."]
in
if Wp_parameters.has_dkey dkey then
Wp_parameters.debug ~dkey "Included directories:%t"
@@ -509,7 +509,7 @@ and bal = parse
then file
else LogicBuiltins.find_lib file)
drivers in
- let default = Wp_parameters.Share.get_file ~mode:`Must_exist "wp.driver" in
+ let default = Wp_parameters.Share.get_file "wp.driver" in
let feedback = Wp_parameters.Share.is_set () in
let ontty = if feedback then `Message else `Transient in
load_file ~ontty default;
diff --git a/src/plugins/wp/wpApi.ml b/src/plugins/wp/wpApi.ml
index 0fa7194ddba374087a2c72de1ce9f022ddb084b2..9c3a0f80149b2615ce73eae8987e742cefdcce2f 100644
--- a/src/plugins/wp/wpApi.ml
+++ b/src/plugins/wp/wpApi.ml
@@ -153,7 +153,7 @@ let get_name = function
| VCS.Why3 p -> Why3Provers.name p
let get_version = function
- | VCS.Qed | Tactical -> Fc_config.version_and_codename
+ | VCS.Qed | Tactical -> System_config.Version.id_and_codename
| Why3 p -> Why3Provers.version p
let iter_provers fn =
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 80bccc0d9a475ea48b8c1521bedcf802b8ba5941..a0334d13b33e70c17d25d9fb35223a6788ed728d 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -47,7 +47,7 @@ let has_dkey (k:category) = is_debug_key_enabled k
let server = ref false
let () = Server.Main.once (fun () -> server := true)
-let is_interactive () = Fc_config.is_gui || !server
+let is_interactive () = System_config.is_gui || !server
(* ------------------------------------------------------------------------ *)
(* --- WP Generation --- *)
diff --git a/tests/libc/check_compliance.ml b/tests/libc/check_compliance.ml
index e75f6dac805235d5831fcb4fc83bc33c6aa3cad9..c9ea93a9517933adeb43f9a0f816a9c0b3d2496a 100644
--- a/tests/libc/check_compliance.ml
+++ b/tests/libc/check_compliance.ml
@@ -130,7 +130,7 @@ let () =
let vis = new stdlib_visitor in
ignore (Visitor.visitFramacFile (vis :> Visitor.frama_c_visitor) (Ast.get ()));
let fc_stdlib_idents = vis#get_idents in
- let dir = Filename.concat (Fc_config.datadir:>string) "compliance" in
+ let dir = Filename.concat (System_config.Share.main:>string) "compliance" in
let c11_idents = Json.(to_table HeadersOnly (parse dir "c11_functions.json"))
and c11_headers = Json.(to_set (parse dir "c11_headers.json"))
and glibc_idents = Json.(to_set (parse dir "glibc_functions.json"))
diff --git a/tests/libc/check_parsing_individual_headers.ml b/tests/libc/check_parsing_individual_headers.ml
index 3f9c35918acef2fdf3f119c27689c2d6d7f5fd3d..21969ad8745198a0bd7e76a325806cafab756894 100644
--- a/tests/libc/check_parsing_individual_headers.ml
+++ b/tests/libc/check_parsing_individual_headers.ml
@@ -14,7 +14,7 @@ let blacklist libc_dir =
(* only goes down one level, which is enough for the libc *)
let collect_headers () =
- let libc_dir = Kernel.Share.get_dir ~mode:`Must_exist "libc" in
+ let libc_dir = Kernel.Share.get_dir "libc" in
let libc_dir_files = Array.to_list (Sys.readdir (libc_dir :> string)) in
let contents =
List.map (Filename.concat (libc_dir :> string)) libc_dir_files
diff --git a/tests/misc/dune b/tests/misc/dune
new file mode 100644
index 0000000000000000000000000000000000000000..93eae8d4100a7dca3874f32ae2879a7bee91c003
--- /dev/null
+++ b/tests/misc/dune
@@ -0,0 +1,4 @@
+(cram
+ (applies_to user_directories.unix.t)
+ (enabled_if (and (= %{os_type} unix) (<> %{system} macos)))
+)
diff --git a/tests/misc/oracle/my_visitor.1.res.oracle b/tests/misc/oracle/my_visitor.1.res.oracle
index cb5171adca05ef60341ce5813896eed563af564e..d7de4e33c03d33fa164d9ed0f242f9ad5ded2499 100644
--- a/tests/misc/oracle/my_visitor.1.res.oracle
+++ b/tests/misc/oracle/my_visitor.1.res.oracle
@@ -1,9 +1,9 @@
[kernel] Warning: emitter emitter1: correctness parameter -s does not exist anymore. Ignored.
[kernel] Warning: emitter emitter2: correctness parameter -s2 does not exist anymore. Ignored.
-[kernel] Warning: 15 states in saved file ignored. They are invalid in this Frama-C configuration.
+[kernel] Warning: 13 states in saved file ignored. They are invalid in this Frama-C configuration.
[kernel] Warning: emitter emitter1: correctness parameter -s does not exist anymore. Ignored.
[kernel] Warning: emitter emitter2: correctness parameter -s2 does not exist anymore. Ignored.
-[kernel] Warning: 15 states in saved file ignored. They are invalid in this Frama-C configuration.
+[kernel] Warning: 13 states in saved file ignored. They are invalid in this Frama-C configuration.
/* Generated by Frama-C */
int f(void)
{
diff --git a/tests/misc/oracle/orphan_emitter.res.oracle b/tests/misc/oracle/orphan_emitter.res.oracle
index b4a4e9e9636b1ef49df2c0fd7a6aaf94a196a565..54742d6322b5c706a0bf20f509252bf510f016ba 100644
--- a/tests/misc/oracle/orphan_emitter.res.oracle
+++ b/tests/misc/oracle/orphan_emitter.res.oracle
@@ -1,2 +1,2 @@
[kernel] Warning: emitter emitter1: correctness parameter -orphan does not exist anymore. Ignored.
-[kernel] Warning: 11 states in saved file ignored. They are invalid in this Frama-C configuration.
+[kernel] Warning: 9 states in saved file ignored. They are invalid in this Frama-C configuration.
diff --git a/tests/misc/share_directory.t/directories.ml b/tests/misc/share_directory.t/directories.ml
new file mode 100644
index 0000000000000000000000000000000000000000..63560876f2361104c6aae4693a9b8ac8cc0eb171
--- /dev/null
+++ b/tests/misc/share_directory.t/directories.ml
@@ -0,0 +1,51 @@
+let () = Plugin.is_share_visible ()
+module Self =
+ Plugin.Register
+ (struct
+ let name = "directories"
+ let shortname = "dirs"
+ let help = ""
+ end)
+
+module Share = Self.Share
+
+module Path =
+ Self.Make_site_dir
+ (Share)
+ (struct let name = "path" end)
+
+let never_fail_get f x =
+ try
+ let s = f x in
+ Self.feedback "Found: %a" Filepath.Normalized.pretty s
+ with _ -> ()
+
+let run_all () =
+ Kernel.feedback "IS_SET %b" (Share.is_set ()) ;
+
+ Self.feedback "path (dir)" ;
+ never_fail_get Share.get_dir "path" ;
+
+ Self.feedback "Path (.)" ;
+ never_fail_get Path.get_dir "." ;
+
+ Self.feedback "path/file.txt (file)" ;
+ never_fail_get Share.get_file "path/file.txt" ;
+
+ Self.feedback "Path (file)" ;
+ never_fail_get Path.get_file "file.txt" ;
+
+ Self.feedback "foo (dir)" ;
+ never_fail_get Share.get_dir "foo" ;
+
+ Self.feedback "foo.txt (file)" ;
+ never_fail_get Share.get_file "foo.txt" ;
+
+ Self.feedback "path (file)" ;
+ never_fail_get Share.get_file "path" ;
+
+ Self.feedback "path/file.txt" ;
+ never_fail_get Share.get_dir "path/file.txt"
+
+
+let () = Boot.Main.extend run_all
diff --git a/tests/misc/share_directory.t/dune b/tests/misc/share_directory.t/dune
new file mode 100644
index 0000000000000000000000000000000000000000..ac507d4db539126a39a363ee88817bcc25a24083
--- /dev/null
+++ b/tests/misc/share_directory.t/dune
@@ -0,0 +1,18 @@
+(library
+ (name directories)
+ (public_name frama-c-directories.core)
+ (flags -open Frama_c_kernel :standard)
+ (libraries frama-c.kernel))
+
+(plugin
+ (optional)
+ (name directories)
+ (libraries frama-c-directories.core)
+ (site
+ (frama-c plugins)))
+
+(install
+ (package frama-c-directories)
+ (section (site (frama-c share)))
+ (files (share/path/file.txt as dirs/path/file.txt))
+)
diff --git a/tests/misc/share_directory.t/dune-project b/tests/misc/share_directory.t/dune-project
new file mode 100644
index 0000000000000000000000000000000000000000..e7f717f9d792787281dc6871500a2f4c7162ab5c
--- /dev/null
+++ b/tests/misc/share_directory.t/dune-project
@@ -0,0 +1,4 @@
+(lang dune 3.7)
+(using dune_site 0.1)
+(name frama-c-directories)
+(package (name frama-c-directories))
diff --git a/tests/misc/share_directory.t/run.t b/tests/misc/share_directory.t/run.t
new file mode 100644
index 0000000000000000000000000000000000000000..c95421570d344b6252a44ef5869b0e01f481ac3d
--- /dev/null
+++ b/tests/misc/share_directory.t/run.t
@@ -0,0 +1,42 @@
+ $ dune build --root . @install
+
+Basic case
+ $ dune exec -- frama-c
+ [kernel] IS_SET false
+ [dirs] path (dir)
+ [dirs] Found: _build/install/default/share/frama-c/share/dirs/path
+ [dirs] Path (.)
+ [dirs] Found: _build/install/default/share/frama-c/share/dirs/path
+ [dirs] path/file.txt (file)
+ [dirs] Found: _build/install/default/share/frama-c/share/dirs/path/file.txt
+ [dirs] Path (file)
+ [dirs] Found: _build/install/default/share/frama-c/share/dirs/path/file.txt
+ [dirs] foo (dir)
+ [dirs] User Error: Could not find directory foo in Frama-C/directories share
+ [dirs] foo.txt (file)
+ [dirs] User Error: Could not find file foo.txt in Frama-C/directories share
+ [dirs] path (file)
+ [dirs] User Error: _build/install/default/share/frama-c/share/dirs/path is expected to be a file
+ [dirs] path/file.txt
+ [dirs] User Error: _build/install/default/share/frama-c/share/dirs/path/file.txt is expected to be a directory
+
+With option
+ $ cp -r share copied
+ $ dune exec -- frama-c -dirs-share copied
+ [kernel] IS_SET true
+ [dirs] path (dir)
+ [dirs] Found: copied/path
+ [dirs] Path (.)
+ [dirs] Found: copied/path
+ [dirs] path/file.txt (file)
+ [dirs] Found: copied/path/file.txt
+ [dirs] Path (file)
+ [dirs] Found: copied/path/file.txt
+ [dirs] foo (dir)
+ [dirs] User Error: Could not find directory foo in Frama-C/directories share
+ [dirs] foo.txt (file)
+ [dirs] User Error: Could not find file foo.txt in Frama-C/directories share
+ [dirs] path (file)
+ [dirs] User Error: copied/path is expected to be a file
+ [dirs] path/file.txt
+ [dirs] User Error: copied/path/file.txt is expected to be a directory
diff --git a/tests/misc/share_directory.t/share/path/file.txt b/tests/misc/share_directory.t/share/path/file.txt
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/misc/user_directories.unix.t/directories.ml b/tests/misc/user_directories.unix.t/directories.ml
new file mode 100644
index 0000000000000000000000000000000000000000..e9b949fdf8d073e52ed3f077b47b149cbcf18668
--- /dev/null
+++ b/tests/misc/user_directories.unix.t/directories.ml
@@ -0,0 +1,93 @@
+let () = Plugin.is_session_visible ()
+module Self =
+ Plugin.Register
+ (struct
+ let name = "directories"
+ let shortname = "dirs"
+ let help = ""
+ end)
+
+module OnlyCache = Self.False(struct
+ let option_name = "-dirs-cache-only"
+ let help = ""
+ end)
+
+module Cache = Self.Cache_dir ()
+module Sub_cache_no_opt =
+ Self.Make_user_dir
+ (Cache)
+ (struct let name = "noopt" end)
+
+module Sub_cache_opt_no_var =
+ Self.Make_user_dir_opt
+ (Cache)
+ (struct
+ let option_name = "-dirs-opt-no-var"
+ let arg_name = "dir"
+ let help = ""
+ let env = None
+ let dirname = "optnovar"
+ end)
+
+module Sub_cache_opt_var =
+ Self.Make_user_dir_opt
+ (Cache)
+ (struct
+ let option_name = "-dirs-optvar"
+ let arg_name = "dir"
+ let help = ""
+ let env = Some "FRAMAC_DIRS_VAR"
+ let dirname = "optvar"
+ end)
+
+module Config = Self.Config_dir ()
+module State = Self.State_dir ()
+module Session = Self.Session
+
+let never_fail_get f x =
+ try
+ let s = f x in
+ Self.feedback "Found: %a" Filepath.Normalized.pretty s
+ with _ -> ()
+
+let run_all () =
+ if OnlyCache.get ()
+ then begin
+ ignore @@ Cache.get_dir ~create_path:true "created" ;
+ ignore @@ Sub_cache_no_opt.get_dir ~create_path:true "." ;
+ ignore @@ Sub_cache_no_opt.get_dir "foo" ;
+ ignore @@ Sub_cache_opt_no_var.get_dir ~create_path:true "." ;
+ ignore @@ Sub_cache_opt_no_var.get_dir "foo" ;
+ ignore @@ Sub_cache_opt_var.get_dir ~create_path:true "." ;
+ ignore @@ Sub_cache_opt_var.get_dir "foo" ;
+
+ ignore @@ Sub_cache_no_opt.get_file "file" ;
+ ignore @@ Sub_cache_opt_var.get_file "file" ;
+
+ never_fail_get Cache.get_file "created" ;
+ never_fail_get Sub_cache_opt_var.get_file "."
+ end
+ else
+ try
+ ignore @@ Cache.get_dir ~create_path:true "created" ;
+ ignore @@ Config.get_dir ~create_path:true "created" ;
+ ignore @@ State.get_dir ~create_path:true "created" ;
+ ignore @@ Session.get_dir ~create_path:true "created" ;
+ ignore @@ Session.get_file ~create_path:true "created_filepath/file" ;
+
+ let cache_dir = Cache.get_dir "not_created" in
+ let config_dir = Config.get_dir "not_created" in
+ let state_dir = State.get_dir "not_created" in
+ let session_dir = Session.get_dir "not_created" in
+ let session_file = Session.get_file "not_created_filepath/file" in
+
+ Self.feedback "Not created:" ;
+ Self.feedback "%a" Filepath.Normalized.pretty cache_dir ;
+ Self.feedback "%a" Filepath.Normalized.pretty config_dir ;
+ Self.feedback "%a" Filepath.Normalized.pretty state_dir ;
+ Self.feedback "%a" Filepath.Normalized.pretty session_dir ;
+ Self.feedback "%a" Filepath.Normalized.pretty session_file
+ with Not_found ->
+ Self.error "Failure when creating directories"
+
+let () = Boot.Main.extend run_all
diff --git a/tests/misc/user_directories.unix.t/dune b/tests/misc/user_directories.unix.t/dune
new file mode 100644
index 0000000000000000000000000000000000000000..1f56f8e1118d52a2bae86d9f5a3d4f74171d9883
--- /dev/null
+++ b/tests/misc/user_directories.unix.t/dune
@@ -0,0 +1,12 @@
+(library
+ (name directories)
+ (public_name frama-c-directories.core)
+ (flags -open Frama_c_kernel :standard)
+ (libraries frama-c.kernel))
+
+(plugin
+ (optional)
+ (name directories)
+ (libraries frama-c-directories.core)
+ (site
+ (frama-c plugins)))
diff --git a/tests/misc/user_directories.unix.t/dune-project b/tests/misc/user_directories.unix.t/dune-project
new file mode 100644
index 0000000000000000000000000000000000000000..e7f717f9d792787281dc6871500a2f4c7162ab5c
--- /dev/null
+++ b/tests/misc/user_directories.unix.t/dune-project
@@ -0,0 +1,4 @@
+(lang dune 3.7)
+(using dune_site 0.1)
+(name frama-c-directories)
+(package (name frama-c-directories))
diff --git a/tests/misc/user_directories.unix.t/run.t b/tests/misc/user_directories.unix.t/run.t
new file mode 100644
index 0000000000000000000000000000000000000000..45724acbd7316d421032175ebb0564d338642465
--- /dev/null
+++ b/tests/misc/user_directories.unix.t/run.t
@@ -0,0 +1,207 @@
+In all these tests please set HOME before executing commands so that it does not
+touch the actual user HOME.
+
+ $ dune build --root . @install
+
+Basic case
+ $ HOME=home dune exec -- frama-c
+ [dirs] Not created:
+ [dirs] home/.cache/frama-c/dirs/not_created
+ [dirs] home/.config/frama-c/dirs/not_created
+ [dirs] home/.local/state/frama-c/dirs/not_created
+ [dirs] .frama-c/dirs/not_created
+ [dirs] .frama-c/dirs/not_created_filepath/file
+ $ find home | sort
+ home
+ home/.cache
+ home/.cache/frama-c
+ home/.cache/frama-c/dirs
+ home/.cache/frama-c/dirs/created
+ home/.config
+ home/.config/frama-c
+ home/.config/frama-c/dirs
+ home/.config/frama-c/dirs/created
+ home/.local
+ home/.local/state
+ home/.local/state/frama-c
+ home/.local/state/frama-c/dirs
+ home/.local/state/frama-c/dirs/created
+ $ rm -rf home
+
+Customized via variables: XDG level
+ $ HOME=home XDG_CACHE_HOME=cache XDG_CONFIG_HOME=config XDG_STATE_HOME=state dune exec -- frama-c
+ [dirs] Not created:
+ [dirs] cache/frama-c/dirs/not_created
+ [dirs] config/frama-c/dirs/not_created
+ [dirs] state/frama-c/dirs/not_created
+ [dirs] .frama-c/dirs/not_created
+ [dirs] .frama-c/dirs/not_created_filepath/file
+ $ find home | sort
+ find: 'home': No such file or directory
+ $ find cache | sort
+ cache
+ cache/frama-c
+ cache/frama-c/dirs
+ cache/frama-c/dirs/created
+ $ find config | sort
+ config
+ config/frama-c
+ config/frama-c/dirs
+ config/frama-c/dirs/created
+ $ find state | sort
+ state
+ state/frama-c
+ state/frama-c/dirs
+ state/frama-c/dirs/created
+ $ rm -rf home cache config state
+
+Customized via variables: Kernel level
+ $ HOME=home FRAMAC_CACHE=cache FRAMAC_CONFIG=config FRAMAC_STATE=state FRAMAC_SESSION=session dune exec -- frama-c
+ [dirs] Not created:
+ [dirs] cache/dirs/not_created
+ [dirs] config/dirs/not_created
+ [dirs] state/dirs/not_created
+ [dirs] session/dirs/not_created
+ [dirs] session/dirs/not_created_filepath/file
+ $ find home | sort
+ find: 'home': No such file or directory
+ $ find cache | sort
+ cache
+ cache/dirs
+ cache/dirs/created
+ $ find config | sort
+ config
+ config/dirs
+ config/dirs/created
+ $ find state | sort
+ state
+ state/dirs
+ state/dirs/created
+ $ rm -rf home cache config state
+
+Customized via variables: Plugin level
+ $ HOME=home FRAMAC_DIRS_CACHE=cache FRAMAC_DIRS_CONFIG=config FRAMAC_DIRS_STATE=state FRAMAC_DIRS_SESSION=session dune exec -- frama-c
+ [dirs] Not created:
+ [dirs] cache/not_created
+ [dirs] config/not_created
+ [dirs] state/not_created
+ [dirs] session/not_created
+ [dirs] session/not_created_filepath/file
+ $ find home | sort
+ find: 'home': No such file or directory
+ $ find cache | sort
+ cache
+ cache/created
+ $ find config | sort
+ config
+ config/created
+ $ find state | sort
+ state
+ state/created
+ $ rm -rf home cache config state
+
+Customized via options kernel level
+ $ HOME=home dune exec -- frama-c -cache cache -config config -state state -session session
+ [dirs] Not created:
+ [dirs] cache/dirs/not_created
+ [dirs] config/dirs/not_created
+ [dirs] state/dirs/not_created
+ [dirs] session/dirs/not_created
+ [dirs] session/dirs/not_created_filepath/file
+ $ find home | sort
+ find: 'home': No such file or directory
+ $ find cache | sort
+ cache
+ cache/dirs
+ cache/dirs/created
+ $ find config | sort
+ config
+ config/dirs
+ config/dirs/created
+ $ find state | sort
+ state
+ state/dirs
+ state/dirs/created
+ $ rm -rf home cache config state
+
+Customized via options plug-in level
+ $ HOME=home dune exec -- frama-c -dirs-cache cache -dirs-config config -dirs-state state -dirs-session session
+ [dirs] Not created:
+ [dirs] cache/not_created
+ [dirs] config/not_created
+ [dirs] state/not_created
+ [dirs] session/not_created
+ [dirs] session/not_created_filepath/file
+ $ find home | sort
+ find: 'home': No such file or directory
+ $ find cache | sort
+ cache
+ cache/created
+ $ find config | sort
+ config
+ config/created
+ $ find state | sort
+ state
+ state/created
+ $ rm -rf home cache config state
+
+Customized plug-in subdir option > plug-in subdir variable
+ $ HOME=home FRAMAC_DIRS_VAR=subdir_bad dune exec -- frama-c -dirs-cache-only -dirs-optvar subdir
+ [dirs] User Error: home/.cache/frama-c/dirs/created is expected to be a file
+ [dirs] User Error: subdir is expected to be a file
+ $ rm -rf home cache subdir
+
+Customized plug-in subdir variable > plug-in option
+ $ HOME=home FRAMAC_DIRS_VAR=subdir dune exec -- frama-c -dirs-cache-only -dirs-cache cache
+ [dirs] User Error: cache/created is expected to be a file
+ [dirs] User Error: subdir is expected to be a file
+ $ rm -rf home cache subdir
+
+Customized plug-in option > plug-in var
+ $ HOME=home FRAMAC_DIRS_CACHE=cache_bad dune exec -- frama-c -dirs-cache-only -dirs-cache cache
+ [dirs] User Error: cache/created is expected to be a file
+ [dirs] User Error: cache/optvar is expected to be a file
+ $ rm -rf home cache
+
+Customized plug-in var > kernel option
+ $ HOME=home FRAMAC_DIRS_CACHE=cache dune exec -- frama-c -dirs-cache-only -cache cache_bad
+ [dirs] User Error: cache/created is expected to be a file
+ [dirs] User Error: cache/optvar is expected to be a file
+ $ rm -rf home cache
+
+Customized kernel option > kernel var
+ $ HOME=home FRAMAC_CACHE=cache_bad dune exec -- frama-c -dirs-cache-only -cache cache
+ [dirs] User Error: cache/dirs/created is expected to be a file
+ [dirs] User Error: cache/dirs/optvar is expected to be a file
+ $ rm -rf home cache
+
+Customized kernel var > xdg var
+ $ HOME=home XDG_CACHE_HOME=cache_bad FRAMAC_CACHE=cache dune exec -- frama-c -dirs-cache-only
+ [dirs] User Error: cache/dirs/created is expected to be a file
+ [dirs] User Error: cache/dirs/optvar is expected to be a file
+ $ rm -rf home cache
+
+Bad home value
+ $ HOME= dune exec -- frama-c
+ [dirs] User Error: Failure when creating directories
+ [dirs] User Error: Deferred error message was emitted during execution. See above messages for more information.
+ [kernel] Plug-in dirs aborted: invalid user input.
+ [1]
+
+Bad home permission
+ $ mkdir home
+ $ chmod -w home
+ $ HOME=home dune exec -- frama-c
+ [dirs] User Error: cannot create cache directory `home/.cache/frama-c/dirs/created'
+ [kernel] Plug-in dirs aborted: invalid user input.
+ [1]
+ $ rm -rf home
+
+File already exists were a directory is expected
+ $ mkdir cache
+ $ touch cache/created
+ $ HOME=home dune exec -- frama-c -dirs-cache cache
+ [dirs] User Error: cache/created is expected to be a directory
+ [kernel] Plug-in dirs aborted: invalid user input.
+ [1]
+ $ rm -rf cache
diff --git a/tests/misc/version.ml b/tests/misc/version.ml
index cddd787c76c38aff5d5b9bb450744645c79045fd..cd75e4c34db5f49d5ca5137ef8bb5c60b95f7311 100644
--- a/tests/misc/version.ml
+++ b/tests/misc/version.ml
@@ -1,20 +1,20 @@
let re_version = Str.regexp "^\\([0-9]+\\)\\.\\([0-9]+\\)"
let run () =
- let version_str = Fc_config.version in
+ let version_str = System_config.Version.id in
if Str.string_match re_version version_str 0 then
let major = Str.matched_group 1 version_str in
let minor = Str.matched_group 2 version_str in
- if major = string_of_int Fc_config.major_version &&
- minor = string_of_int Fc_config.minor_version
+ if major = string_of_int System_config.Version.major &&
+ minor = string_of_int System_config.Version.minor
then
Kernel.feedback "version numbers match"
else
Kernel.abort
"error parsing major/minor version: expected %s.%s, got %d.%d"
- major minor Fc_config.major_version Fc_config.minor_version
+ major minor System_config.Version.major System_config.Version.minor
else
Kernel.abort
- "could not parse Fc_config.version"
+ "could not parse System_config.Version.id"
let () = Boot.Main.extend run
diff --git a/tests/saveload/oracle/basic.4.res.oracle b/tests/saveload/oracle/basic.4.res.oracle
index 7452402948f0fad8d57c67cc0b5465f130d5c22a..eeed93b93d1467d26a2d89b1bca0736fb1c0c510 100644
--- a/tests/saveload/oracle/basic.4.res.oracle
+++ b/tests/saveload/oracle/basic.4.res.oracle
@@ -1 +1 @@
-[kernel] Warning: 11 states in saved file ignored. They are invalid in this Frama-C configuration.
+[kernel] Warning: 9 states in saved file ignored. They are invalid in this Frama-C configuration.