Verifying programs with ACSL contracts but without implementations.

[jesper-amilon]

It would be nice if TriCera could support the verification of programs where some functions only have an ACSL-contract, but not implementation. Essentially, you would then at call sites to the function first assert the pre-condition, and then assume the post-condition. Bonus points if it could also handle assigns clauses.

[zafer-esen]

I think this could be added while fixing #22.

[jesper-amilon]

I agree