From 50d2e5f09bae684dab750a80fff70632a2b70edd Mon Sep 17 00:00:00 2001 From: Thibault Martin <thi.martin.pro@pm.me> Date: Thu, 4 Jul 2024 10:42:53 +0200 Subject: [PATCH] [doc] Update man --- man/frama-c.1 | 43 ++++++++++++++++++------------------------- 1 file changed, 18 insertions(+), 25 deletions(-) diff --git a/man/frama-c.1 b/man/frama-c.1 index d73aecf02e4..af751133d76 100644 --- a/man/frama-c.1 +++ b/man/frama-c.1 @@ -1,7 +1,6 @@ -.\" Automatically generated by Pandoc 2.14.0.3 +.\" Automatically generated by Pandoc 3.1.8 .\" .TH "FRAMA-C" "1" "" "2024-04-24" "" -.hy .\"------------------------------------------------------------------------ .\" .\" This file is part of Frama-C documentation @@ -18,15 +17,12 @@ .\" 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 -.PP frama-c - a static analyzer for C programs .PP frama-c-gui - the graphical interface of frama-c .SH SYNOPSIS -.PP \f[B]frama-c\f[R] [ \f[I]options\f[R] ] \f[I]files\f[R] .SH DESCRIPTION -.PP \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 @@ -57,7 +53,6 @@ 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 -.PP Options taking an additional parameter can also be written under the form .RS @@ -179,8 +174,8 @@ version of this option) when a typechecking error occurs is to reject the source file as is the case for typechecking errors within the C code. With this option on, the typechecker will only output a warning and -discard the annotation but type\[hy]checking will continue (errors in C -code are still fatal, though). +discard the annotation but typeâ€checking will continue (errors in C code +are still fatal, though). .PD 0 .P .PD @@ -209,8 +204,7 @@ Note that this option is often better replaced by .TP -cpp-extra-args \f[I]args\f[R] gives additional arguments to the preprocessor. -Preprocessing annotations is done in two separate preprocessing -stages. +Preprocessing annotations is done in two separate preprocessing stages. The first one is a normal pass on the C code which retains macro definitions. These are then used in the second pass during which annotations are @@ -308,8 +302,14 @@ Defaults to no. when \f[B]-simplify-cfg\f[R] is set, keeps switch statements. Defaults to no. .TP --keep-unused-specified-functions -see \f[B]-remove-unused-specified-functions\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], +\f[B]all\f[R], and \f[B]all_debug\f[R]; \f[B]specified\f[R] (the default +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]. @@ -456,12 +456,6 @@ inlined. 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-specified-functions -keeps function prototypes that have an ACSL specification but are not -used in the code. -This is the default. -Functions having the attribute \f[B]FRAMAC_BUILTIN\f[R] are always kept. -.TP -remove-unused-types remove types and struct/union/enum declarations that are not referenced anywhere else in the code. @@ -491,7 +485,8 @@ statements before analyses. Defaults to no. .TP [-no]-simplify-trivial-loops -simplifies trivial loops such as \f[B]do \&... while (0)\f[R] loops. +simplifies trivial loops such as \f[B]do \&... +while (0)\f[R] loops. Defaults to yes. .TP -then @@ -526,12 +521,13 @@ 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 pragma -unroll \f[R] directive. +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 -ignores \f[B]UNROLL\f[R] loop pragmas disabling unrolling. +ignores \f[B]loop unfold \[lq]done\[rq]\f[R] disabling syntactic loop +unrolling. .PP [-no]-unicode outputs ACSL formulas with UTF-8 characters. This is the default. @@ -601,7 +597,6 @@ Defaults to no. generates alarms for reads of trap representations of _Bool lvalues. Defaults to yes. .SS Plugin-specific options -.PP For each plugin, the command .RS .PP @@ -633,7 +628,6 @@ 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). .SH ENVIRONMENT VARIABLES -.PP It is possible to control the places where Frama-C looks for its files through the following variables. .TP @@ -644,7 +638,6 @@ FRAMAC_SHARE The directory where Frama-C data (e.g.\ its version of the standard library) is installed. .SH SEE ALSO -.PP Frama-C user manual: https://frama-c.com/download/frama-c-user-manual.pdf .PP -- GitLab