search

au-ts / cogent

Cogent Project
https://trustworthy.systems/projects/TS/cogent.pml
Other
158 stars 26 forks source link

&& and || should shortcut #215

Open zilinc opened 6 years ago

zilinc commented 6 years ago

Issue by chu090 Wed Dec 9 08:58:51 2015 Originally opened as https://github.csiro.au/ts-filesystems/Cogent/issues/110

We're doing more work than necessary. For instance, in ext2_match, the code is dirent.inode /= 0 && wordarray_cmp (c_name, dirent.name)

If dirent.inode is zero there's no need to call the external comparison function.

zilinc commented 6 years ago

Comment by lim060 Wed Dec 9 09:51:11 2015

We can't always translate this to the desired && in C, because the right operand could (and in this case, will) generate multiple statements. The simplest solution now is to just implement the short-circuiting manually:

if dirent.inode /= 0 then wordarray_cmp(c_name, dirent.name) else False

(The ANF compiler pass then blows it up, but that's another issue.)