Reese Levine comments

Repositories
Issues
Comments

Results 4 comments of


                                            Reese Levine

Data Race Handling

Ah ok, and it's because Dartagnan operates directly on the source files that it doesn't have to worry about UB caused by data races in the C code when running...

Issue in constraint generation enforcing reads-from

Although, adding this constraint causes many of the existing tests to fail, so need to look into this a little more.

Issue in constraint generation enforcing reads-from

Ok, needed to add a couple checks to deal with cases where write/read values are unconstrained. The full condition now is: ``` } else if (instState.loadStore[i].var == instState.loadStore[j].var && instState.isWrite(i)...

Issue in constraint generation enforcing reads-from

I'm running into one other potentially buggy test outcome. Given this test: ``` NEWWG NEWSG NEWTHREAD st.sc0 a = 1 ld.sc0 b = 1 NOSOLUTION consistent[X] && #dr=0 ``` A...