Added concept of canonical goto program

Author: Enrico Steffinlongo

doc/ADR/README.md

@@ -6,6 +6,9 @@ where taken at the time they were, so that future maintainers
 can more easily identify constraints that shaped the architecture
 of the system and the surrounding infrastructure.
 
+## Canonical goto program
+\subpage canonical-goto
+
 ## Release & Packaging
 
 * \subpage release-process

doc/ADR/canonical_goto.md

@@ -0,0 +1,22 @@
+\page canonical-goto Canonical goto definition
+
+During the analysis of a program CBMC transforms the program in an intermediate language called
+extended goto. Then the tool performs a series of simplifications on the obtained goto program until
+the program is given to the solver.
+
+Here we define the concept of **canonical goto program** as a program that has been simplified to
+remove all extended-goto specific features.
+
+More specifically, a program that is in **canonical goto program form** is one that can be analyzed
+by any solver deriving from `goto_verifiert` by using the `goto_verifiert::operator()` function
+without requiring any lowering step.
+
+At the time of writing verifiers extending `goto_verifiert`, so defining what a **canonical goto
+program** is are:
+
+* `all_properties_verifier_with_fault_localizationt`,
+* `all_properties_verifier_with_trace_storaget`,
+* `all_properties_verifiert`,
+* `cover_goals_verifier_with_trace_storaget`,
+* `stop_on_fail_verifier_with_fault_localizationt`,
+* `stop_on_fail_verifiert`.