public boolean isSafe() {
if (!left.isSafe())
return false;
+
FieldDescriptor tmpfd=fd;
- if (tmpfd instanceof ArrayDescriptor)
- return false; // Arrays could be out of bounds
+
if (tmpfd.getPtr()) // Pointers cound be invalid
return false;
- return true;
+
+ if (tmpfd instanceof ArrayDescriptor) {
+ Expr arrayindex=((ArrayDescriptor)tmpfd).getIndexBound();
+ if (index instanceof IntegerLiteralExpr&&arrayindex instanceof IntegerLiteralExpr) {
+ int indexvalue=((IntegerLiteralExpr)index).getValue();
+ int arrayindexvalue=((IntegerLiteralExpr)arrayindex).getValue();
+ if (indexvalue>=0&&indexvalue<arrayindexvalue)
+ return true;
+ }
+ return false; // Otherwise, arrays could be out of bounds
+ }
+ return true;
}
public Set freeVars() {
if (intindex != null) {
v.addAll(intindex.getRequiredDescriptors());
}
+ v.add(fd);
return v;
}
if (writer.getInvariantValue()!=null&&
writer.getInvariantValue().isInvariant(this)) {
- writer.outputline(getType().getGenerateType().getSafeSymbol()+
- " "+dest.getSafeSymbol()+"="+writer.getInvariantValue().getValue(this).getSafeSymbol()+";");
+ writer.addDeclaration(getType().getGenerateType().getSafeSymbol().toString(), dest.getSafeSymbol());
+ writer.outputline(dest.getSafeSymbol()+"="+writer.getInvariantValue().getValue(this).getSafeSymbol()+";");
writer.outputline("maybe="+writer.getInvariantValue().getMaybe(this).getSafeSymbol()+";");
return;
}
boolean doboundscheck=true;
boolean performedboundscheck=false;
- writer.outputline(getType().getGenerateType() + " " + dest.getSafeSymbol()+"=0;");
+ writer.addDeclaration(getType().getGenerateType().toString(),dest.getSafeSymbol());
+ writer.outputline(dest.getSafeSymbol()+"=0;");
if (intindex != null) {
if (intindex instanceof IntegerLiteralExpr && ((IntegerLiteralExpr) intindex).getValue() == 0) {
/* derive offset in bytes */
VarDescriptor offset = VarDescriptor.makeNew("offset");
- writer.outputline("int " + offset.getSafeSymbol() + " = " + ob.getSafeSymbol() + " >> 3;");
+ writer.addDeclaration("int", offset.getSafeSymbol());
+ writer.outputline(offset.getSafeSymbol() + " = " + ob.getSafeSymbol() + " >> 3;");
if (fd.getType() instanceof ReservedTypeDescriptor && !fd.getPtr()) {
VarDescriptor shift = VarDescriptor.makeNew("shift");
- writer.outputline("int " + shift.getSafeSymbol() + " = " + ob.getSafeSymbol() +
+ writer.addDeclaration("int", shift.getSafeSymbol());
+ writer.outputline(shift.getSafeSymbol() + " = " + ob.getSafeSymbol() +
" - (" + offset.getSafeSymbol() + " << 3);");
int mask = bitmask(((IntegerLiteralExpr)fd.getType().getSizeExpr()).getValue());
writer.startblock();
VarDescriptor typevar=VarDescriptor.makeNew("typechecks");
if (DOMEMCHECKS&&(!DOTYPECHECKS)) {
- writer.outputline("bool "+typevar.getSafeSymbol()+"=assertvalidmemory(" + dest.getSafeSymbol() + ", " + this.td.getId() + ");");
+ writer.addDeclaration("bool", typevar.getSafeSymbol());
+ writer.outputline(typevar.getSafeSymbol()+"=assertvalidmemory(" + dest.getSafeSymbol() + ", " + this.td.getId() + ");");
dotypecheck = true;
} else if (DOTYPECHECKS) {
- writer.outputline("bool "+typevar.getSafeSymbol()+"=assertvalidtype(" + dest.getSafeSymbol() + ", " + this.td.getId() + ");");
+ writer.addDeclaration("bool", typevar.getSafeSymbol());
+ writer.outputline(typevar.getSafeSymbol()+"=assertvalidtype(" + dest.getSafeSymbol() + ", " + this.td.getId() + ");");
}
if (DOTYPECHECKS||DOMEMCHECKS) {
assert intindex == null;
intindex = ld.getIndex();
} else {
+ if (fd==null) {
+ throw new Error("Null fd for: "+field);
+ }
fieldtype = fd.getType();
intindex=index;
}