diff options
Diffstat (limited to 'debug/vericertTest.ml')
| -rw-r--r-- | debug/vericertTest.ml | 48 |
1 files changed, 24 insertions, 24 deletions
diff --git a/debug/vericertTest.ml b/debug/vericertTest.ml index 4d4e55f..a67d30d 100644 --- a/debug/vericertTest.ml +++ b/debug/vericertTest.ml @@ -28,9 +28,9 @@ let schedule_oracle l bb bbt = printf "F1:\n%a\n" PrintAbstr.print_forest bb'; printf "F2:\n%a\n" PrintAbstr.print_forest bbt'; flush stdout; (&&) - ((&&) ((&&) (if check l bb' bbt' then true else (Printf.printf "Failed 1\n"; false)) (empty_trees bb bbt)) - (if (check_evaluability1 reg_expr reg_expr_t) then true else (Printf.printf "Failed 12\n"; false))) - (if check_evaluability2 m_expr m_expr_t then true else (Printf.printf "Failed 13\n"; false)) + ((&&) ((&&) (if check_unhashed [] bb' bbt' then true else (Printf.printf "Failed 1\n"; false)) (empty_trees bb bbt)) + (if (check_evaluability1_unhashed bb'.forest_preds bbt'.forest_preds reg_expr reg_expr_t) then true else (Printf.printf "Failed 12\n"; false))) + (if check_evaluability2_unhashed bb'.forest_preds bbt'.forest_preds m_expr m_expr_t then true else (Printf.printf "Failed 13\n"; false)) | None -> (printf "FAILED1\n"; false)) | None -> (printf "FAILED2\n"; false) @@ -53,27 +53,27 @@ let sett p d1 r1: Gible.instr = RBsetpred (p, Ccompimm (Ceq, int 0), [reg r1], p let goto p n: Gible.instr = RBexit (p, (RBgoto (node n))) let () = - (* (if schedule_oracle [] *) - (* [ add None 2 1 4; *) - (* seteq (Some (plit true 1)) 3 4 2; *) - (* add (Some (plit true 1)) 1 2 4; *) - (* mul (Some (Pand (plit false 1, plit false 2))) 3 1 1; *) - (* mul (Some (plit true 2)) 3 1 4; *) - (* goto (Some (plit true 2)) 10; *) - (* mul (Some (plit false 2)) 3 3 3; *) - (* goto None 10; *) - (* ] *) - (* [ [ [ mul (Some (Pand (plit false 1, plit false 2))) 3 1 1; ]; *) - (* [ add None 2 1 4; *) - (* add (Some (plit true 1)) 1 2 4; *) - (* seteq (Some (plit true 1)) 3 4 2; ] ]; *) - (* [ [ mul (Some (plit true 2)) 3 1 4; ]; *) - (* [ mul (Some (plit false 2)) 3 3 3; ]; *) - (* [ goto None 10; ] *) - (* ] *) - (* ] *) - (* then Printf.printf "Passed 1\n" *) - (* else Printf.printf "Failed 1\n"); *) + (if schedule_oracle [] + [ add None 2 1 4; + seteq (Some (plit true 1)) 3 4 2; + add (Some (plit true 1)) 1 2 4; + mul (Some (Pand (plit false 1, plit false 2))) 3 1 1; + mul (Some (plit true 2)) 3 1 4; + goto (Some (plit true 2)) 10; + mul (Some (plit false 2)) 3 3 3; + goto None 10; + ] + [ [ [ mul (Some (Pand (plit false 1, plit false 2))) 3 1 1; ]; + [ add None 2 1 4; + add (Some (plit true 1)) 1 2 4; + seteq (Some (plit true 1)) 3 4 2; ] ]; + [ [ mul (Some (plit true 2)) 3 1 4; ]; + [ mul (Some (plit false 2)) 3 3 3; ]; + [ goto None 10; ] + ] + ] + then Printf.printf "Passed 1\n" + else Printf.printf "Failed 1\n"); (* (if schedule_oracle [] *) (* [ seteq (Some (plit true 1)) 2 1 2; *) (* goto None 10; *) |