all_tests: list[bool] =
let m = full_map,
ori = cfar_aws_state,
vari = cfar_aws_zipr_state
in
(: test_1efc(m, ori, vari), test_1efd(m, ori, vari), test_100b(m, ori, vari), test_1e7c(m, ori, vari),
.... :)
Let's say the list is 10000 elements long. PVS produces the same warning 10000 - 50 times:
"typechecking list ... with 10000 elements: slow without knowing the type"
"typechecking list ... with 9999 elements: slow without knowing the type"
"typechecking list ... with 9998 elements: slow without knowing the type"
....
One warning would be enough. Also, it's not clear how I should fix my spec to avoid this.
I've tried adding a coercion ::list[bool] but that doesn't make any difference.
Second problem: because the list is so long, Emacs complains and beeps every time
the warning is produced:
"error in process filter: Stack overflow in regexp matcher"
Third problem: after a while, an Emacs Warnings buffer pops up to tell me
that the 'pvs' buffer is really big and the undo information was discarded because
it exceeded undo-outer-limit.
samowre
commented
3 years ago
I have a long list of booleans embedded in a let:
all_tests: list[bool] = let m = full_map, ori = cfar_aws_state, vari = cfar_aws_zipr_state in (: test_1efc(m, ori, vari), test_1efd(m, ori, vari), test_100b(m, ori, vari), test_1e7c(m, ori, vari), .... :)
Let's say the list is 10000 elements long. PVS produces the same warning 10000 - 50 times:
"typechecking list ... with 10000 elements: slow without knowing the type" "typechecking list ... with 9999 elements: slow without knowing the type" "typechecking list ... with 9998 elements: slow without knowing the type" ....
One warning would be enough. Also, it's not clear how I should fix my spec to avoid this. I've tried adding a coercion ::list[bool] but that doesn't make any difference.
Second problem: because the list is so long, Emacs complains and beeps every time the warning is produced:
"error in process filter: Stack overflow in regexp matcher"
Third problem: after a while, an Emacs Warnings buffer pops up to tell me that the 'pvs' buffer is really big and the undo information was discarded because it exceeded
undo-outer-limit.The cure is worse than the disease.