Simmo Saan
Simmo Saan
The function `__builtin_unreachable()` is called in many LDV benchmarks: https://github.com/sosy-lab/sv-benchmarks/search?p=17&q=__builtin_unreachable. However, the function is nowhere defined or even declared. Clearly this is supposed to be a GCC builtin: https://gcc.gnu.org/onlinedocs/gcc/Other-Builtins.html#index-_005f_005fbuiltin_005funreachable. Unfortunately...
In our own testing Goblint gave the result `true` for `ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--media--dvb-core--dvb-core.ko-entry_point.cil.out.yml` but its expected verdict is `false`. Obviously we want to fix our unsoundness so I've been desperately trying to...
Running reanalyze https://github.com/rescript-association/reanalyze/commit/389dd682223201b42c33e5c444e5c79e0805adad on Goblint https://github.com/goblint/analyzer/commit/a544002114324a207df72f9e79eb656c3ebe7b5b revealed the following. At this include of `Batteries` into a module named `All`, reanalyze complains about `Ana.result.Error` being dead: ```ocaml module All = struct...
Running reanalyze https://github.com/rescript-association/reanalyze/commit/389dd682223201b42c33e5c444e5c79e0805adad on Goblint https://github.com/goblint/analyzer/commit/a544002114324a207df72f9e79eb656c3ebe7b5b revealed the following. In a file we have this [binding operator](https://v2.ocaml.org/manual/bindingops.html) definition: ```ocaml let (let+) xs f = List.map f xs ``` This is...
Running reanalyze https://github.com/rescript-association/reanalyze/commit/389dd682223201b42c33e5c444e5c79e0805adad on Goblint https://github.com/goblint/analyzer/commit/a544002114324a207df72f9e79eb656c3ebe7b5b revealed the following. In `MyCFG` module we have the following [_re-exporting_](https://v2.ocaml.org/manual/typedecl.html) type definition: ```ocaml (** Re-exported [Edge.t] with constructors. See [Edge.t] for documentation. *)...
Running reanalyze https://github.com/rescript-association/reanalyze/commit/389dd682223201b42c33e5c444e5c79e0805adad on Goblint https://github.com/goblint/analyzer/commit/a544002114324a207df72f9e79eb656c3ebe7b5b revealed the following. In the terminal output there's a dead module warning: ``` Warning Dead Module File "./gobview/src/state/gvMessages.ml", line 1, characters 0-0 +gvMessages is...
Running reanalyze https://github.com/rescript-association/reanalyze/commit/389dd682223201b42c33e5c444e5c79e0805adad on Goblint https://github.com/goblint/analyzer/commit/a544002114324a207df72f9e79eb656c3ebe7b5b revealed the following. If an entire module is unused, then every single definition in the module is marked with a dead annotation (using `-write`...
Running reanalyze https://github.com/rescript-association/reanalyze/commit/389dd682223201b42c33e5c444e5c79e0805adad on Goblint https://github.com/goblint/analyzer/commit/a544002114324a207df72f9e79eb656c3ebe7b5b revealed the following. When `-write` modifies a file to add dead code attributes, it removes the trailing newline from the file. Since all other...
A week ago I was messing around with the `plugins.var.python.go.sort` option and noticed some issues/weird things: 1. The option's help text is incomplete, the source code contains a complete version....
**emoji.lua script provides the same functionality but is free of the issues described here and is thus recommended instead of this script.** Incoming line like (hypothetical) ``` :nick!user@123:101:ffff QUIT :my...