Crucible backend lacks a crucible_return_arbitrary command

[TomMD]

LLVM has:

    llvm_return_arbitrary : LLVMSetup ()

Indicate that an LLVM function returns an arbitrary, unspecified value.

That help text should also say "non-deterministic". Useful for modeling interactions with external entities (IO).

It appears there is no matching crucible_* operation.

[brianhuffman]

@atomb has suggested (#182) that crucible_fresh_var statements, when used in the post-condition section (i.e. after crucible_execute_func), should denote arbitrary return values like what you want. If we implemented this, then we could use them with either crucible_return to indicate an unspecified return value, or with crucible_points_to to indicate that a function writes an unspecified value through a pointer.

[TomMD]

@brianhuffman That sounds like the right outcome. I'm not sure I like the statefulness of sawscript, particularly the crucible backend where even the llvm module is implicit during verify and assume calls but that's another issue.

I'll close this ticket since it's duplicative.