From 7cb0981f14e25435d8267d86690965ca74c0e448 Mon Sep 17 00:00:00 2001
From: Enrico Steffinlongo <enrico.steffinlongo@diffblue.com>
Date: Wed, 25 Jan 2023 17:11:25 +0000
Subject: [PATCH] Added concept of canonical goto program

---
 doc/ADR/README.md    |  3 +++
 doc/ADR/core_goto.md | 20 ++++++++++++++++++++
 2 files changed, 23 insertions(+)
 create mode 100644 doc/ADR/core_goto.md

diff --git a/doc/ADR/README.md b/doc/ADR/README.md
index 489f3e5fe37..9420ce20d83 100644
--- a/doc/ADR/README.md
+++ b/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.
 
+## Core goto form
+\subpage core-goto
+
 ## Release & Packaging
 
 * \subpage release-process
diff --git a/doc/ADR/core_goto.md b/doc/ADR/core_goto.md
new file mode 100644
index 00000000000..1104942ab8e
--- /dev/null
+++ b/doc/ADR/core_goto.md
@@ -0,0 +1,20 @@
+\page core-goto Core goto definition
+
+During the analysis of a program CBMC transforms the input 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.
+
+We say that a program is in the **core goto form** when all the extended goto features have
+been simplified.
+
+More specifically, a program that is in **core goto form** is one that can be passed to **symex** by
+using any solver deriving from `goto_verifiert` without requiring any lowering step.
+
+At the time of writing, verifiers extending `goto_verifiert` 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`.