diff options
| author | Delphine Demange <delphine.demange@irisa.fr> | 2020-11-05 15:23:08 +0100 |
|---|---|---|
| committer | Delphine Demange <delphine.demange@irisa.fr> | 2020-11-05 15:23:08 +0100 |
| commit | ea755b0fb4b1dda69faa9e3206a90ae1cd1da16e (patch) | |
| tree | b10fc99930116b4f32a952eb861fafb23d4dbbb5 | |
| parent | b58c3626a7a0c85da5d598e238466b0647830e7f (diff) | |
| download | compcert-kvx-ea755b0fb4b1dda69faa9e3206a90ae1cd1da16e.tar.gz compcert-kvx-ea755b0fb4b1dda69faa9e3206a90ae1cd1da16e.zip | |
low-cost error messages
| -rw-r--r-- | midend/CSSAgen.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/midend/CSSAgen.v b/midend/CSSAgen.v index 968195c6..1e67c810 100644 --- a/midend/CSSAgen.v +++ b/midend/CSSAgen.v @@ -149,7 +149,7 @@ Qed. Definition add_parcopy (parcopy: CSSA.parcopy) (pc: node) : mon unit := fun s => match PTree.get pc (st_parcopycode s) with - | None => Error (Errors.msg "") + | None => Error (Errors.msg "CSSAgen - 1") | Some parcopies => let new_parcb := parcopy :: parcopies in @@ -188,7 +188,7 @@ Definition add_new_phi (dst': reg ) (args': list reg) (pc: node) := fun s => match PTree.get pc (st_phicode s) with - | None => Error (Errors.msg "") + | None => Error (Errors.msg "CSSAgen - 2") | Some phib' => OK tt (mkstate |