Skip to content

fix outline error printing #839

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

fix outline error printing #839

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions src/ecPrinting.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2085,10 +2085,10 @@ and pp_form ppe fmt f =
pp_form_r ppe (min_op_prec, `NonAssoc) fmt f

and pp_expr ppe fmt e =
let f = match (EcEnv.Memory.get_active_ss ppe.PPEnv.ppe_env) with
| None -> form_of_expr e
| Some m -> (ss_inv_of_expr m e).inv in
pp_form ppe fmt f
let m = match (EcEnv.Memory.get_active_ss ppe.PPEnv.ppe_env) with
| None -> EcIdent.create "&hr"
| Some m -> m in
pp_form ppe fmt (ss_inv_of_expr m e).inv

and pp_tuple_expr ppe fmt e =
match e.e_node with
Expand Down
2 changes: 1 addition & 1 deletion src/phl/ecPhlOutline.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -90,7 +90,7 @@ let process_outline info tc =
| UnificationError UE_InvalidRetInstr ->
tc_error !!tc "Outline: return instruction must be an assign. Perhaps consider using the alias variant using `~`."
| UnificationError (UE_DifferentProgramLengths (s1, s2)) ->
tc_error !!tc "Outline: body's are different lengths\n%a ~ %a." (EcPrinting.pp_stmt ppe) s1 (EcPrinting.pp_stmt ppe) s2
tc_error !!tc "Outline: bodies are different lengths\n%a ~ %a." (EcPrinting.pp_stmt ppe) s1 (EcPrinting.pp_stmt ppe) s2
| UnificationError (UE_InstrNotInLockstep (i1, i2))->
tc_error !!tc "outline: instructions not in sync\n%a ~ %a." (EcPrinting.pp_instr ppe) i1 (EcPrinting.pp_instr ppe) i2
| UnificationError (UE_LvNotInLockstep (_lv1, _lv2))->
Expand Down