search

metasepi / postmortem

Postmortem for open-source operating systems
MIT License
1 stars 0 forks source link

Avoid FreeBSD-SA-20:03.thrmisc #14

Closed master-q closed 4 years ago

master-q commented 4 years ago

It's caused by uninitialized value. ATS may easily avoid this issue with at-view. But it may be difficult at VeriFast.

master-q commented 4 years ago

Asked at mailing list: https://groups.google.com/g/ats-lang-users/c/1UPfZUz-dig

master-q commented 4 years ago

ATS2 can avoid this issue. 295cc4b899e7c79b524b9ba5512999687cd5c868

master-q commented 4 years ago

How about VeriFast?

master-q commented 4 years ago

Asked at mailing list: https://groups.google.com/g/verifast/c/vJUViRAQbkI

master-q commented 4 years ago

Bart said:

VeriFast currently does not help you find this type of problems. It currently treats an uninitialized variable just like any other variable. This is not strictly compliant with the C standard, which states that if the program reads an uninitialized variable whose address is never taken, its behavior is undefined (C18 §6.3.2.1). (Interestingly, from this paragraph it seems that reading an uninitialized variable whose address is taken is not a problem.) So it would make sense for a future version of VeriFast to distinguish between initialized and uninitialized variables and not allow reading uninitialized variables.

VeriFast can't avoid FreeBSD-SA-20:03.thrmisc.