Skip to content
Snippets Groups Projects
Commit 79ad9ebe authored by Basile Desloges's avatar Basile Desloges
Browse files

[eacsl] Fix e_acsl_observation_model.h contracts

If the Frama-C libc is used, then include `__fc_alloc_axiomatic.h`,
otherwise redeclare the axiomatics from this file.

In the redeclared axiomatics, use `SIZE_MAX` instead of `__FC_SIZE_MAX`
in E-ACSL specification since the Frama-C libc will not be available to
define this constant.
parent 88555f1b
No related branches found
No related tags found
Loading
Loading
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment