User: Password:
Subscribe / Log in / New account

C89 includes blocks you know...

C89 includes blocks you know...

Posted Jun 12, 2008 16:08 UTC (Thu) by davecb (subscriber, #1574)
In reply to: C89 includes blocks you know... by ballombe
Parent article: Implications of pure and constant functions

Interestingly, allowing the internal block structure 
can increase the difficulty of doing logic on
the code to the point where building proof tools become
NP-complete (or at least insanely hard).

This is relevant if you're tying to use static analysis
tools, not just if you're trying to prove theoroms (;-))

--dave (who proveth not, but analyzeth a lot) c-b

(Log in to post comments)

C89 includes blocks you know...

Posted Jun 19, 2008 17:23 UTC (Thu) by jlokier (guest, #52227) [Link]

Hardly.  C code with blocks and variables declared inside blocks is trivially convertible to a
flat function with all variables at the start, and in trivial time.  Same goes for the control
flow blocks: they are trivially replacable with if (variable) gotos.

So the proof difficulty is identical with/without blocks and local declarations in the

Copyright © 2017, Eklektix, Inc.
Comments and public postings are copyrighted by their creators.
Linux is a registered trademark of Linus Torvalds