Commit dc684f95 authored by Basile Desloges's avatar Basile Desloges
Browse files

[eacsl] Admit post-condition of contract init function

parent 21b49440
......@@ -57,7 +57,7 @@ typedef struct contract_t __attribute__((__FC_BUILTIN__)) contract_t;
* \return A structure to hold pieces of information about contracts at runtime.
/*@ assigns \result \from indirect:__fc_heap_status, indirect:size;
@ ensures \valid(\result); */
@ admit ensures \valid(\result); */
contract_t * contract_init(size_t size) __attribute__((FC_BUILTIN));
/*! \brief Cleanup the structure `c` previously allocated by
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment