Documentation update

Author: Remi Delmas

doc/cprover-manual/properties.md

@@ -134,40 +134,64 @@ As all of these checks apply across the entire input program, we may wish to
 disable them for selected statements in the program. For example, unsigned
 overflows can be expected and acceptable in certain instructions even when
 elsewhere we do not expect them. As of version 5.12, CBMC supports selectively
-disabling or enabling automatically generated properties. 
+disabling or enabling automatically generated properties using pragmas. 
 
-To disable property generation,
-use `#pragma CPROVER check disable "<name_of_check>"`, which remains in effect
-until a `#pragma CPROVER check pop` (to re-enable all properties
-disabled or enabled before or since the last `#pragma CPROVER check push`) is provided. 
+
+CPROVER pragmas are handled using a stack:
+- `#pragma CPROVER check push` pushes a new level on the pragma stack
+- `#pragma CPROVER check disable "<name_of_check>"` adds a disable pragma at the top of the stack
+- `#pragma CPROVER check enable "<name_of_check>"` adds a enable pragma at the top of the stack
+- an `enable` or `disable` pragma for a given check present at the top level of the stack shadows other pragmas for the same in lower levels of the stack
+- adding both `enable` and `disable` pragmas for a same check in a same level of the stack creates a warning, the most recent pragma takes precedence
+- `#pragma CPROVER check pop` pops a level in the stack and restores the state of pragmas at the sub level  
 
 For example, for unsigned overflow checks, use
+
 ```
 unsigned foo(unsigned x)
 {
 #pragma CPROVER check push
-#pragma CPROVER check disable "unsigned-overflow"
-  x = x + 1; // immediately follows the pragma, no unsigned overflow check here
+#pragma CPROVER check enable "unsigned-overflow"
+  x = x + 1; // immediately follows the pragma, unsigned overflow check apply here
 #pragma CPROVER check pop
-  x = x + 2; // unsigned overflow checks are generated here
+  x = x + 2; // unsigned overflow checks do not apply here
 ```
 
-To enable property generation,
-use `#pragma CPROVER check enable "<name_of_check>"`, which remains in effect
-until a `#pragma CPROVER check pop` (to re-enable all properties
-disabled or enabled before or since the last `#pragma CPROVER check push`) is provided.
+```
+unsigned foo(unsigned x)
+{
+#pragma CPROVER check push
+#pragma CPROVER check enable "unsigned-overflow"
+#pragma CPROVER check enable "signed-overflow"
+  x = x + 1; // unsigned and signed overflow check apply here
+#pragma CPROVER check push
+#pragma CPROVER check disable "unsigned-overflow"
+  x = x + 2; // only signed overflow check apply here
+#pragma CPROVER check pop
+  x = x + 3; // unsigned and signed overflow check apply here
+#pragma CPROVER check pop
+  x = x + 2; // unsigned overflow checks do not apply here
+```
 
-For example, for unsigned overflow checks, use
 ```
 unsigned foo(unsigned x)
 {
 #pragma CPROVER check push
 #pragma CPROVER check enable "unsigned-overflow"
-  x = x + 1; // immediately follows the pragma, unsigned overflow check are generated here
+#pragma CPROVER check enable "signed-overflow"
+  x = x + 1; // unsigned and signed overflow check apply here
+#pragma CPROVER check push
+#pragma CPROVER check disable "unsigned-overflow"
+#pragma CPROVER check enable "unsigned-overflow" 
+  // warning: both enable and disable for unsigned-overflow (last one takes precedence)
+  x = x + 2; // unsigned and signed overflow check apply here
 #pragma CPROVER check pop
-  x = x + 2; // unsigned overflow checks are not generated here
+  x = x + 3; // unsigned and signed overflow check apply here
+#pragma CPROVER check pop
+  x = x + 2; // unsigned overflow checks do not apply here
 ```
 
+
 #### Flag --nan-check limitations
 
 Please note that `--nan-check` flag is adding not-a-number checks only for