search

GillianPlatform / Gillian

The Gillian Platform main repository
https://GillianPlatform.github.io
BSD 3-Clause "New" or "Revised" License
73 stars 11 forks source link

Allow empty postcondition+vanishing function calls #288

Closed N1ark closed 2 months ago

N1ark commented 4 months ago

Allows the verification of vanishing function calls and empty (false) post-conditions.

NatKarmios commented 4 months ago

Hmm, sorry to be annoying but I think I want all warnings to stdout False post-conditions is too much of a footgun to leave it lost in the log file

Not sure if it matters for this project, but be aware that prints to stdout make the debugger crash (if it's encountered while debugging) 🙂

giltho commented 4 months ago

@NatKarmios Let's just change print_to_all to only print to stdout if not in debugger mode?