2010-05-06 |
Adam Chlipala |
Some Iflow improvements for gradebook |
2010-05-01 |
Adam Chlipala |
Safe unmodeled SQL expressions marked as known |
2010-05-01 |
Adam Chlipala |
Basic handling of recursive functions in Iflow |
2010-04-29 |
Adam Chlipala |
Add rand to Basis and handle it in Iflow |
2010-04-29 |
Adam Chlipala |
Complain about DValRec; optimizations for unit-valued ECase and forgetting of path conditions across ESeq |
2010-04-19 |
Adam Chlipala |
Avoid state space explosion with ECase that just writes a constant in each case |
2010-04-18 |
Adam Chlipala |
Fix innappropriate removal of duplicate tables from DML policies |
2010-04-18 |
Adam Chlipala |
Better handling of DELETE and UPDATE |
2010-04-18 |
Adam Chlipala |
Take advantage of equalities between get_cookie calls |
2010-04-18 |
Adam Chlipala |
Use key information in more places, and catch cases where one key completion depends on another having happened already |
2010-04-18 |
Adam Chlipala |
Parsing boolean SQL constants and fixing a related prover bug |
2010-04-17 |
Adam Chlipala |
At loop heads, havoc relations that might be changed by the loop |
2010-04-15 |
Adam Chlipala |
Check for implicit flows via expressions injected into SQL |
2010-04-15 |
Adam Chlipala |
Parsing ORDER BY |
2010-04-14 |
Adam Chlipala |
Get refurbished Iflow working with calendar |
2010-04-13 |
Adam Chlipala |
More descriptive info flow error message |
2010-04-13 |
Adam Chlipala |
Completely redid main Iflow logic; so far, policy and policy2 work |
2010-04-13 |
Adam Chlipala |
Command-line use of Iflow |
2010-04-13 |
Adam Chlipala |
Catching lame FFI applications |
2010-04-13 |
Adam Chlipala |
Fix problem with overly weak ambients for queries; fix known-related bug in assert for Dt1 |
2010-04-13 |
Adam Chlipala |
When applying multiple policies at once, filter the policy set at the beginning, removing unmatchable policies |
2010-04-13 |
Adam Chlipala |
Avoid pointless rebuilding of hypothesis E-graphs |
2010-04-13 |
Adam Chlipala |
Havoc relations that have been updated |
2010-04-11 |
Adam Chlipala |
sendOwnIds policies |
2010-04-11 |
Adam Chlipala |
Using multiple policies to check a written value |
2010-04-11 |
Adam Chlipala |
Iflow working with a UNION |
2010-04-11 |
Adam Chlipala |
Use functional dependency information |
2010-04-11 |
Adam Chlipala |
Complete update records with fields that are not being set |
2010-04-11 |
Adam Chlipala |
Update policies |
2010-04-11 |
Adam Chlipala |
Express all query outputs using record literals |
2010-04-11 |
Adam Chlipala |
Delete policies |
2010-04-11 |
Adam Chlipala |
Insert policies |
2010-04-10 |
Adam Chlipala |
Constants are known |
2010-04-10 |
Adam Chlipala |
Path conditions, used to track implicit flows |
2010-04-10 |
Adam Chlipala |
Abstract type for evalExp state; handle WHERE conditions soundly |
2010-04-08 |
Adam Chlipala |
Some serious debugging of the new Cc |
2010-04-08 |
Adam Chlipala |
Implemented proper congruence closure, to the point where tests/policy works |
2010-04-08 |
Adam Chlipala |
Change query_policy to sendClient; all arguments passed to SQL predicates are variables |
2010-04-06 |
Adam Chlipala |
secret logon |
2010-04-06 |
Adam Chlipala |
Replaced Select predicate with special-case handling for one-or-no-rows queries |
2010-04-06 |
Adam Chlipala |
About to try removing Select predicate |
2010-04-06 |
Adam Chlipala |
Parsing more comparison operators |
2010-04-06 |
Adam Chlipala |
Parsing float and string SQL literals |
2010-04-06 |
Adam Chlipala |
Checking known() correctly, according to a pair of examples |
2010-04-06 |
Adam Chlipala |
Introduced the known() predicate |
2010-04-04 |
Adam Chlipala |
Parsing more of WHERE |
2010-04-04 |
Adam Chlipala |
WHERE-dependent checking |
2010-04-04 |
Adam Chlipala |
Parsed a WHERE clause |
2010-04-04 |
Adam Chlipala |
Relax checking of table implications |
2010-04-04 |
Adam Chlipala |
Iflow tested with positive and negative cases |
2010-04-04 |
Adam Chlipala |
Generating a good Iflow condition for a test query |
2010-04-04 |
Adam Chlipala |
Generated basic dummy Iflow conditions |