Support out-of-bounds checks on arrays of dynamic size
Previously the code would rely on type sizes being constant when building a subtraction; this is unnecessary as the expression is sent to the solver for evaluation anyway.
This commit is contained in:
parent
49bceb269a
commit
d078dd89e5
|
@ -0,0 +1,14 @@
|
|||
#include <stdlib.h>
|
||||
|
||||
int main()
|
||||
{
|
||||
unsigned x;
|
||||
|
||||
int *A=malloc(x*sizeof(int));
|
||||
|
||||
char *p=&A[1];
|
||||
|
||||
char c=*p;
|
||||
|
||||
return c;
|
||||
}
|
|
@ -0,0 +1,9 @@
|
|||
CORE
|
||||
main.c
|
||||
--pointer-check
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^VERIFICATION FAILED$
|
||||
--
|
||||
^warning: ignoring
|
||||
^unknown or invalid type size:
|
|
@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
#include <cassert>
|
||||
|
||||
#include <util/invariant.h>
|
||||
#include <util/string2int.h>
|
||||
#include <util/expr_util.h>
|
||||
#include <util/base_type.h>
|
||||
|
@ -858,16 +859,24 @@ bool value_set_dereferencet::memory_model_bytes(
|
|||
{
|
||||
// upper bound
|
||||
{
|
||||
mp_integer from_width=pointer_offset_size(from_type, ns);
|
||||
if(from_width<=0)
|
||||
throw "unknown or invalid type size:\n"+from_type.pretty();
|
||||
exprt from_width=size_of_expr(from_type, ns);
|
||||
INVARIANT(
|
||||
from_width.is_not_nil(),
|
||||
"unknown or invalid type size:\n"+from_type.pretty());
|
||||
|
||||
mp_integer to_width=
|
||||
to_type.id()==ID_empty?0: pointer_offset_size(to_type, ns);
|
||||
if(to_width<0)
|
||||
throw "unknown or invalid type size:\n"+to_type.pretty();
|
||||
exprt to_width=
|
||||
to_type.id()==ID_empty?
|
||||
from_integer(0, size_type()):size_of_expr(to_type, ns);
|
||||
INVARIANT(
|
||||
to_width.is_not_nil(),
|
||||
"unknown or invalid type size:\n"+to_type.pretty());
|
||||
INVARIANT(
|
||||
from_width.type()==to_width.type(),
|
||||
"type mismatch on result of size_of_expr");
|
||||
|
||||
exprt bound=from_integer(from_width-to_width, offset.type());
|
||||
minus_exprt bound(from_width, to_width);
|
||||
if(bound.type()!=offset.type())
|
||||
bound.make_typecast(offset.type());
|
||||
|
||||
binary_relation_exprt
|
||||
offset_upper_bound(offset, ID_gt, bound);
|
||||
|
|
Loading…
Reference in New Issue