Fix st_inc (increase dst, not src! src is not even an address)

avrmodel.mlw

@@ -225,16 +225,16 @@ let ldd (dst src ofs: register): unit
 let st_inc (dst src: register): unit
   writes { reg }
   writes { mem }
-  requires { 32 <= uint 2 reg src < pow2 16-1 }
-  ensures { let cur = uint 2 (old reg) src in
+  requires { 32 <= uint 2 reg dst < pow2 16-1 }
+  ensures { let cur = uint 2 (old reg) dst in
             let inc = cur+1 in
-            reg = (old reg)[src <- mod inc 256][src+1 <- div inc 256] }
-  ensures { let cur = uint 2 (old reg) src in
+            reg = (old reg)[dst <- mod inc 256][dst+1 <- div inc 256] }
+  ensures { let cur = uint 2 (old reg) dst in
             mem = (old mem)[cur <- reg[src]] }
-  ensures { uint 2 reg src = old(uint 2 reg src)+1 }
-= let cur = Map.get reg.data src + 256*Map.get reg.data (src+1) in
+  ensures { uint 2 reg dst = old(uint 2 reg dst)+1 }
+= let cur = Map.get reg.data dst + 256*Map.get reg.data (dst+1) in
   let nxt = mod (cur+1) (pow2 16) in
-  reg.data <- Map.set (Map.set reg.data src (mod nxt 256)) (src+1) (div nxt 256);
+  reg.data <- Map.set (Map.set reg.data dst (mod nxt 256)) (dst+1) (div nxt 256);
   mem.data <- Map.set mem.data cur (Map.get reg.data src)
 
 let std (dst ofs src: register): unit
@@ -386,7 +386,7 @@ meta compute_max_steps 0x1000000
 (* word operations *)
 let movw (dst src: register): unit
 (* TODO unnecessary
-  requires { mod dst 2 = 0 /\ mod src 2 = 0 } 
+  requires { mod dst 2 = 0 /\ mod src 2 = 0 }
 *)
   writes { reg }
   ensures { reg = old reg[dst<-reg[src]][dst+1<-reg[src+1]] }
@@ -407,7 +407,7 @@ let adiw (dst: register) (k: int): unit
   reg.data <- Map.set reg.data dst (mod sum 256);
   reg.data <- Map.set reg.data (dst+1) (mod (div sum 256) 256);
   cf.value <- (sum > 65535)
-  
+
 
 let sbiw (dst: register) (k: int): unit
   requires { 0 <= k < 64 }
@@ -539,11 +539,11 @@ lemma one_def:
   BV8.nth (BV8.of_int 1) 0 /\ forall b. 0 < b < 8 -> not BV8.nth (BV8.of_int 1) b
 
 goal bitset_correct1:
-  forall w, b, v. 0 <= b < 8 -> 
+  forall w, b, v. 0 <= b < 8 ->
     BV8.nth (bitset w b v) b = v
 
 goal bitset_correct2:
-  forall w, b i, v. 0 <= b < 8 -> 0 <= i < 8 -> i <> b -> 
+  forall w, b i, v. 0 <= b < 8 -> 0 <= i < 8 -> i <> b ->
     BV8.nth (bitset w b v) i = BV8.nth w i
 
 goal bitset_equiv_def:
@@ -617,7 +617,7 @@ use import ref.Ref
 use import AVRint as AVR
 use map.Map
 
-type shadow_registers = { 
+type shadow_registers = {
 	ghost r0: ref int;
 	ghost r1: ref int;
 	ghost r2: ref int;
@@ -684,7 +684,7 @@ predicate synchronized (self: shadow_registers) (avr: address_space) =
 	avr[28] = !(self.r28) /\
 	avr[29] = !(self.r29) /\
 	avr[30] = !(self.r30) /\
-	avr[31] = !(self.r31) 
+	avr[31] = !(self.r31)
 
 val shadow: shadow_registers