Merge pull request #5652 from tautschnig/fix-cas

__atomic_compare_exchange{,_n}: correctly handle not-equal case

Author: kroening

regression/cbmc/atomic_load_store-1/main.c

@@ -15,6 +15,10 @@ int main()
   assert(__atomic_exchange_n(&x, 42, 0) == x_before);
   __atomic_exchange(&x, &v, &x_before, 0);
 
+  int v2 = x == 0;
+  assert(!__atomic_compare_exchange_n(&x, &v2, 42, 0, 0, 0));
+  assert(v2 == x);
+
   assert(__atomic_compare_exchange_n(&x, &v, 42, 0, 0, 0));
   v = 42;
   assert(__atomic_compare_exchange(&x, &v, &v, 0, 0, 0));

src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp

@@ -1166,17 +1166,20 @@ static void instantiate_atomic_compare_exchange(
     source_location}};
   success_fence.add_source_location() = source_location;
 
+  code_assignt assign_not_equal{dereference_exprt{parameter_exprs[1]},
+                                deref_ptr};
+  assign_not_equal.add_source_location() = source_location;
   code_expressiont failure_fence{side_effect_expr_function_callt{
     symbol_exprt::typeless("__atomic_thread_fence"),
     {parameter_exprs[5]},
     typet{},
     source_location}};
   failure_fence.add_source_location() = source_location;
 
-  block.add(
-    code_ifthenelset{result,
-                     code_blockt{{std::move(assign), std::move(success_fence)}},
-                     std::move(failure_fence)});
+  block.add(code_ifthenelset{
+    result,
+    code_blockt{{std::move(assign), std::move(success_fence)}},
+    code_blockt{{std::move(assign_not_equal), std::move(failure_fence)}}});
 
   block.add(code_expressiont{side_effect_expr_function_callt{
     symbol_exprt::typeless(CPROVER_PREFIX "atomic_end"),