Add regression test for fix to unified goto program processing

This adds a regression test that checks to ensure that goto-analyser
reaches the "Checking assertions" phase of it's execution and also
one of the checks was SUCCESFUL. This also fails on any invariant
violation.

Author: TGWDB

regression/goto-cc-goto-analyzer/instrument_preconditions_locations/s2n_hash_inlined.c

@@ -0,0 +1,44 @@
+struct evp_md_ctx_st
+{
+  const void *digest;
+};
+struct s2n_evp_digest
+{
+  const void *ctx;
+};
+union s2n_hash_low_level_digest {
+};
+struct s2n_hash_evp_digest
+{
+  struct s2n_evp_digest evp_md5_secondary;
+};
+struct s2n_hash_state
+{
+  const struct s2n_hash *hash_impl;
+  union {
+    union s2n_hash_low_level_digest low_level;
+    struct s2n_hash_evp_digest high_level;
+  } digest;
+};
+struct s2n_hash
+{
+  int (*free)(struct s2n_hash_state *state);
+};
+void EVP_MD_CTX_free(struct evp_md_ctx_st *ctx)
+{
+  free(ctx->digest);
+  free(ctx);
+}
+static int s2n_evp_hash_free(struct s2n_hash_state *state)
+{
+  (EVP_MD_CTX_free((state->digest.high_level.evp_md5_secondary.ctx)));
+  return 0;
+}
+static const struct s2n_hash s2n_evp_hash = {
+  .free = &s2n_evp_hash_free,
+};
+static int s2n_hash_set_impl(struct s2n_hash_state *state)
+{
+  state->hash_impl = &s2n_evp_hash;
+  return 0;
+}

regression/goto-cc-goto-analyzer/instrument_preconditions_locations/simple.c

@@ -0,0 +1,3 @@
+void s2n_hash_free_harness()
+{
+}

regression/goto-cc-goto-analyzer/instrument_preconditions_locations/test.desc

@@ -0,0 +1,16 @@
+CORE
+test.c
+--verify
+^EXIT=0$
+^SIGNAL=0$
+Checking assertions
+^\[EVP_MD_CTX_free.precondition_instance.1\] line \d+ free argument must be NULL or valid pointer: SUCCESS
+--
+Invariant check failed
+--
+This test checks that after building the goto binary (see test.sh)
+that there is no errors that lead to invariant violations.
+This was created after a bug was found due to the
+instrument_preconditions code not correctly fixing locations and
+the invariant check of partial inlining detecting this location
+inconsistency.

regression/goto-cc-goto-analyzer/instrument_preconditions_locations/test.sh

@@ -0,0 +1,18 @@
+#!/usr/bin/env bash
+set -e
+
+goto_cc=$1
+is_windows=$2
+
+if [[ "${is_windows}" == "true" ]]; then
+  ${goto_cc}  --export-file-local-symbols  simple.c 
+  mv simple.exe simple.gb
+  ${goto_cc}  --export-file-local-symbols  s2n_hash_inlined.c
+  mv s2n_hash_inlined.exe s2n_hash_inlined.gb
+  ${goto_cc}  --function s2n_hash_free_harness simple.gb s2n_hash_inlined.gb
+  mv simple.exe test.gb
+else
+  ${goto_cc}  --export-file-local-symbols  simple.c -o simple.gb
+  ${goto_cc}  --export-file-local-symbols  s2n_hash_inlined.c -o s2n_hash_inlined.gb
+  ${goto_cc}  --function s2n_hash_free_harness simple.gb s2n_hash_inlined.gb -o test.gb
+fi