Add elegant extension to signs analysis tutorial

docs/developer-guide/firstanalysis.md

@@ -72,4 +72,11 @@ With this in place, we should have sufficient information to tell Goblint that t
 
 ## Extending the domain
 
-You could now independently enrich the lattice to also keep track of non-negative and non-positive values, such that the join of Zero and Pos is NonNeg, and then handle assertions for `x >= 0`.
+You could now enrich the lattice to also have a representation for non-negative (i.e., zero or positive) values.
+Then the join of `Zero` and `Pos` would be "non-negative" instead of `Top`, allowing you to prove that such join is greated than `Neg`.
+For example, have a look at the following program: `tests/regression/99-tutorials/02-first-extend.c`.
+
+_Hint:_
+The easiest way to do this is to use the powerset lattice of `{-, 0, +}`.
+For example, "non-negative" is represented by `{0, +}`, while negative is represented by `{-}`.
+To do this, modify `SL` by using `SetDomain.Make` instead of `Lattice.Flat` and reimplementing the two functions using `singleton` and `for_all`.

tests/regression/99-tutorials/02-first-extend.c

@@ -0,0 +1,20 @@
+// PARAM: --set "ana.activated[+]" signs
+#include <assert.h>
+
+int main() {
+  int x;
+  int unknown;
+
+  if (unknown) {
+    x = 5;
+  } else {
+    x = 0;
+  }
+
+  // The above code branches on an uninitialized variable.
+  // The value of x could be either 5 or 0.
+
+  assert(x > -1); // TODO: Thus, this assertion should hold!
+
+  return 0;
+}