analyzer
analyzer copied to clipboard
goblint
Static analysis framework for C
This is work in progress on implementing the modular function summaries. The (internal) project documenting the tasks can be found [here](https://github.com/orgs/goblint/projects/12)
This draft PR enhances the detection of buffer overflows by introducing a variable for the length of array/blob as suggested by @michael-schwarz in #620. Arrays: Upon creation of a VLA...
Noticed during benchmarking of #1354 but already present on master at 8c485c924 ## No-Overflow - [ ] `./goblint --conf conf/svcomp24.json --sets ana.specification ~/Documents/sv-comp/sv-benchmarks/c/properties/no-overflow.prp --sets exp.architecture 32bit ~/Documents/sv-comp/sv-benchmarks/c/ldv-regression/test_overflow.i` (#54) ## Mem-Safety...
Inspired by @michael-schwarz's rant, this issue is for possible ideas and discussions about improving `dune runtest` output from #1367. - [x] `update_suite`: instead of printing every executed test, print a...
Leftover from #1372: Cannot have `location_invariant` right before loop because we have no non-loop-head node there. This meant our existing witness tests had to be changed to `loop_invariant`s which make...
While using the abstract debugger on an analysis that used `svcomp24` configuration, adding a breakpoint to a program point that had a warning showed a greyed-out breakpoint with the message...
We should consider enhancing the framework with backwards analyses. This could range from - Some simple textbook analyses to give to students as warmups - Trying to see if we...
While trying to minimize the examples for #1302 I noticed that our printer apparently only prints these attributes in some places, which makes it hard to extract an example that...
As discussed here https://github.com/goblint/analyzer/pull/1354/files/05bd808ad40aea8555f53f1d235f257d26d67988#r1498877891 and in the GobCon. A separate T is to be introduced that conceptually ranges over the entire environment. I gave it a shot today, but turns...
After #1340 has landed, we might want to generalize our constraint system to support Callstring-like contexts in a more natural manner. I think the only change would be to change...