val p4 : IfcMonitor.com
let p4 = If (AOp Plus (AVar (to_id 3)) (AInt (- 5))) (Assign (to_id 1) (AInt 0)) Skip
(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module IfcMonitorTest

open Label
open IfcMonitor
open FStar.DM4F.Heap.IntStoreFixed
module T = FStar.Tactics

assume val from_id (x:id) : GTot int
assume
val to_from_inv (x:nat{x `op_LessThan` store_size})
  : Lemma
    (ensures from_id (to_id x) == x)
    [SMTPat (to_id x)]
  
  

(* Some test cases *)

let h0 = create 5
let env x = if x = to_id 3 || x = to_id 4 then High else Low

(* l1 := h1 *)
let p1 = Assign (to_id 1) (AVar (to_id 3))
let test1 = 
  assert (None? (interpret_com h0 p1 env Low))

          

(* l1 := l2 *)
let p2 = Assign (to_id 1) (AVar (to_id 2))
let test2 = assert_norm (Some? (interpret_com h0 p2 env Low))

(* If (h1 + 2 <> 0 then {l1 := 9}   [env0(h1) = 5] *)
let p3 = If (AOp Plus (AVar (to_id 3)) (AInt 2)) (Assign (to_id 1) (AInt 0)) Skip
let test3 = assert_norm (None? (interpret_com h0 p3 env Low))

(* This is example shows a difference to the type system*)
/
prims.fst.checked label.fst.checked IfcMonitor.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.fsti.checked FStar.DM4F.Heap.IntStoreFixed.fsti.checked
IfcMonitorTest.fst
IfcMonitor.com
IfcMonitor.If IfcMonitor.AOp IfcMonitor.Plus IfcMonitor.AVar FStar.DM4F.Heap.IntStoreFixed.to_id IfcMonitor.AInt Prims.op_Minus IfcMonitor.Assign IfcMonitor.Skip
let p4 =
  
If (AOp Plus (AVar (to_id 3)) (AInt (- 5))) (Assign (to_id 1) (AInt 0)) Skip