diff --git a/man/frama-c.1 b/man/frama-c.1 index 27e9941f2597e2be1899c63954d2307bf2e10d68..5fe5295b91b14ef7d0e96ae47b15b006f2980c62 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 dfcc64130a0a5f126644e5818c73a4dc67551348..0715eff62118a7e6ef21cb4dfc67bb741aaeff44 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