easyuc / EasyUC

Experiments with Universal Composability in EasyCrypt
30 stars 1 forks source link

Assertion messages formatting #11

Closed 01tomislav closed 11 months ago

01tomislav commented 11 months ago

Low priority, but assertion failures messages can use a little work:

assert of EffectMsgOut failed. The message that was sent ,((func ++ [3], 1))@ Forwarding.FwAdv.fw_obs ((func ++ [], 1), (func ++ [], 2), (epdp_pair_univ epdp_port_univ epdp_port_univ).enc ((env_root_addr, 1), ([], 1))) @((adv, 2)) is different from the asserted one ((func ++ [3], 2))@ Forwarding.FwAdv.fw_obs ((func ++ [], 1), (func ++ [], 2), (epdp_pair_univ epdp_port_univ epdp_port_univ).enc ((env_root_addr, 1), ([], 1))) @((adv, 2))]

Maybe you aren't putting a break at the right point?