fx

Author: kroening

regression/cbmc/map-type/basic1.c

@@ -2,9 +2,9 @@ int main()
 {
   __CPROVER_map(int, int) my_map;
 
-  my_map[1] = 10;
-  my_map[2] = 20;
+  my_map = __CPROVER_map_update(my_map, 1, 10);
+  my_map = __CPROVER_map_update(my_map, 2, 20);
 
-  __CPROVER_assert(my_map[1] == 10, "[1]");
-  __CPROVER_assert(my_map[2] == 20, "[2]");
+  __CPROVER_assert(my_map(1) == 10, "[1]");
+  __CPROVER_assert(my_map(2) == 20, "[2]");
 }

src/ansi-c/c_typecheck_expr.cpp

@@ -2534,6 +2534,7 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
     function_application_exprt function_application(f_op, expr.arguments());
 
     function_application.add_source_location() = expr.source_location();
+    function_application.type() = mathematical_function_type.codomain();
 
     expr.swap(function_application);
     return;