manual: cleaned up chapter about bug hunting

man/manual.md

@@ -863,85 +863,4 @@ Cppcheck output:
             foo(x);
                 ^
 
-## Philosopphy
-
-It is very important that we do warn about all unsafe code. We want that users can feel fully confident about the code we say is "safe".
-
-However, a sloppy analysis that will report too much noise will not be useful. We need to have strong heuristics to avoid false positives.
-
-At the moment there is no whole program analysis but that will be added later to avoid definite false positives.
-
-The focus will be to detect "hidden" bugs. Good candidates are undefined behavior that does not cause a crash immediately but will just cause strange behavior.
- * Buffer overflows
- * Uninitialized variables
- * Usage of dead pointers
-
-## Compiling
-
-make USE_Z3=yes
-
-## Verification for work-in-progress
-
-It is possible to instantly verify your code changes directly in your editor.
-
-You can for instance configure a save action like this:
-
-    cd repo ; git diff > temp.diff ; cppcheck --verify-diff=temp.diff
-
-Ensure that the warnings are sent to your editor and displayed.
-
-From now on, only use 'git commit' when you think all the verification warnings you get looks safe.
-
-With this method, Cppcheck will verify all functions that you are modifying.
-
-## Verification during review
-
-... well I am hoping it will be possible to integrate cppcheck verification in github, gerrit, etc.
-
-## Annotations
-
-To silence Cppcheck verification warnings it is possible to use annotations.
-
-Example code:
-
-    void foo(int x) {
-        return 10000 / x;
-    }
-
-Cppcheck verification will say that there is division and it can't determine that it's not division by zero.
-
-Example code with SAL annotation:
-
-    void foo(int _In_range_(1,1000) x) {
-        return 10000 / x;
-    }
-
-Example code with Cppcheck annotation:
-
-    void foo(int __cppcheck_low__(1) x) {
-        return 10000 / x;
-    }
-
-## Function calls
-
-For a reliable verification it will be very important that `--check-library` is used, you need to ensure that critical library functions are configured.
-
-### Uninitialized variables
-
-When `const` is used for pointer arguments that will be seen as a annotation.
-
-This function:
-
-    void foo(char *p);
-
-Cppcheck will assume that `p` points at uninitialized memory. When `foo` is checked it will be ensured that it initializes the memory.
-
-This function:
-
-    void foo(const char *p);
-
-Cppcheck will assume that `p` points at initialized memory. If you call `foo` and pass a pointer to uninitialized memory we will warn.
-
-TODO: Further annotations to specify how a function initializes memory will be required.
-