CONTRACTS: new test with ternary assignment LHS

Author: Remi Delmas

regression/contracts-dfcc/ternary-lhs-loop-contract/main.c

@@ -0,0 +1,25 @@
+#include <stdbool.h>
+#include <stdlib.h>
+
+void foo(int a, int b)
+{
+  char arr1[10];
+  char arr2[10];
+  char arr3[10];
+  int i = 0;
+
+  while(i < 10)
+    __CPROVER_loop_invariant(0 <= i && i <= 10)
+    {
+      ((a > 0) ? arr1 : b > 0 ? arr2 : arr3)[i] = 0;
+      i++;
+    }
+}
+
+int main()
+{
+  int a;
+  int b;
+  foo(a, b);
+  return 0;
+}

regression/contracts-dfcc/ternary-lhs-loop-contract/test.desc

@@ -0,0 +1,11 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo --apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+checks that when assignment lhs expressions have ternary expressions,
+loop assigns clause checking correctly infers what gets assigned and
+automatically tracks targets in the both the top level and the loop write sets.