Martin Schaef

Run Infer on standalone Jar/War files.

3

I want to run Infer in bulk on a few Jar files. Is there a way to run infer capture without the `--sourcepath` option and just tell it to ingest...

Missing case in check

1

Our static analysis says that line 47 needs to be guarded, otherwise line 53 does not make sense.

Missing case in exception handling

1

We are experimenting with a static analysis tool and it suggested this change to make the exception handling more robust. The problem it reports is that f[0] is accessed in...

*Description of changes:* Adds an action to run CodeGuru Reviewer on push events to the master branch. Example is here: https://github.com/martinschaef/aws-toolkit-eclipse/actions/runs/1559154615 Recommendations will be posted to the GitHub Security tab....

Unsound result for test case

3

For some micro examples, Soot's optimizations lead to unsound results because some operations get simplified to no-ops. Below our intermediate for the failing test case [horn-encoding/regression/UnsatInstOf.java](https://github.com/jayhorn/jayhorn/blob/svcomp19/jayhorn/src/test/resources/horn-encoding/regression/UnsatInstOf.java). I'll see if I...

For our [example program](https://github.com/jayhorn/jayhorn/blob/b6f0e1fd28c8e2bd1aecce9951acf400303f02f5/jayhorn/src/test/resources/horn-encoding/lpar/SatObjectArray2.java#L14): ```java public static void main(String[] args) { final int size = 10; final int[] table = new int[size] ; Node l1 = null; Node l2 =...

Potentially buggy bytecode transformation

3

In soottocfg.test.translation_test.DynamicTest I had to disable [this test](https://github.com/jayhorn/jayhorn/blob/devel/soottocfg/src/test/resources/dynamic_tests/DynamicTest03.java#L15) because it creates illegal bytecode. I assume it has something to do with the order in which we apply transformations but I...