diff options
Diffstat (limited to 'scheduling/RTLpathSE_impl.v')
| -rw-r--r-- | scheduling/RTLpathSE_impl.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v index 71b446cc..40a05739 100644 --- a/scheduling/RTLpathSE_impl.v +++ b/scheduling/RTLpathSE_impl.v @@ -1845,10 +1845,10 @@ Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpa let (pc2, pc1) := m in (* creating the hash-consing tables *) DO hC_sval <~ hCons hSVAL;; - DO hc_scond <~ hCons hSCOND;; + DO hC_scond <~ hCons hSCOND;; DO hC_list_hsval <~ hCons hLSVAL;; DO hC_hsmem <~ hCons hSMEM;; - let hsexec := hsexec hC_sval.(hC) hC_list_hsval.(hC) hC_hsmem.(hC) hc_scond.(hC) in + let hsexec := hsexec hC_sval.(hC) hC_list_hsval.(hC) hC_hsmem.(hC) hC_scond.(hC) in (* performing the hash-consed executions *) XDEBUG pc1 (fun pc => DO name_pc <~ string_of_Z (Zpos pc);; RET ("entry-point of input superblock: " +; name_pc)%string);; DO hst1 <~ hsexec f pc1;; |