This project has moved. For the latest updates, please go here.

Taint not propagating

Run: dependency.exe _v2.bpl /taint:v1.bpl_changed_lines.txt /prune The read function does not get tainted.

Id #6 | Release: None | Updated: Sep 8, 2016 at 8:16 PM by shuvendu | Created: Sep 8, 2016 at 7:12 PM by gyori

Build Errors (PreProcess.cs, SmackPreprocessorTransform.cs)

Installed Boogie successfully, but the build fails for SymDiff. Is the build instructions/dependencies up to date? Error 11 The type or namespace name 'ProgTransformation' could not be found (ar...

Id #5 | Release: None | Updated: Jul 31 at 4:41 PM by liyistc | Created: Mar 19, 2016 at 6:08 AM by rvt

Loop extraction bug

Original program: procedure Main() returns(r:int) { var i : int; var Flag : bool; var b : bool; i := 0; Flag := false; while(i<9) { havoc b; if (b || Flag) { i := i + 1; } else { ...

Id #4 | Release: None | Updated: Oct 28, 2015 at 1:46 AM by shuvendu | Created: Oct 14, 2015 at 8:33 PM by Guoanshisb

Dependency bug in "inlining" benchmark.

"If you run: Dependency.exe _v2.bpl /taint:v1.bpl_changed_lines.txt /prune /coarseDiff You will find that the argument of the procedure should_not_taint is not tainted by dependency, although it ...

Id #3 | Release: None | Updated: Aug 21, 2015 at 2:15 PM by nimrodpar | Created: Aug 21, 2015 at 2:04 PM by nimrodpar

Procedure extraction for nested loops looks buggy

The recent fix creates another bug. For example, procedure Main() returns(r:int) { var i,j:int; i := 0; while(i < 10) { j := 0; while(j < 10) { j := j + 1; } i := i + 1; } Its outer loop...

Id #1 | Release: None | Updated: Nov 11, 2015 at 2:39 AM by Guoanshisb | Created: May 28, 2015 at 11:53 PM by shuvendu

  • 1-5 of 5 Work Items
    • Previous
    • 1
    • Next
    • Showing
    • All
    • Work Items