From 0b94b439e0ec0aa03cbfa1ee4a5bfd16ee46ae33 Mon Sep 17 00:00:00 2001
From: Farah <farah.benmouhoub@cea.fr>
Date: Thu, 26 Sep 2024 15:50:30 +0200
Subject: [PATCH] [man] add help message for generated specs

---
 man/frama-c.1    | 12 ++++++++++++
 man/frama-c.1.md | 10 ++++++++++
 2 files changed, 22 insertions(+)

diff --git a/man/frama-c.1 b/man/frama-c.1
index 27e9941f25..5fe5295b91 100644
--- a/man/frama-c.1
+++ b/man/frama-c.1
@@ -160,6 +160,18 @@ lvalue it is assigned to.
 Otherwise, a temporary variable is used and the cast is made explicit.
 Defaults to yes.
 .TP
+\-generated\-spec\-mode \f[I]mode\f[R]
+selects which \f[I]mode\f[R] will be used to generate missing
+specifications.
+Can be one of: \f[I]frama\-c\f[R], \f[I]acsl\f[R], \f[I]safe\f[R], or
+the name of a custom registered in plug\-in.
+.TP
+\-generated\-spec\-custom \f[I]c_1:m_1,\&...,c_n:m_n\f[R]
+fine\-tunes missing specification generation by manually selecting modes
+for each clause.
+Can be one of: \f[I]frama\-c\f[R], \f[I]acsl\f[R], \f[I]safe\f[R],
+\f[I]skip\f[R], or the name of a custom registered mode.
+.TP
 \-config \f[I]dir\f[R]
 overrides default Frama\-C configuration directory
 .TP
diff --git a/man/frama-c.1.md b/man/frama-c.1.md
index dfcc64130a..0715eff621 100644
--- a/man/frama-c.1.md
+++ b/man/frama-c.1.md
@@ -149,6 +149,16 @@ syntax. Defaults to yes.
 it is assigned to. Otherwise, a temporary variable is used and the cast is made
 explicit. Defaults to yes.
 
+-generated-spec-mode *mode*
+: selects which *mode* will be used to generate missing specifications.
+Can be one of: *frama-c*, *acsl*, *safe*, or the name of a custom
+registered in plug-in.
+
+-generated-spec-custom *c_1:m_1,...,c_n:m_n*
+: fine-tunes missing specification generation by manually selecting
+modes for each clause. Can be one of: *frama-c*, *acsl*, *safe*, *skip*, or
+the name of a custom registered mode.
+
 -config *dir*
 : overrides default Frama-C configuration directory
 
-- 
GitLab