Fix contract enforcement to work with (local and global) static variables

Signed-off-by: Felipe R. Monteiro <[email protected]>

Author: feliperodri

regression/contracts/assigns_enforce_19/main.c

@@ -0,0 +1,33 @@
+#include <assert.h>
+
+static int b = 0;
+static int c = 0;
+
+int f() __CPROVER_assigns()
+{
+  static int a = 0;
+  a++;
+  return a;
+}
+
+int g(int *points_to_b, int *points_to_c)
+  __CPROVER_assigns(b) // Error: it should also mention c
+{
+  b = 1;
+  c = 2;
+  *points_to_b = 1;
+  *points_to_c = 2;
+}
+
+int main()
+{
+  assert(f() == 1);
+  assert(f() == 2);
+  assert(b == 0);
+  assert(c == 0);
+  g(&b, &c);
+  assert(b == 1);
+  assert(c == 2);
+
+  return 0;
+}

regression/contracts/assigns_enforce_19/test.desc

@@ -0,0 +1,17 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^\[f.\d+\] line \d+ Check that a is assignable: SUCCESS$
+^\[g.\d+\] line \d+ Check that b is assignable: SUCCESS$
+^\[g.\d+\] line \d+ Check that c is assignable: FAILURE$
+^\[g.\d+\] line \d+ Check that \*points\_to\_b is assignable: SUCCESS$
+^\[g.\d+\] line \d+ Check that \*points\_to\_c is assignable: FAILURE$
+^VERIFICATION FAILED$
+--
+--
+Checks whether contract enforcement works with (local and global) static variables.
+Local static variables should be part of the local write set.
+Global static variables should be included in the global write set,
+otherwise any assignment to it is invalid.

src/goto-instrument/contracts/contracts.cpp

@@ -678,6 +678,20 @@ void code_contractst::instrument_assign_statement(
 
   const exprt &lhs = instruction_iterator->assign_lhs();
 
+  // Local static variables are not declared locally, therefore, they are not
+  // included in the local write set during declaration. We check here whether
+  // lhs of the assignment is a local static variable and, if it is indeed
+  // true, we add lhs to our local write set before checking the assignment.
+  if(lhs.id() == ID_symbol)
+  {
+    auto lhs_sym = ns.lookup(lhs.get(ID_identifier));
+    if(
+      lhs_sym.is_static_lifetime &&
+      lhs_sym.location.get_function() ==
+        instruction_iterator->source_location.get_function())
+      assigns_clause.add_local_write_set(lhs);
+  }
+
   goto_programt alias_assertion;
   alias_assertion.add(goto_programt::make_assertion(
     assigns_clause.generate_containment_check(lhs),