Famous proven but not tested has been fixed

4 files changed, 14 insertions, 14 deletions

diff --git a/Makefile b/Makefile
index 3128c23..3f387f3 100644
--- a/Makefile
+++ b/Makefile
@@ -38,7 +38,7 @@ lib/COMPCERTSTAMP: lib/CompCert/Makefile.config
 	$(MAKE) HAS_RUNTIME_LIB=false CLIGHTGEN=false INSTALL_COQDEV=false -C lib/CompCert
 	touch $@
 
-install: docs/vericert.1
+install: doc/vericert.1
 	sed -i'' -e 's/arch=verilog/arch=x86/' _build/default/driver/compcert.ini
 	install -d $(PREFIX)/bin
 	install -C -m 644 _build/default/driver/compcert.ini $(PREFIX)/bin
diff --git a/src/hls/Partition.ml b/src/hls/Partition.ml
index 545277b..4e699e6 100644
--- a/src/hls/Partition.ml
+++ b/src/hls/Partition.ml
@@ -73,7 +73,7 @@ let rec next_bblock_from_RTL is_start e (c : RTL.code) s i =
     if List.exists (fun x -> x = s) (fst e) then
       Errors.OK { bb_body = [i']; bb_exit = RBgoto s' }
     else if List.exists (fun x -> x = s) (snd e) && not is_start then
-      Errors.OK { bb_body = [RBnop]; bb_exit = RBgoto s }
+      Errors.OK { bb_body = []; bb_exit = RBgoto s }
     else begin
       match next_bblock_from_RTL false e c s' i_n with
       | Errors.OK bb ->
diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v
index 214da6f..d425049 100644
--- a/src/hls/RTLPargen.v
+++ b/src/hls/RTLPargen.v
@@ -227,7 +227,7 @@ We define the top-level oracle that will check if two basic blocks are
 equivalent after a scheduling transformation.
 |*)
 
-Definition empty_trees (bb: list RTLBlock.bb) (bbt: list RTLPar.bb) : bool :=
+Definition empty_trees (bb: RTLBlock.bb) (bbt: RTLPar.bb) : bool :=
   match bb with
   | nil =>
     match bbt with
diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v
index 689c11a..f975601 100644
--- a/src/hls/RTLPargenproof.v
+++ b/src/hls/RTLPargenproof.v
@@ -590,7 +590,7 @@ Proof.
     econstructor; auto.
     match goal with H: eval_pred _ _ _ _ |- _ => inv H end.
     repeat econstructor; try erewrite match_states_list; eauto.
-  - destruct p. match goal with H: eval_pred _ _ _ _ |- _ => inv H end.
+  (*- destruct p. match goal with H: eval_pred _ _ _ _ |- _ => inv H end.
     repeat econstructor; try erewrite match_states_list; eauto.
     erewrite <- eval_predf_pr_equiv; eassumption.
     apply PTree_matches; assumption.
@@ -615,7 +615,7 @@ Proof.
     match goal with
     H: forall _, _ |- context[Mem.storev] => erewrite <- H; eauto
     end.
-  - admit. Admitted.
+  - admit.*) Admitted.
 
 Lemma step_instr_list_matches :
   forall a ge sp st st',
@@ -799,22 +799,22 @@ Definition match_prog (prog : RTLBlock.program) (tprog : RTLPar.program) :=
 (* TODO: Fix the `bb` and add matches for them. *)
 Inductive match_stackframes: RTLBlock.stackframe -> RTLPar.stackframe -> Prop :=
 | match_stackframe:
-    forall f tf res sp pc rs rs' ps ps' bb bb',
+    forall f tf res sp pc rs rs' ps ps',
       transl_function f = OK tf ->
       (forall x, rs !! x = rs' !! x) ->
       (forall x, ps !! x = ps' !! x) ->
-      match_stackframes (Stackframe res f sp pc bb rs ps)
-                        (Stackframe res tf sp pc bb' rs' ps').
+      match_stackframes (Stackframe res f sp pc rs ps)
+                        (Stackframe res tf sp pc rs' ps').
 
 Inductive match_states: RTLBlock.state -> RTLPar.state -> Prop :=
 | match_state:
-    forall sf f sp pc rs rs' m sf' tf ps ps' bb bb'
+    forall sf f sp pc rs rs' m sf' tf ps ps'
       (TRANSL: transl_function f = OK tf)
       (STACKS: list_forall2 match_stackframes sf sf')
       (REG: forall x, rs !! x = rs' !! x)
       (REG: forall x, ps !! x = ps' !! x),
-      match_states (State sf f sp pc bb rs ps m)
-                   (State sf' tf sp pc bb' rs' ps' m)
+      match_states (State sf f sp pc rs ps m)
+                   (State sf' tf sp pc rs' ps' m)
 | match_returnstate:
     forall stack stack' v m
       (STACKS: list_forall2 match_stackframes stack stack'),
@@ -1044,11 +1044,11 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
 
   (* TODO: Fix these proofs, now the cf_instr is in the State. *)
   Lemma step_cf_instr_correct:
-    forall t s s',
-      step_cf_instr ge s t s' ->
+    forall t s s' cf,
+      step_cf_instr ge s cf t s' ->
       forall r,
         match_states s r ->
-        exists r', step_cf_instr tge r t r' /\ match_states s' r'.
+        exists r', step_cf_instr tge r cf t r' /\ match_states s' r'.
   Proof using TRANSL.
 
     (*induction 1; repeat semantics_simpl;