Updates requested in the PR.

Author: marek-trtik

src/goto-programs/README.md

@@ -379,37 +379,38 @@ This stage concludes the *analysis-independent* program transformations.
 To be documented.
 
 
-\section section-goto-binary Binary Represenration
+\section section-goto-binary Binary Representation
 
-An instance of `goto_modelt` can be serialised to a binary stream (which is
+An instance of `::goto_modelt` can be serialised to a binary stream (which is
 typically a file on the disk), and later deserialised from that stream back to
-an equivalent `goto_modelt` instance.
+an equivalent `::goto_modelt` instance.
 
 \subsection subsection-goto-binary-serialisation Serialisation
 
 The serialisation is implemented in C++ modules:
   - `write_goto_binary.h`
   - `write_goto_binary.cpp`
 
-To serialise a `goto_modelt` instance `gm` to a stream `ostr` call the function `write_goto_binary`, e.g. `write_goto_binary(ostr, gm)`.
+To serialise a `::goto_modelt` instance `gm` to a stream `ostr` call the
+function `::write_goto_binary`, e.g. `write_goto_binary(ostr, gm)`.
 
-The content of the written stream will have this strucutre:
+The content of the written stream will have this structure:
   - The header:
     - A magic number: byte `0x7f` followed by 3 characters `GBF`.
-    - A version number written in the 7-bit encoding. Currently, only version `4` is supported.
+    - A version number written in the 7-bit encoding (see [number serialisation](\ref irep-serialization-numbers)). Currently, only version `4` is supported.
   - The symbol table:
     - The number of symbols in the table in the 7-bit encoding.
     - The array of individual symbols in the table. Each written symbol `s` has this structure:
-      - The `irept` instance `s.type`.
-      - The `irept` instance `s.value`.
-      - The `irept` instance `s.location`.
+      - The `::irept` instance `s.type`.
+      - The `::irept` instance `s.value`.
+      - The `::irept` instance `s.location`.
       - The string `s.name`.
       - The string `s.module`.
       - The string `s.base_name`.
       - The string `s.mode`.
       - The string `s.pretty_name`.
       - The number `0` in the 7-bit encoding.
-      - The flags word in the 7-bit encoding. The bits in the flags word correspond to the following `bool` fields (from the most significant bit):
+      - The flags word in the 7-bit encoding. The bits in the flags word correspond to the following `Boolean` fields (from the most significant bit):
         - `s.is_weak`
         - `s.is_type`
         - `s.is_property`
@@ -429,33 +430,33 @@ The content of the written stream will have this strucutre:
         - `s.is_volatile`
   - The functions with bodies, i.e. those missing a body are skipped.
     - The number of functions with bodies in the 7-bit encoding.
-    - The array of individual function with bodies. Each written function has this structure:
+    - The array of individual functions with bodies. Each written function has this structure:
       - The string with the name of the function.
       - The number of instructions in the body of the function in the 7-bit encoding.
-      - The array of individual instruction in function's body. Each written instruction `I` has this structure:
-        - The `irept` instance `I.code`, i.e. data of the instruction, like arguments.
+      - The array of individual instructions in function's body. Each written instruction `I` has this structure:
+        - The `::irept` instance `I.code`, i.e. data of the instruction, like arguments.
         - The string `I.function`, i.e. the name of the function this instruction belongs to.
-        - The `irept` instance `I.source_location`, i.e. the reference to the original source code (file, line).
+        - The `::irept` instance `I.source_location`, i.e. the reference to the original source code (file, line).
         - The word in the 7-bit encoding `I.type`, i.e. the op-code of the instruction.
-        - The `irept` instance `I.guard`.
+        - The `::irept` instance `I.guard`.
         - The empty string (representing former `I.event`).
         - The word in the 7-bit encoding `I.target_number`, i.e. the jump target to this instruction from other instructions.
         - The word in the 7-bit encoding `I.targets.size()`, i.e. the count of jump targets from this instruction.
         - The array of individual jump targets from this instruction, each written as a word in the 7-bit encoding.
         - The word in the 7-bit encoding `I.labels.size()`.
         - The array of individual labels, each written as a word in the 7-bit encoding.
 
-An important propery of the serialisation is that each serialised `irept`
+An important propery of the serialisation is that each serialised `::irept`
 instance occurs in the stream exactly once. Namely, in the position of
-its first serialisation query. All other such queries save only hash
-code (i.e. reference) of the `irept` instance.
+its first serialisation query. All other such queries save only a hash
+code (i.e. reference) of the `::irept` instance.
 
-The similar strategy is used for serialisation of string constants
-shared amongst `irept` instances. Such a string is fully saved only in
-the first serialisation query of an `irept` instance it appears in and
-all other queries only save its integer has code.
+A similar strategy is used for serialisation of string constants
+shared amongst `::irept` instances. Such a string is fully saved only in
+the first serialisation query of an `::irept` instance it appears in and
+all other queries only save its integer hash code.
 
-Details about serialisation of `irept` instances, strings, and words in
+Details about serialisation of `::irept` instances, strings, and words in
 7-bit encoding can be found [here](\ref irep-serialization).
 
 \subsection subsection-goto-binary-deserialisation Deserialisation
@@ -466,29 +467,30 @@ The deserialisation is implemented in C++ modules:
   - `read_bin_goto_object.h`
   - `read_bin_goto_object.cpp`
 
-First two modules are responsible for location of the stream with the
+The first two modules are responsible for location of the stream with the
 serialised data within a passed file. And the remaining two modules
-perform the actual deserialisation of `goto_modelt` instance from
+perform the actual deserialisation of a `::goto_modelt` instance from
 the located stream.
 
-To deserialise a `goto_modelt` instance `gm` from a file `/some/path/name.gbf`
-call the function `read_goto_binary`, e.g.
+To deserialise a `::goto_modelt` instance `gm` from a file
+`/some/path/name.gbf` call the function `::read_goto_binary`, e.g.
 `read_goto_binary("/some/path/name.gbf", gm, message_handler)`, where
-`message_handler` must be an instance of `message_handlert` and serves
+`message_handler` must be an instance of `::message_handlert` and serves
 for reporting issues during the process.
 
 The passed binary file is assumed to have the same structure as described in
 the [previous subsection](\ref subsection-goto-binary-serialisation).
 The process of the deserialisation does not involve any seeking in the file.
-The content is read linearly from the beginning to the end. `irept` instances
-and their string constats are deserialised into the memory only once at their
-first occurreces in the stream. All subsequent deserialisation queries are
-resolved as in-memory references to the `irept` instances and/or strings.
+The content is read linearly from the beginning to the end. `::irept` instances
+and their string constants are deserialised into the memory only once at their
+first occurrences in the stream. All subsequent deserialisation queries are
+resolved as in-memory references to already deserialised the `::irept`
+instances and/or strings, based on hash code matching.
 
 NOTE: The first deserialisation is detected so that the loaded hash code
 is new. That implies that the full definition follows right after the hash.
 
-Details about serialisation of `irept` instances, strings, and words in
+Details about serialisation of `::irept` instances, strings, and words in
 7-bit encoding can be found [here](\ref irep-serialization).
 
 \subsubsection subsection-goto-binary-deserialisation-from-elf Deserialisation from ELF image
@@ -498,24 +500,24 @@ One can decide to store the serialised stream as a separate section, named
 automatic detection of that section in an ELF file and the deserialisation
 will be automatically started from that section.
 
-For reading the ELF images there is used an instance of `elf_readert`
+For reading the ELF images there is used an instance of `::elf_readert`
 implemented in the C++ module:
   - `elf_reader.h`
   - `elf_reader.cpp`
 
-\subsubsection subsection-goto-binary-deserialisation-from-mac-o-fat-image Deserialisation from Mac-O fat image
+\subsubsection subsection-goto-binary-deserialisation-from-mach-o-fat-image Deserialisation from Mach-O fat image
 
-One can decide to store the serialised stream into Mac-O fat image as a
+One can decide to store the serialised stream into Mach-O fat image as a
 separate non-empty section with flags `CPU_TYPE_HPPA` and
 `CPU_SUBTYPE_HPPA_7100LC`. Then the deserialisation has a support of
-automatic detection of that section in a Mac-O fat image, extraction
+automatic detection of that section in a Mach-O fat image, extraction
 of the section from the emage into a temporary file (this is done by
 calling `lipo` utility with `-thin hppa7100LC` option), and the
 deserialisation will be automatically started from that temporary
 file.
 
-For reading the Mac-O fat images there is used an instance of
-`osx_fat_readert` implemented in the C++ module:
+For reading the Mach-O fat images there is used an instance of
+`::osx_fat_readert` implemented in the C++ module:
   - `osx_fat_reader.h`
   - `osx_fat_reader.cpp`
 
@@ -524,25 +526,25 @@ on a MacOS machine.
 
 \subsubsection subsection-goto-binary-is-binary-file Checking file type
 
-You can use function `is_goto_binary` to check whether a passed file contains
-a sederialised `goto_modelt` instance or not. This is done by checking the
+You can use function `::is_goto_binary` to check whether a passed file contains
+a deserialised `::goto_modelt` instance or not. This is done by checking the
 magic number of the stream (see subsection
 [Serialisation](\ref subsection-goto-binary-serialisation)). However, in the
-case when the deserialised data were stored into ELF or Mac-O fat image, then
+case when the deserialised data were stored into ELF or Mach-O fat image, then
 only the check for presence of the concrete section in the image is performed.
 
 \subsubsection subsection-goto-binary-deserialisation-linking Linking Goto Models
 
 Similar to linking of object files together by C/C++ linker, the module
-provides linking of a dereserialised `goto_modelt` instance into a given
-(i.e. previously deserialised or otherwise created) `goto_modelt` instance.
+provides linking of a dereserialised `::goto_modelt` instance into a given
+(i.e. previously deserialised or otherwise created) `::goto_modelt` instance.
 
-This is implemented in function `read_object_and_link`. The function first
-deserialises the passed file into a temporary `goto_modelt` instance, and
+This is implemented in function `::read_object_and_link`. The function first
+deserialises the passed file into a temporary `::goto_modelt` instance, and
 then it performs 'linking' of the temporary into a passed destination
-`goto_modelt` instance.
+`::goto_modelt` instance.
 
-Details about linking of `goto_modelt` instances can be found
+Details about linking of `::goto_modelt` instances can be found
 [here](\ref section-linking-goto-models).
 
 

src/util/README.md

@@ -162,15 +162,15 @@ This is implemented in C++ modules:
 
 \subsubsection irep-serialization-numbers Serialization of Numbers
 
-A number is serialiased in 7-bit encoding. For example. given a 2-byte
-number in base 2, like `10101010 01010101`, then it is save in 3 bytes,
+A number is serialiased in 7-bit encoding. For example, given a 2-byte
+number in base 2, like `10101010 01010101`, then it is saves in 3 bytes,
 where each byte takes only 7 bits from the number, reading from the
 left. The 8th bit in each output byte is set to 1 except in the last
-byte, where the bit is 0. That 0 bit indicates the end of the end
+byte, where the bit is 0. That 0 bit indicates the end of the
 encoding of the number. So, the output bytes look like this:
 `11010101 11010100 00000010`.
 
-This is implmented in the function `write_gb_word`.
+This is implmented in the function `::write_gb_word`.
 
 The deserialisation does the oposite process and it is implemented in
 `irep_serializationt::read_gb_word`.
@@ -181,10 +181,10 @@ A string is encoded as classic 0-terminated C string. However,
 characters `0` and `\\` are escaped by writing additional `\\` 
 before them. 
 
-This is implmented in the function `write_gb_string` and the
+This is implmented in the function `::write_gb_string` and the
 deserialisation is implemented in `irep_serializationt::read_gb_string`.
 
-Each string which is stored inside an `irept` instance is saved (meaining
+Each string which is stored inside an `::irept` instance is saved (meaining
 its characters) into the ouptut stream, only in the first serialisation
 query of the string. In that case, before the string there is also saved
 a computed integer hash code of the string. Then, all subsequent