Fixed doc, commits and formatting

Author: Remi Delmas

regression/contracts/assigns_enforce_arrays_05/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract assigns_ptr --enforce-contract assigns_range
+--enforce-contract assigns_range
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/contracts/quantifiers-forall-ensures-enforce/main.c

@@ -23,7 +23,7 @@ int f1(int *arr, int len)
 int main()
 {
   int len;
-  __CPROVER_assume(0 <= len && len <= MAX_LEN);
+  __CPROVER_assume(0 < len && len <= MAX_LEN);
 
   int *arr = malloc(len * sizeof(int));
   f1(arr, len);

src/analyses/goto_check.cpp

@@ -25,8 +25,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/ieee_float.h>
 #include <util/invariant.h>
 #include <util/make_unique.h>
-#include <util/options.h>
 #include <util/message.h>
+#include <util/options.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
@@ -50,10 +50,8 @@ class goto_checkt
   goto_checkt(
     const namespacet &_ns,
     const optionst &_options,
-    message_handlert &_message_handler):
-    ns(_ns),
-    local_bitvector_analysis(nullptr),
-    log(_message_handler)
+    message_handlert &_message_handler)
+    : ns(_ns), local_bitvector_analysis(nullptr), log(_message_handler)
   {
     no_enum_check = false;
     enable_bounds_check=_options.get_bool_option("bounds-check");
@@ -1856,7 +1854,7 @@ optionalt<exprt> goto_checkt::rw_ok_check(exprt expr)
 class flag_resett
 {
 public:
-  /// \brief Store the current value of \p flag and 
+  /// \brief Store the current value of \p flag and
   /// then set its value to \p new_value.
   /// \returns true if the flag was already seen before
   bool set_flag(bool &flag, bool new_value)
@@ -1877,7 +1875,7 @@ class flag_resett
     return seen_flags.find(&flag) != seen_flags.end();
   }
 
-  /// \brief Restore the values of all flags that have been 
+  /// \brief Restore the values of all flags that have been
   /// modified via `set_flag`.
   ~flag_resett()
   {

src/goto-instrument/contracts/assigns.cpp

@@ -81,6 +81,22 @@ assigns_clauset::conditional_address_ranget::conditional_address_ranget(
 {
 }
 
+// clang-format off
+/// \brief Generates and returns snapshot instructions for source_expr.
+///
+/// ```
+/// DECL bool __car_valid
+/// DECL char *__car_lb
+/// DECL char *__car_ub
+/// ASSIGN __car_lb := NULL
+/// ASSIGN __car_ub := NULL
+/// ASSIGN __car_valid := all_dereferences_are_valid(source_expr) & rw_ok(&(source_expr), size)
+/// IF !__car_valid GOTO END_SNAPSHOT
+/// ASSIGN __car_lb := &(source_expr)
+/// ASSIGN __car_ub := &(source_expr) + size-1
+/// END_SNAPSHOT: SKIP
+/// ```
+// clang-format on
 goto_programt
 assigns_clauset::conditional_address_ranget::generate_snapshot_instructions()
   const
@@ -109,16 +125,17 @@ assigns_clauset::conditional_address_ranget::generate_snapshot_instructions()
     null_pointer_exprt{to_pointer_type(slice.first.type())},
     location_no_checks));
 
-  goto_programt skip_program;
-  const auto skip_target =
-    skip_program.add(goto_programt::make_skip(location_no_checks));
-
+  // check validity
   const auto validity_check_expr = and_exprt{
     all_dereferences_are_valid(source_expr, parent.ns),
     w_ok_exprt{slice.first, slice.second}};
   instructions.add(goto_programt::make_assignment(
     validity_condition_var, validity_check_expr, location_no_checks));
 
+  // jump here if validity_check_expr is false
+  goto_programt skip_program;
+  const auto skip_target = skip_program.add(goto_programt::make_skip(location));
+
   instructions.add(goto_programt::make_goto(
     skip_target, not_exprt{validity_condition_var}, location_no_checks));
 

src/goto-instrument/contracts/contracts.h

@@ -216,7 +216,6 @@ class code_contractst
   ///
   /// @param function the function to search local static symbols in
   /// @param assigns assigns clause where search results are added
-  /// @return true if failure, false if success
   ///
   /// A symbol is considered a static local symbol iff:
   /// - it has a static lifetime annotation

src/goto-instrument/contracts/utils.h

@@ -91,10 +91,16 @@ void insert_before_swap_and_advance(
 
 /// \brief Adds a new temporary symbol to the symbol table.
 ///
+/// The unique name is generated as:
+/// ```
+/// "location.function() + "::" + suffix + "$" + uid
+/// ```
+///
 /// \param type: The type of the new symbol.
 /// \param location: The source location for the new symbol.
 /// \param mode: The mode for the new symbol, e.g. ID_C, ID_java.
 /// \param symtab: The symbol table to which the new symbol is to be added.
+/// \param suffix: base suffix used to generate the unique name.
 /// \return The new symbolt object.
 const symbolt &new_tmp_symbol(
   const typet &type,