Make flattening accept negative array sizes

romainbrenguier · romainbrenguier · commit d6da90945c1b · 2019-09-25T12:07:21.000+01:00
If the specified array size is negative just do as if it was 0, this is
similar to the case where the array size is not given.
diff --git a/src/solvers/flattening/boolbv_width.cpp b/src/solvers/flattening/boolbv_width.cpp
@@ -141,7 +141,10 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
       if(total>(1<<30)) // realistic limit
         throw analysis_exceptiont("array too large for flattening");
 
-      entry.total_width = numeric_cast_v<std::size_t>(total);
+      if(total < 0)
+        entry.total_width = 0;
+      else
+        entry.total_width = numeric_cast_v<std::size_t>(total);
     }
   }
   else if(type_id==ID_vector)

Original file line number	Diff line number	Diff line change
`@@ -141,7 +141,10 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const`
`141`	`141`	`if(total>(1<<30)) // realistic limit`
`142`	`142`	`throw analysis_exceptiont("array too large for flattening");`
`143`	`143`
`144`		`- entry.total_width = numeric_cast_v<std::size_t>(total);`
	`144`	`+ if(total < 0)`
	`145`	`+ entry.total_width = 0;`
	`146`	`+ else`
	`147`	`+ entry.total_width = numeric_cast_v<std::size_t>(total);`
`145`	`148`	`}`
`146`	`149`	`}`
`147`	`150`	`else if(type_id==ID_vector)`