CONTRACTS: use map.element_type() in index_exprt

Remi Delmas · Remi Delmas · commit fe2ddda95f9d · 2022-10-26T11:50:39.000-04:00
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp
@@ -520,7 +520,7 @@ const symbolt &dfcc_libraryt::get_instrumented_functions_map_symbol()
     source_locationt{},
     ID_C,
     "<built-in-library>",
-    array_of_exprt(from_integer(0, unsigned_char_type()), map_type),
+    array_of_exprt(from_integer(0, map_type.element_type()), map_type),
     true);
 }
 

Original file line number	Diff line number	Diff line change
`@@ -520,7 +520,7 @@ const symbolt &dfcc_libraryt::get_instrumented_functions_map_symbol()`
`520`	`520`	`source_locationt{},`
`521`	`521`	`ID_C,`
`522`	`522`	`"<built-in-library>",`
`523`		`- array_of_exprt(from_integer(0, unsigned_char_type()), map_type),`
	`523`	`+ array_of_exprt(from_integer(0, map_type.element_type()), map_type),`
`524`	`524`	`true);`
`525`	`525`	`}`
`526`	`526`