Fix shadow memory param1 regression test

Enrico Steffinlongo · Enrico Steffinlongo · commit 6f974d706e4b · 2023-09-05T18:01:45.000+02:00
diff --git a/regression/cbmc-shadow-memory/param1/main.c b/regression/cbmc-shadow-memory/param1/main.c
@@ -103,7 +103,7 @@ void f_int_local(int rec, int value)
 
 int main()
 {
-  __CPROVER_field_decl_local("field1", (char)0);
+  __CPROVER_field_decl_local("field1", (unsigned char)0);
   int x;
   __CPROVER_set_field(&x, "field1", 255);
   f_int_val(x);
diff --git a/regression/cbmc-shadow-memory/param1/test.desc b/regression/cbmc-shadow-memory/param1/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=0$

Original file line number	Diff line number	Diff line change
`@@ -103,7 +103,7 @@ void f_int_local(int rec, int value)`
`103`	`103`
`104`	`104`	`int main()`
`105`	`105`	`{`
`106`		`- __CPROVER_field_decl_local("field1", (char)0);`
	`106`	`+ __CPROVER_field_decl_local("field1", (unsigned char)0);`
`107`	`107`	`int x;`
`108`	`108`	`__CPROVER_set_field(&x, "field1", 255);`
`109`	`109`	`f_int_val(x);`