moved GoalInjector description

README.md

@@ -1,9 +1,6 @@
 # C-instrumentator
 A C instrumentation library
 
-The objective of this tool is to extend and reimplement some ideas from
-[FuSeBMC](https://github.com/kaled-alshmrany/FuSeBMC) in a way that is
-easier to integrate with ESBMC tools.
 
 # Project Structure
 
@@ -23,6 +20,28 @@ I want to keep the dependencies at a minimum. So far, the required dependencies
 
 Please, avoid adding dependencies. The idea is for this to be used as a library.
 
-# How it works
+# GoalInjector
+
+The objective of this instrumentation is to extend and reimplement some ideas from
+[FuSeBMC](https://github.com/kaled-alshmrany/FuSeBMC) in a way that is
+easier to integrate with ESBMC tools.
 
-It basically adds GOAL labels into something
+## Example
+
+```c
+int main() {
+  while(1)
+    while(1) ;
+  return 0;
+})";
+```
+
+is transformed into
+
+```c
+int main() {__ESBMC_assert(0, "0");
+  while(1)
+    {__ESBMC_assert(0, "1");while(1) {__ESBMC_assert(0, "2");;}}
+  return 0;
+})";
+```