@Untainted multiplied by a constant should be @Untainted

[GoogleCodeExporter]

Currently an @Untainted int multiplied by a constant is @Tainted, e.g.
"z" below is currently @Tainted

void test(@Untainted int x) {
    y = x * 10;
    String z = "test" + y;
}

Original issue reported on code.google.com by trask.st...@gmail.com on 28 Jan 2015 at 3:39

[mernst]

Here is a compilable version of the test case:

import org.checkerframework.checker.tainting.qual.*;

class TaintingTest {

  void test(@Untainted int x) {
    @Untainted int y = x * 10;
    @Untainted String z = "test" + y;
  }
}