Mercurial > urweb

changeset 1230:8768145eed1e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Havoc relations that have been updated
author Adam Chlipala <adamc@hcoop.net>
date Tue, 13 Apr 2010 09:17:52 -0400
parents a2cd6664f57f
children 5fa8ae2a34e3
files src/iflow.sml
diffstat 1 files changed, 19 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/src/iflow.sml	Sun Apr 11 17:55:37 2010 -0400
+++ b/src/iflow.sml	Tue Apr 13 09:17:52 2010 -0400
@@ -1984,6 +1984,21 @@
 
 end
 
+fun havocReln r =
+    let
+        fun hr p =
+            case p of
+                True => p
+              | False => p
+              | Unknown => p
+              | And (p1, p2) => And (hr p1, hr p2)
+              | Or (p1, p2) => Or (hr p1, hr p2)
+              | Reln (r', _) => if r' = r then True else p
+              | Cond (e, p) => Cond (e, hr p)
+    in
+        hr
+    end
+
 fun evalExp env (e as (_, loc), st) =
     let
         fun default () =
@@ -2259,6 +2274,8 @@
                          val p = And (p,
                                       And (Reln (Sql "$Old", [Var old]),
                                            Reln (Sql tab, [Var old])))
+
+                         val st = St.setAmbient (st, havocReln (Sql tab) (St.ambient st))
                      in
                          (Recd [], St.addDelete (st, (loc, And (St.ambient st, p))))
                      end
@@ -2308,6 +2325,8 @@
                                       And (Reln (Sql (tab ^ "$New"), [Recd fs]),
                                            And (Reln (Sql "$Old", [Var old]),
                                                 Reln (Sql tab, [Var old]))))
+
+                         val st = St.setAmbient (st, havocReln (Sql tab) (St.ambient st))
                      in
                          (Recd [], St.addUpdate (st, (loc, And (St.ambient st, p))))
                      end)