Simplifier does not modify out-of-bounds access

kroening · kroening · commit 5e1d557ec85c · 2016-02-17T17:23:34.000Z
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@6390 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
diff --git a/src/solvers/flattening/boolbv_index.cpp b/src/solvers/flattening/boolbv_index.cpp
@@ -339,6 +339,12 @@ void boolbvt::convert_index(
      offset+width<=mp_integer(tmp.size()))
   {
     // in bounds
+
+    // Expression simplification should remove these cases
+    assert(array.id()!=ID_array_of &&
+           array.id()!=ID_array);
+    // If not there are large improvements possible as above
+
     for(unsigned i=0; i<width; i++)
       bv[i]=tmp[integer2long(offset+i)];
   }

Original file line number	Diff line number	Diff line change
`@@ -339,6 +339,12 @@ void boolbvt::convert_index(`
`339`	`339`	`offset+width<=mp_integer(tmp.size()))`
`340`	`340`	`{`
`341`	`341`	`// in bounds`
	`342`	`+`
	`343`	`+ // Expression simplification should remove these cases`
	`344`	`+ assert(array.id()!=ID_array_of &&`
	`345`	`+ array.id()!=ID_array);`
	`346`	`+ // If not there are large improvements possible as above`
	`347`	`+`
`342`	`348`	`for(unsigned i=0; i<width; i++)`
`343`	`349`	`bv[i]=tmp[integer2long(offset+i)];`
`344`	`350`	`}`