Marek Chalupa
Marek Chalupa
Hmm, isn't it different in C89? (I do not know). What I am saying is that to adhere to such a behavior, we should also have a switch that says...
By the way, related to this is also the indeterminism in evaluating operands with side effects, e.g., if the C code calls `foo() + bar()` than it is unspecified which...
In general, we would like to handle these other assertions (probably as you proposed: just replace these with __assert_fail) but in the context of SV-COMP, these are wrong benchmarks and...
check what is -const-array-opt
This are the commits from svcomp22 branch right? Don't know how much they are polished, but they have been quite well tested as they were used in SV-COMP 22. Also,...
> I am not sure whether I made any mistakes. You did not, sometimes the analyses just take too much time. > Or are there any extensions/forked projects to improve...
Hi, I have improved the data structures in PTA a bit, so you may want to try pulling new dg and trying again ;)
Did you try to use `-sc` instead of `-c`? (`-c` is an older switch that is meant to get a name of a function). And I do not see any...
Ok, found the problem. There is a bug in the reachability slicer that runs before the main slicer. You can workaround it by using `-cuttof-diverging=false`. I.e., these commands should work:...
> 1. why the results of forward slicing (e.g., `./llvm-slicer -sc "7#r" -cutoff-diverging=false -entry fact -forward fact.bc` ) seems contain the code generated by backward slicing? Because it does. It...