diff options
| author | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2021-08-18 18:05:14 +0200 |
|---|---|---|
| committer | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2021-08-18 18:05:14 +0200 |
| commit | 95d972434bd4d3b6ee0d0f68c688920dafe14afc (patch) | |
| tree | d2ddc4bb12ebd95387752a28fa7dc4861d81467f | |
| parent | d0fd34aa9cc0d3c94a2a3af56fa9d50115a0e37f (diff) | |
| download | compcert-kvx-95d972434bd4d3b6ee0d0f68c688920dafe14afc.tar.gz compcert-kvx-95d972434bd4d3b6ee0d0f68c688920dafe14afc.zip | |
Match naming convention of surrounding code.
| -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;; |