Clarify Fulminate API #469
Conversation
ZippeyKeys12
added
the
Fulminate
ZippeyKeys12
force-pushed
the
clarify-fulminate-api
branch
3 times, most recently
from
3d98971 to
d1ba26d
Compare
rbanerjee20
left a comment
rbanerjee20
left a comment
There was a problem hiding this comment.
Mostly looks good to me, bar the comments/questions I've left. Thanks for doing this - the single utils.h file had become quite unruly
| #include "rts_deps.h" | ||
| #include "stack.h" | ||
|
|
||
| #define fallthrough __attribute__((__fallthrough__)) |
There was a problem hiding this comment.
Why do we still need this file at all?
| #define alignof _Alignof | ||
|
|
||
| #define bool _Bool | ||
| #define true 1 |
There was a problem hiding this comment.
We want to clean up this file too (@pqwy and I discussed it at length a few months ago) but I'm happy to leave that to be in another PR
There was a problem hiding this comment.
You should be able to edit this PR and make whatever changes you want
|
|
||
| /* Signed bitvectors */ | ||
|
|
||
| typedef struct cn_bits_i8 { |
There was a problem hiding this comment.
I'd probably prefer there to be a different header for the type definitions (e.g. fulminate/ghost_types.h), which gets included in this header, and then the rest can make up eval.h
| @@ -0,0 +1,426 @@ | |||
| #ifndef CN_EVAL_H | |||
There was a problem hiding this comment.
and minor question, but why is this under cn-executable and not fulminate?
There was a problem hiding this comment.
I've been thinking of Fulminate as the instrumentation, while the stuff in eval.h is the ability to evaluate pure CN terms.
From the testing's perspective, the instrumentation is not necessary, but rather a stronger oracle, whereas evaluating pure CN terms is necessary. In the future, testing will support being run without the instrumentation, but will still require the stuff in cn-executable.
For the counterexample program synthesis prototype, it needs to be able to evaluate CN terms, but instrumentation is unrelated.
| void cn_pop_msg_info(void); | ||
|
|
||
| void cn_assert(cn_bool* cn_b, enum spec_mode spec_mode); | ||
|
|
There was a problem hiding this comment.
shouldn't this morally also include the CN_LOAD, CN_STORE etc macros?
There was a problem hiding this comment.
Callbacks for use by testing
fulminate/api.h
Why would we want to expose those to testing frameworks? Excluding them is the main motivator for testing.
ZippeyKeys12
force-pushed
the
clarify-fulminate-api
branch
from
93a24c5 to
2e649e1
Compare
2 participants
Closes #461
Addresses the four uses:
fulminate/internals.hcn-executable/eval.hfulminate/user.hfulminate/api.hNote: This doesn't really clean up the
*.cfiles