Files
SPARKlib/manual_proof.in
Johannes Kanig f5e451566d Fixes to sparklib proofs
- fixes to session generation script
- fixed line/col numbers for VCs
2026-01-20 10:53:48 +09:00

11 lines
547 B
Plaintext

spark-lemmas-arithmetic.ads:56:17:VC_POSTCONDITION
spark-lemmas-arithmetic.ads:103:16:VC_POSTCONDITION
spark-lemmas-mod_arithmetic.ads:36:16:VC_POSTCONDITION
spark-lemmas-mod_arithmetic.ads:49:16:VC_POSTCONDITION
spark-lemmas-mod_arithmetic.ads:56:16:VC_POSTCONDITION
spark-lemmas-mod_arithmetic.ads:62:16:VC_POSTCONDITION
spark-lemmas-mod_arithmetic.ads:72:16:VC_POSTCONDITION
spark-lemmas-mod_arithmetic.ads:78:17:VC_POSTCONDITION
spark-lemmas-mod_arithmetic.ads:84:17:VC_POSTCONDITION
spark-lemmas-unconstrained_array.ads:37:9:VC_POSTCONDITION