formatting

Author: Remi Delmas

doc/cprover-manual/properties.md

@@ -134,16 +134,21 @@ 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 using pragmas. 
+disabling or enabling automatically generated properties using pragmas.
 
 
 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 PARSING_ERROR.
-- `#pragma CPROVER check pop` pops a level in the stack and restores the state of pragmas at the sub level  
+- `#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 PARSING_ERROR.
+- `#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
 
@@ -152,9 +157,11 @@ unsigned foo(unsigned x)
 {
 #pragma CPROVER check push
 #pragma CPROVER check enable "unsigned-overflow"
-  x = x + 1; // immediately follows the pragma, unsigned overflow check apply here
+  // unsigned overflow check apply here
+  x = x + 1;
 #pragma CPROVER check pop
-  x = x + 2; // unsigned overflow checks do not apply here
+  // unsigned overflow checks do not apply here
+  x = x + 2;
 ```
 
 ```
@@ -163,14 +170,18 @@ 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
+  // unsigned and signed overflow check apply here
+  x = x + 1;
 #pragma CPROVER check push
 #pragma CPROVER check disable "unsigned-overflow"
-  x = x + 2; // only signed overflow check apply here
+  // only signed overflow check apply here
+  x = x + 2;
 #pragma CPROVER check pop
-  x = x + 3; // unsigned and signed overflow check apply here
+  // unsigned and signed overflow check apply here
+  x = x + 3;
 #pragma CPROVER check pop
-  x = x + 2; // unsigned overflow checks do not apply here
+  // unsigned overflow checks do not apply here
+  x = x + 2;
 ```
 
 ```
@@ -179,19 +190,19 @@ 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
+  // unsigned and signed overflow check apply here
+  x = x + 1;
 #pragma CPROVER check push
 #pragma CPROVER check disable "unsigned-overflow"
-#pragma CPROVER check enable "unsigned-overflow" 
-  // PARSING_ERROR ... Found enable and disable pragmas for unsigned-overflow-check
+#pragma CPROVER check enable "unsigned-overflow"
+  // PARSING_ERROR Found enable and disable pragmas for unsigned-overflow-check
   x = x + 2;
 #pragma CPROVER check pop
   x = x + 3;
 #pragma CPROVER check pop
   x = x + 2;
 ```
 
-
 #### Flag --nan-check limitations
 
 Please note that `--nan-check` flag is adding not-a-number checks only for

regression/cbmc/pragma_cprover_enable1/test.desc

@@ -9,4 +9,4 @@ main.c
 ^SIGNAL=0$
 --
 --
-Checks that we can selectively activate checks using pragmas.
+Checks that we can selectively activate checks using pragmas.

regression/cbmc/pragma_cprover_enable3/test.desc

@@ -14,5 +14,5 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 --
-^\[main.pointer_primitives.\d+\] line 17 
+^\[main.pointer_primitives.\d+\] line 17
 --

regression/cbmc/pragma_cprover_enable_disable_global_off/test.desc

@@ -30,7 +30,7 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 --
-^\[main.pointer_primitives.\d+\] line 17 
-^\[main.pointer_primitives.\d+\] line 28 
-^\[main.pointer_primitives.\d+\] line 38 
+^\[main.pointer_primitives.\d+\] line 17
+^\[main.pointer_primitives.\d+\] line 28
+^\[main.pointer_primitives.\d+\] line 38
 --

regression/cbmc/pragma_cprover_enable_disable_global_on/test.desc

@@ -38,6 +38,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 --
-^\[main.pointer_primitives.\d+\] line 17 
-^\[main.pointer_primitives.\d+\] line 28 
+^\[main.pointer_primitives.\d+\] line 17
+^\[main.pointer_primitives.\d+\] line 28
 --

src/analyses/goto_check.cpp

@@ -1917,8 +1917,7 @@ void goto_checkt::goto_check(
     const auto &pragmas = i.source_location().get_pragmas();
     for(const auto &d : pragmas)
     {
-      auto err_msg = [&]()
-      {
+      auto err_msg = [&]() {
         return "Found enable and disable pragmas for " + id2string(d.first) +
                " at \n" + i.source_location().pretty();
       };
@@ -2041,8 +2040,7 @@ void goto_checkt::goto_check(
       // safety
       {
         flag_resett no_enum_check_flag_resetter;
-        auto err_msg = [&]()
-        {
+        auto err_msg = [&]() {
           return "no_enum_check flag disabled and enabled at \n" +
                  i.source_location().pretty();
         };

src/ansi-c/ansi_c_parser.cpp

@@ -1,6 +1,9 @@
 /*******************************************************************\
+
 Module:
+
 Author: Daniel Kroening, [email protected]
+
 \*******************************************************************/
 
 #include "ansi_c_parser.h"

src/ansi-c/ansi_c_parser.h

@@ -1,6 +1,9 @@
 /*******************************************************************\
+
 Module:
+
 Author: Daniel Kroening, [email protected]
+
 \*******************************************************************/