From 27948deaa6115f5b5a266f278cf7117c136e7bc9 Mon Sep 17 00:00:00 2001 From: Florian Deljarry Date: Tue, 14 Jul 2020 14:27:32 -0400 Subject: [PATCH] man/nitc: Update man page Update man page to add `--in-out-invariant` option Signed-off-by: Florian Deljarry --- share/man/nitc.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/share/man/nitc.md b/share/man/nitc.md index 64d8c530d0..75f349ae71 100644 --- a/share/man/nitc.md +++ b/share/man/nitc.md @@ -548,6 +548,9 @@ Option used to disable the contracts(ensures, expects) usage. ### `--full-contract` Option used to enables contracts (ensures, expects) on all classes. Warning this is an expensive option at runtime. +### `--in-out-invariant` +Option used to enable `invariant` verification on entry and exit of a method. By default, invariants are only checked on exit. Note, that the contracts are not checked on a `self` call. + # ENVIRONMENT VARIABLES ### `NIT_DIR`