proof: starting support for e-acsl runtime assertion as advanced security mode#34
Draft
PThierry wants to merge 8 commits into
Draft
proof: starting support for e-acsl runtime assertion as advanced security mode#34PThierry wants to merge 8 commits into
PThierry wants to merge 8 commits into
Conversation
PThierry
force-pushed
the
functional-proof/e-acsl-support
branch
3 times, most recently
from
June 23, 2025 14:20
76108da to
e3ff20e
Compare
PThierry
changed the title
PThierry
force-pushed
the
functional-proof/e-acsl-support
branch
from
June 23, 2025 14:37
e3ff20e to
6ffbc91
Compare
PThierry
added
question
PThierry
force-pushed
the
functional-proof/e-acsl-support
branch
from
October 4, 2025 08:45
f3878bb to
2b0ab26
Compare
NOTE: need CEA support on this
fixing e-acsl call with fewer checks
PThierry
force-pushed
the
functional-proof/e-acsl-support
branch
from
February 18, 2026 14:08
2b0ab26 to
66125bf
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR enables the support for generated annotated C code using e-acsl based on the various ACSL assertions written in the input C file.
The ability to add e-acsl annotations is supported kernel-wide and is made to be enabled easily.
By now, the kernel zlib's string.c implementation of memset/memcpy/strnlen do support e-acsl annotations.
Triggering the annotated C code generation and inclusion is made based on the
CONFIG_SECU_ENABLE_EACSLkconfig trigger (default n).In that very case, Frama-C, including the e-acsl plugin and the
e-acsl-gcc.shtool, generates annotated sources that allow automatically runtime assertion checks baed on static frama-C assertions, that have been proven as valid in a sound model.As a consequence, any invalid runtime assertion can't be triggered through a valid logical path and is the consequence of an external event (EM, fault).
runtime annotations increase the kernel size, and is deactivated by default. By now, only the string memory manipulation library is protected (as already validated as correct in a sound envionrment), but such runtime assertions can be generated to any code part that is already demonstrated as correct without risk.
NOTE: need CEA support on this, ass the e-acsl plugin C symbols implementation library need to be compiled and linked