diff --git a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 index dd9c939836267b6087c54c2d652ae48e32f368c8..9b1c8283fdcd51ef1667a73ad34f5971beecca38 100644 --- a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 +++ b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 @@ -99,6 +99,9 @@ use the \fBFrama-C\fP standard library instead of a system-wide one. .B -M, --full-mmodel maximize memory-related instrumentation. .TP +.B --temporal +enable checking for temporal memory errors in \\\fBvalid\fP and \\\fBvalid_read\fP predicates. +.TP .B --weak-validity enable notion of weak validity. By default expression \fB(p+i)\fP, where \fBp\fP is a pointer and \fBi\fP is an integer offset is deemed valid if both addresses